-- Mathlib/CategoryTheory/Galois/Examples.lean
theorem Action.isConnected_of_transitive (X : FintypeCat) [MulAction G X]
    [MulAction.IsPretransitive G X] [h : Nonempty X] :
    IsConnected (Action.FintypeCat.ofMulAction G X) where
  notInitial := not_initial_of_inhabited (Action.forget _ _) h.some
  noTrivialComponent Y i hm hni

Proof state:
case refine_2
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'

Tactic:
obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'

Result:
case refine_2.intro
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'

Proof state:
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
⊢ IsIso i

Tactic:
obtain ⟨(y : Y.V)⟩ := (not_initial_iff_fiber_nonempty (Action.forget _ _) Y).mp hni

Result:
case intro
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
⊢ IsIso i

Proof state:
case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ (ConcreteCategory.hom i.hom) (σ • y) = x'

Tactic:
show (Y.ρ σ ≫ i.hom) y = x'

Result:
case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ (Y.ρ σ ≫ i.hom) y = x'

Proof state:
case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ (Action.FintypeCat.ofMulAction G X).ρ σ (i.hom y) = x'

Tactic:
exact hσ

Result:
no goals

Proof state:
case refine_1
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
this : Mono i.hom
⊢ Function.Injective ⇑(ConcreteCategory.hom i.hom)

Tactic:
exact ConcreteCategory.injective_of_mono_of_preservesPullback i.hom

Result:
no goals

Proof state:
case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ (Y.ρ σ ≫ i.hom) y = x'

Tactic:
rw [i.comm, FintypeCat.comp_apply]

Result:
case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ (Action.FintypeCat.ofMulAction G X).ρ σ (i.hom y) = x'

Proof state:
case intro
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
this : IsIso i.hom
⊢ IsIso i

Tactic:
apply isIso_of_reflects_iso i (Action.forget _ _)

Result:
no goals

Proof state:
case refine_1
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
⊢ Function.Injective ⇑(ConcreteCategory.hom i.hom)

Tactic:
haveI : Mono i.hom := map_mono (forget₂ _ _) i

Result:
case refine_1
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
this : Mono i.hom
⊢ Function.Injective ⇑(ConcreteCategory.hom i.hom)

Proof state:
case refine_2.intro
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'

Tactic:
use σ • y

Result:
case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
σ : G
hσ : σ • x = x'
⊢ (ConcreteCategory.hom i.hom) (σ • y) = x'

Proof state:
case refine_2
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'

Tactic:
letI x : X := i.hom y

Result:
case refine_2
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.carrier
inst✝ : MulAction.IsPretransitive G X.carrier
h : Nonempty X.carrier
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : IsInitial Y → False
y : Y.V.carrier
x' : (Action.FintypeCat.ofMulAction G X).V.carrier
x : X.carrier := i.hom y
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'