-- Mathlib/Algebra/Group/Subgroup/Order.lean
lemma isCoatom_comap_of_surjective
    {H : Type*} [Group H] {φ : G →* H} (hφ : Function.Surjective φ)
    {M : Subgroup H} (hM : IsCoatom M) : IsCoatom (M.comap φ)

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
⊢ K = ⊤

Tactic:
rw [comap_map_eq_self ((M.ker_le_comap φ).trans hK.le), comap_top] at hM

Result:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < K → K = ⊤
⊢ K = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM : IsCoatom M
⊢ IsCoatom (comap φ M)

Tactic:
refine And.imp (fun hM ↦ ?_) (fun hM ↦ ?_) hM

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : M ≠ ⊤
⊢ comap φ M ≠ ⊤

case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
⊢ ∀ (b : Subgroup G), comap φ M < b → b = ⊤

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
⊢ ∀ (b : Subgroup G), comap φ M < b → b = ⊤

Tactic:
intro K hK

Result:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
K : Subgroup G
hK : comap φ M < K
⊢ K = ⊤

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : M ≠ ⊤
⊢ comap φ M ≠ ⊤

Tactic:
rwa [← (comap_injective hφ).ne_iff, comap_top] at hM

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
K : Subgroup G
hK : comap φ M < K
⊢ K = ⊤

Tactic:
specialize hM (K.map φ)

Result:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : M < map φ K → map φ K = ⊤
⊢ K = ⊤

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < K → K = ⊤
⊢ K = ⊤

Tactic:
exact hM hK

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : M < map φ K → map φ K = ⊤
⊢ K = ⊤

Tactic:
rw [← comap_lt_comap_of_surjective hφ, ← (comap_injective hφ).eq_iff] at hM

Result:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
⊢ K = ⊤