awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
simp :
  ∀
    (hw₁'3 :
      ∀ u ∈ Option.map Prod.fst w₁.toList.head?,
        w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G))
    (hw₂'3 :
      ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
        w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)),
    ∀ u ∈ Option.map Prod.fst w₁.toList.head?,
      w₁.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
⊢ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)

Tactic:
simp only [← leftCoset_eq_iff] at *

Premises used: leftCoset_eq_iff
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 :
  ∀ u ∈ Option.map Prod.fst w₁.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G)
hw₂'3 :
  ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
rw : u ∈ Option.map Prod.fst w₂.toList.head?
⊢ w₁.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)

Tactic:
rw [← hw₁'3 _ hu, ← hw₂'3 _]
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 :
  ∀ u ∈ Option.map Prod.fst w₁.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G)
hw₂'3 :
  ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
rwa : u ∈ (List.map Prod.fst w₂.toList).head?
rwa₁ : u ∈ (List.map Prod.fst w₁'.toList).head?
rwa₂ : u ∈ (List.map Prod.fst w₁.toList).head?
rwa₃ rwa₄ rwa₅ rwa₆ : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ u ∈ Option.map Prod.fst w₂.toList.head?

Tactic:
rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map]

Premises used: List.head?_map
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
hw : Membership.mem (γ := Subgroup (HNNExtension G A B φ)) (MonoidHom.range of) (ReducedWord.prod φ w)
rcases : ∀ (g : G) (hg : (of : (a : G) → HNNExtension G A B φ) g = ReducedWord.prod φ w), w.toList = []
⊢ w.toList = []

Tactic:
rcases hw with ⟨g, hg⟩
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : (of : (a : G) → HNNExtension G A B φ) g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ ReducedWord.prod φ w = ReducedWord.prod φ w'

Tactic:
simp [w', ReducedWord.prod, hg]

Premises used: HNNExtension.NormalWord.ReducedWord.prod
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : (of : (a : G) → HNNExtension G A B φ) g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ ReducedWord.prod φ w = ReducedWord.prod φ w'

Tactic:
have : w.prod φ = w'.prod φ := by simp [w', ReducedWord.prod, hg]
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : (of : (a : G) → HNNExtension G A B φ) g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
this : ReducedWord.prod φ w = ReducedWord.prod φ w'
⊢ w.toList = []

Tactic:
simpa [w'] using (map_fst_eq_and_of_prod_eq φ this).1

Premises used: And.left, HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
simp :
  ∀ (x y : G'),
    x⁻¹ * y ∈ comap f H ↔ HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G) ∈ H
⊢ ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)

Tactic:
simp only [QuotientGroup.leftRel_apply]

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x y : G'
rw :
  HMul.hMul (α := G) (β := G) ((f : (a : G') → G) x⁻¹ : G) ((f : (a : G') → G) y : G) =
    HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)
rw₁ rw₂ :
  HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G) =
    HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)
⊢ (f : (a : G') → G) (x⁻¹ * y) = HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)

Tactic:
rw [f.map_mul, f.map_inv]

Premises used: MonoidHom.map_inv, MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
⊢ ∀ (x y : G'),
    x⁻¹ * y ∈ comap f H ↔ HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G) ∈ H

Tactic:
exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))

Premises used: Membership.mem, congr_arg, iff_of_eq
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
⊢ ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)

Tactic:
have key : ∀ x y : G',
      QuotientGroup.leftRel (H.comap f) x y ↔ QuotientGroup.leftRel H (f x) (f y) := by
    simp only [QuotientGroup.leftRel_apply]
    exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
⊢ (comap f H).index = H.index

Tactic:
Nat.card_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)

Premises used: Nat.card_congr, And.intro, Subgroup.index, Equiv.ofBijective, Iff.mp, Quotient.map', DFunLike.coe
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
refine_1 : Injective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)
refine_2 : Surjective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)
⊢ (comap f H).index = H.index

Tactic:
refine Nat.card_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)

Premises used: Nat.card_congr, And.intro, Equiv.ofBijective, Iff.mp, Quotient.map', DFunLike.coe
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
⊢ ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))

Tactic:
simp_rw [← Quotient.eq''] at key

Premises used: Quotient.eq''
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
⊢ Injective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)

Tactic:
Quotient.ind' fun x => ?_

Premises used: Quotient.ind', Function.Injective
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
refine_1 :
  ∀ (x : G') ⦃a₂ : G' ⧸ comap f H⦄,
    Eq.{u_1 + 1} (α := G ⧸ H)
        (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' x))
        (Quotient.map' (⇑f : (a : G') → G) ⋯ a₂) →
      Quotient.mk'' x = a₂
⊢ Injective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)

Tactic:
refine Quotient.ind' fun x => ?_
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄,
    Eq.{u_1 + 1} (α := G ⧸ H)
        (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' x))
        (Quotient.map' (⇑f : (a : G') → G) ⋯ a₂) →
      Quotient.mk'' x = a₂

Tactic:
Quotient.ind' fun y => ?_

Premises used: Quotient.ind'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
x : G'
refine_1 :
  ∀ (y : G'),
    Eq.{u_1 + 1} (α := G ⧸ H)
        (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' x))
        (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' y)) →
      Eq (α := G' ⧸ comap f H) (Quotient.mk'' x) (Quotient.mk'' y)
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄,
    Eq.{u_1 + 1} (α := G ⧸ H)
        (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' x))
        (Quotient.map' (⇑f : (a : G') → G) ⋯ a₂) →
      Quotient.mk'' x = a₂

Tactic:
refine Quotient.ind' fun y => ?_
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
x y : G'
⊢ Eq.{u_1 + 1} (α := G ⧸ H)
      (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' x))
      (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' y)) →
    Eq (α := G' ⧸ comap f H) (Quotient.mk'' x) (Quotient.mk'' y)

Tactic:
(key x y).mpr

Premises used: Iff.mpr, Quot.map, Quotient.map'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
x y : G'
⊢ Eq.{u_1 + 1} (α := G ⧸ H)
      (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' x))
      (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' y)) →
    Eq (α := G' ⧸ comap f H) (Quotient.mk'' x) (Quotient.mk'' y)

Tactic:
exact (key x y).mpr

Premises used: Iff.mpr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
⊢ Surjective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)

Tactic:
Quotient.ind' fun x => ?_

Premises used: Quotient.ind', Function.Surjective
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
refine_2 : ∀ (x : G), ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯ a) (Quotient.mk'' x)
⊢ Surjective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)

Tactic:
refine Quotient.ind' fun x => ?_
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
x : G
refine_2 :
  ∀ (y : G') (hy : (f : (a : G') → G) y = x),
    ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯ a) (Quotient.mk'' x)
⊢ ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯ a) (Quotient.mk'' x)

Tactic:
obtain ⟨y, hy⟩ := hf x
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
x : G
y : G'
hy : (f : (a : G') → G) y = x
⊢ ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯ a) (Quotient.mk'' x)

Tactic:
⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩

Premises used: QuotientGroup.mk, Quotient.mk'', congr_arg, Exists.intro, Quotient.map'_mk'', DFunLike.coe, Eq.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
x : G
y : G'
hy : (f : (a : G') → G) y = x
⊢ ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯ a) (Quotient.mk'' x)

Tactic:
exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
⊢ comap f H = comap f.rangeRestrict (H.subgroupOf f.range)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
rw : ((comap f H).subgroupOf K).index = H.relIndex (map f K)
rw₁ : (comap K.subtype (comap f H)).index = H.relIndex (map f K)
rw₂ : (comap (f.comp K.subtype) H).index = H.relIndex (map f K)
rw₃ : H.relIndex (f.comp K.subtype).range = H.relIndex (map f K)
rw₄ : H.relIndex (map f K.subtype.range) = H.relIndex (map f K)
rw₅ rw₆ : H.relIndex (map f K) = H.relIndex (map f K)
⊢ (comap f H).relIndex K = H.relIndex (map f K)

Tactic:
rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]

Premises used: Subgroup.subgroupOf, MonoidHom.map_range, Subgroup.relIndex, Subgroup.index_comap, Subgroup.comap_comap, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
H K : Subgroup G
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : (comap f (map f H)).relIndex K = H.relIndex K
rw₁ rw₂ : H.relIndex K = H.relIndex K
⊢ (map f H).relIndex (map f K) = H.relIndex K

Tactic:
rw [← Subgroup.relIndex_comap, Subgroup.comap_map_eq_self_of_injective hf]

Premises used: Subgroup.comap_map_eq_self_of_injective, Subgroup.relIndex_comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
H K : Subgroup G
rw : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (K ⊔ f.ker)
rw₁ : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (comap f (map f K))
rw₂ : (map f H).relIndex (map f K) = (map f H).relIndex (map f (comap f (map f K)))
rw₃ rw₄ : (map f H).relIndex (map f K) = (map f H).relIndex (map f K)
⊢ (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)

Tactic:
rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]

Premises used: Subgroup.gc_map_comap, GaloisConnection.l_u_l_eq_l, Subgroup.comap_map_eq, Subgroup.relIndex_comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
rw : K.index * H.relIndex K = H.index
⊢ H.relIndex K * K.index = H.index

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
simp_rw : K.index * (H.subgroupOf K).index = H.index
simp_rw₁ : Nat.card.{u_1} (G ⧸ K) * Nat.card.{u_1} (↥K ⧸ H.subgroupOf K) = Nat.card.{u_1} (G ⧸ H)
simp_rw₂ : Nat.card.{u_1} ((G ⧸ K) × ↥K ⧸ H.subgroupOf K) = Nat.card.{u_1} (G ⧸ H)
⊢ K.index * H.relIndex K = H.index

Tactic:
simp_rw [relIndex, index, ← Nat.card_prod, Nat.card_congr <| quotientEquivProdOfLE h]

Premises used: Subgroup.relIndex, Nat.card_congr, Subgroup.index, Nat.card_prod, Subgroup.quotientEquivProdOfLE
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index ∣ H.index

Tactic:
dvd_of_mul_left_eq (H.relIndex K) (relIndex_mul_index h)

Premises used: Subgroup.relIndex_mul_index, dvd_of_mul_left_eq, Subgroup.relIndex
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ H.relIndex K ∣ H.index

Tactic:
dvd_of_mul_right_eq K.index (relIndex_mul_index h)

Premises used: Subgroup.relIndex_mul_index, dvd_of_mul_right_eq, Subgroup.index
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hKL : K ≤ L
⊢ (H.subgroupOf L).relIndex (K.subgroupOf L) = H.relIndex K

Tactic:
((index_comap (H.subgroupOf L) (inclusion hKL)).trans (congr_arg _ (inclusion_range hKL))).symm

Premises used: Subgroup.subgroupOf, MonoidHom.mk', Set.Mem, Subgroup.subtype, setOf, Subgroup.relIndex, congr_arg, Subgroup.inclusion, Set.preimage, Subgroup.index_comap, Subgroup.inclusion_range, Eq.symm, Subgroup.comap, Eq.trans