-- Mathlib/GroupTheory/Coset/Basic.lean
theorem strictMono_comap_prod_image :
    StrictMono fun t : Subgroup α ↦ (t.comap s.subtype, mk (s := s) '' t)

Proof state:
case h.e'_1
α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ ↑t₂
le1 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
a' : α
h' : a' ∈ ↑t₁
eq : ↑a' = ↑a
⊢ a' * s.subtype ⟨a'⁻¹ * a, ⋯⟩ = a

Tactic:
apply mul_inv_cancel_left

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ StrictMono fun t => (Subgroup.comap s.subtype t, mk '' ↑t)

Tactic:
refine fun t₁ t₂ h ↦ ⟨⟨Subgroup.comap_mono h.1, Set.image_mono h.1⟩,
  mt (fun ⟨le1, le2⟩ a ha ↦ ?_) h.2⟩

Result:
α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ ↑t₂
le1 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
⊢ a ∈ ↑t₁

Proof state:
α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ ↑t₂
le1 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
⊢ a ∈ ↑t₁

Tactic:
obtain ⟨a', h', eq⟩ := le2 ⟨_, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ ↑t₂
le1 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
a' : α
h' : a' ∈ ↑t₁
eq : ↑a' = ↑a
⊢ a ∈ ↑t₁

Proof state:
case intro.intro
α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ ↑t₂
le1 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
a' : α
h' : a' ∈ ↑t₁
eq : ↑a' = ↑a
⊢ a ∈ ↑t₁

Tactic:
convert ← t₁.mul_mem h' (@le1 ⟨_, QuotientGroup.eq.1 eq⟩ <| t₂.mul_mem (t₂.inv_mem <| h.1 h') ha)

Result:
case h.e'_1
α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ ↑t₂
le1 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 :
  ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ≤ ((fun t => (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
a' : α
h' : a' ∈ ↑t₁
eq : ↑a' = ↑a
⊢ a' * s.subtype ⟨a'⁻¹ * a, ⋯⟩ = a