awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
d : Transversal (G := G) φ
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
h : H
heq :
  Eq (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) : PushoutI (G := G) φ)
this :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
⊢ w = Word.empty (M := G)
have heq₁ : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h sorry) = w'.prod (G := G)
Tactic: rw [← hw'prod, ← this] at heq
Cleared hypotheses: heq, this
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
d : Transversal (G := G) φ
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
h : H
heq : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this_1 :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
this : w'.toWord (G := G) = Word.empty (M := G)
⊢ w = Word.empty (M := G)
have hw'map₁ : w.toList (M := G) = []
Tactic: simp [this, @eq_comm _ []] at hw'map
Cleared hypotheses: hw'map
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
d : Transversal (G := G) φ
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
h : H
heq : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this_1 :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
this : w'.toWord (G := G) = Word.empty (M := G)
hw'map : w.toList (M := G) = []
⊢ w = Word.empty (M := G)
have toList : ∀ (i : ℕ) (a : (i : ι) × G i),
  getElem? (valid := fun (as : List ((i : ι) × G i)) (i : ℕ) ↦ i < as.length) (w.toList (M := G)) i = some a ↔
    getElem? (valid := fun (as : List ((i : ι) × G i)) (i : ℕ) ↦ i < as.length)
        (Word.toList (M := G) (Word.empty (M := G))) i =
      some a
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
d : Transversal (G := G) φ
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
h : H
heq : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
⊢ w = Word.empty (M := G)
have suffices : w'.toWord (G := G) = Word.empty (M := G)
Tactic: suffices w'.toWord = .empty by
    simp [this, @eq_comm _ []] at hw'map
    ext
    simp [hw'map]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
d : Transversal (G := G) φ
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
h : H
heq : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
⊢ w'.toWord (G := G) = Word.empty (M := G)
have rw : Eq (α := Word G) (toWord (G := G) (φ := φ) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h sorry))
  (Word.empty (M := G))
Tactic: rw [← prod_injective heq]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
⊢ Membership.mem (γ := Subgroup (PushoutI (G := G) φ))
      (MonoidHom.range (of (G := G) i) ⊓ MonoidHom.range (of (G := G) j)) x →
    x ∈ (base (G := G) φ).range
have this : ∀ (g₁ : G i) (hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x) (g₂ : G j)
  (hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x), x ∈ (base (G := G) φ).range
Tactic: ⟨⟨g₁, hg₁⟩, ⟨g₂, hg₂⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
⊢ x ∈ (base (G := G) φ).range
have by_contra : ∀ (hx : ¬x ∈ (base (G := G) φ).range), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
⊢ False
have hx1 : x ≠ 1
Tactic: have hx1 : x ≠ 1 := by rintro rfl; simp_all only [ne_eq, one_mem, not_true_eq_false]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
⊢ False
have hg₁1 : g₁ ≠ 1
Tactic: have hg₁1 : g₁ ≠ 1 :=
        ne_of_apply_ne (of (φ := φ) i) (by simp_all)
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
⊢ False
have hg₂1 : g₂ ≠ 1
Tactic: have hg₂1 : g₂ ≠ 1 :=
        ne_of_apply_ne (of (φ := φ) j) (by simp_all)
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₂1 : g₂ ≠ 1
y : H
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) = x
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
⊢ False
have hg₃ : Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
  ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
Tactic: subst hg₁
Cleared hypotheses: x, hg₂, hx, hx1, hg₁
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₂1 : g₂ ≠ 1
y : H
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) = x
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
⊢ False
have hx₁ : ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
Tactic: subst hg₁
Cleared hypotheses: x, hg₂, hx, hx1, hg₁
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₂1 : g₂ ≠ 1
y : H
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) = x
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
hx₁ :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
⊢ False
have hx1₁ : Ne (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
  (1 : PushoutI (G := G) φ)
Tactic: subst hg₁
Cleared hypotheses: x, hg₂, hx, hx1, hg₁
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
⊢ False
have hg₁r : g₁ ∉ (φ i).range
Tactic: have hg₁r : g₁ ∉ (φ i).range := by
        rintro ⟨y, rfl⟩
        subst hg₁
        exact hx (of_apply_eq_base φ i y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) = x
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
⊢ False
have hg₃ : Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
  ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
Tactic: subst hg₂
Cleared hypotheses: x, hg₁, hx, hx1, hg₂
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) = x
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
⊢ False
have hx₁ : ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
Tactic: subst hg₂
Cleared hypotheses: x, hg₁, hx, hx1, hg₂
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) = x
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
hx₁ :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
⊢ False
have hx1₁ : Ne (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
  (1 : PushoutI (G := G) φ)
Tactic: subst hg₂
Cleared hypotheses: x, hg₁, hx, hx1, hg₂
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
⊢ False
have hg₂r : g₂ ∉ (φ j).range
Tactic: have hg₂r : g₂ ∉ (φ j).range := by
        rintro ⟨y, rfl⟩
        subst hg₂
        exact hx (of_apply_eq_base φ j y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := Word.mk (M := G) [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹] ⋯ ⋯
⊢ False
have hw : Reduced (G := G) φ w
Tactic: have hw : Reduced φ w := by
        simp only [w, Reduced, List.mem_cons,
          forall_eq_or_imp, not_false_eq_true,
          hg₁r, hg₂r, List.mem_nil_iff, false_imp_iff, imp_true_iff, and_true,
          inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := Word.mk (M := G) [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹] ⋯ ⋯
hw : Reduced (G := G) φ w
⊢ False
have this : w = Word.empty (M := G)
Tactic: have := hw.eq_empty_of_mem_range hφ (by
        simp only [w, Word.prod, List.map_cons, List.prod_cons, List.prod_nil,
          List.map_nil, map_mul, ofCoprodI_of, hg₁, hg₂, map_inv, mul_one,
          mul_inv_cancel, one_mem])
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
⊢ (base (G := G) φ).range ≤ MonoidHom.range (of (G := G) i)
have rw : LE.le (α := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (G := H) (MonoidHom.comp (of (G := G) i) (φ i)))
  (MonoidHom.range (of (G := G) i))
Tactic: rw [← of_comp_eq_base i]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
⊢ (base (G := G) φ).range ≤ MonoidHom.range (of (G := G) j)
have rw : LE.le (α := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (G := H) (MonoidHom.comp (of (G := G) j) (φ j)))
  (MonoidHom.range (of (G := G) j))
Tactic: rw [← of_comp_eq_base j]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
⊢ N = ⊤
have h₁ : ∀ (x : G), x ∈ N ↔ Membership.mem (γ := Subgroup G) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
⊢ N = ⊤
have h₁ : ∀ (x : G), x ∈ N ↔ Membership.mem (γ := Subgroup G) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : (leftRel N : G → G → Prop) a b
hcd : (leftRel N : G → G → Prop) c d
⊢ (leftRel N : G → G → Prop) (a * c) (b * d)
have rw : ∀ (hab : a⁻¹ * b ∈ N) (hcd : c⁻¹ * d ∈ N), (fun (x y : G) ↦ x⁻¹ * y ∈ N) (a * c) (b * d)
Tactic: rw [leftRel_eq] at hab hcd ⊢
Cleared hypotheses: hab, hcd
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (a * c)⁻¹ * (b * d) ∈ N
have N₁ : c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) = (a * c)⁻¹ * (b * d)
Tactic: calc
      c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
      _ = (a * c)⁻¹ * (b * d) := by
        simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
⊢ QuotientGroup.con f.ker = Con.ker f
have H : ∀ (x y : G), (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
x y : G
⊢ (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
have H : ({ toSetoid := leftRel f.ker, mul' := sorry } : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
Tactic: rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
x y : G
H : ({ toSetoid := leftRel f.ker, mul' := ⋯ } : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
⊢ (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
have H₁ : (leftRel f.ker : G → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
Tactic: rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
x y : G
H : ({ toSetoid := leftRel f.ker, mul' := ⋯ } : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₁ : (leftRel f.ker : G → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
⊢ (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
have H₂ : (leftRel f.ker : G → G → Prop) y x ↔ (Con.ker f : (a : G) → G → Prop) x y
Tactic: rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
x y : G
H : ({ toSetoid := leftRel f.ker, mul' := ⋯ } : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₁ : (leftRel f.ker : G → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₂ : (leftRel f.ker : G → G → Prop) y x ↔ (Con.ker f : (a : G) → G → Prop) x y
⊢ (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
have H₃ : y⁻¹ * x ∈ f.ker ↔ (Con.ker f : (a : G) → G → Prop) x y
Tactic: rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]