-- 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:
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

Tactic:
use g

Result:
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

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))
⊢ ∃ g, g • x = y

Tactic:
let T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of T)

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)
⊢ ∃ g, g • x = y

Proof state:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.carrier
⊢ ∃ g, g • x = y

Tactic:
let T : Set X.V := 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
⊢ ∃ 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
⊢ Nonempty ((Action.forget FintypeCat G).obj T').carrier

Tactic:
exact Set.Nonempty.coe_sort (MulAction.orbit_nonempty x)

Result:
no goals

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
⊢ IsIso i

Tactic:
apply IsConnected.noTrivialComponent T' i

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
⊢ IsInitial T' → False

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
⊢ IsIso i.hom

Tactic:
exact map_isIso (forget₂ _ FintypeCat) i

Result:
no goals

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
⊢ ∃ g, g • x = y

Tactic:
have : Fintype T := Fintype.ofFinite T

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
⊢ ∃ 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
⊢ ∃ g, g • x = y

Tactic:
have hb : Function.Bijective i.hom := by
  apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
  exact map_isIso (forget₂ _ FintypeCat) i

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
hb : Function.Bijective i.hom
⊢ ∃ 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)
⊢ ∃ g, g • x = y

Tactic:
let i : T' ⟶ X := ⟨Subtype.val, fun _ ↦ rfl⟩

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 := ⋯ }
⊢ ∃ 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
⊢ IsInitial T' → False

Tactic:
apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr

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
⊢ Nonempty ((Action.forget FintypeCat G).obj T').carrier