Query about basic proofs

Stream: new members

[Atif Sarwar Sayed]

image.png

I'm a beginner, and I can't figure out how I can prove these.. I tried "by exact?" and it gives me these options, but I don't know what I should write after this.

[Riccardo Brasca]

I guess you just proved them (since they are already in the library exact? is able to find the correct lemma).

[Riccardo Brasca]

In the future please try to write a #mwe

[Atif Sarwar Sayed]

Right, but the info-view doesn't show that the lemma is proved..? Also, here is the whole code:
image.png

[Atif Sarwar Sayed]

right, that's not an mwe, one sec

[Atif Sarwar Sayed]

import Mathlib
import Mathlib.Tactic
import Mathlib.Algebra.Group.Action.Basic
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
import Mathlib.Algebra.Group.Subgroup.Defs
import Mathlib.Algebra.Group.Submonoid.MulAction
import Mathlib.Data.Set.BooleanAlgebra
open scoped BigOperators
open MulAction
section GroupActions
variable (X : Type)
variable (G : Type) [Group G]
variable [MulAction G X]
lemma orbit_mem_iff (x y: X):
 y ∈ orbit G x ↔ ∃ g : G, g • x = y :=
 by exact mem_orbit_iff
lemma stabilizer_mem_iff (x : X) (g : G) :
 g ∈ stabilizer G x ↔ g • x = x :=
 by exact mem_stabilizer_iff

[Vlad Tsyrklevich]

If you put your cursor before the exact, and then go one step right, you will see that it goes to "No goals", e.g. it is proved. If you replace the exact ... with constructor you will see the highlighted red line showing you it is not proved.

[Atif Sarwar Sayed]

Ahhh! Ok I was confused because I had switched to the online compiler from vscode. Thanks everyone!!