-- Mathlib/CategoryTheory/Galois/Examples.lean
theorem Action.pretransitive_of_isConnected (X : Action FintypeCat G)
    [IsConnected X] : MulAction.IsPretransitive G X.V where
  exists_smul_eq x y

Proof state:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this✝ : Mono i
this : IsIso i
hb : Function.Bijective i.hom
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨⟨y', ⟨g, (hg : g • x = y')⟩⟩, (hy' : y' = y)⟩ := hb.surjective y

Result:
case intro.mk.intro
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this✝ : Mono i
this : IsIso i
hb : Function.Bijective i.hom
y' : X.V.carrier
g : G
hg : g • x = y'
hy' : y' = y
⊢ ∃ g, g • x = y

Proof state:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝¹ : Fintype ↑T
this✝ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this : Mono i
⊢ ∃ g, g • x = y

Tactic:
have : IsIso i := by
  apply IsConnected.noTrivialComponent T' i
  apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr
  exact Set.Nonempty.coe_sort (MulAction.orbit_nonempty x)

Result:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this✝ : Mono i
this : IsIso i
⊢ ∃ g, g • x = y

Proof state:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this : Fintype ↑T
⊢ ∃ g, g • x = y

Tactic:
letI : MulAction G (FintypeCat.of T) := inferInstanceAs <| MulAction G ↑(MulAction.orbit G x)

Result:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝ : Fintype ↑T
this : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
⊢ ∃ g, g • x = y

Proof state:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this✝ : Mono i
this : IsIso i
⊢ Function.Bijective i.hom

Tactic:
apply (ConcreteCategory.isIso_iff_bijective i.hom).mp

Result:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this✝ : Mono i
this : IsIso i
⊢ IsIso i.hom

Proof state:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝ : Fintype ↑T
this : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
⊢ ∃ g, g • x = y

Tactic:
have : Mono i := ConcreteCategory.mono_of_injective _ (Subtype.val_injective)

Result:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝¹ : Fintype ↑T
this✝ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this : Mono i
⊢ ∃ g, g • x = y

Proof state:
case h
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
T : Set X.V.carrier := MulAction.orbit G x
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).carrier := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }
this✝ : Mono i
this : IsIso i
hb : Function.Bijective i.hom
y' : X.V.carrier
g : G
hg : g • x = y'
hy' : y' = y
⊢ g • x = y

Tactic:
exact hg.trans hy'

Result:
no goals