awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)
head_eq : (x, b) = a
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
have H₁ : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
Tactic: injection H with _ H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq : (x, b) = a
H neg : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
have neg₁ : L2 ++ (x', b') :: (x', !b') :: L3 = L2 ++ (x', b') :: (x', !b') :: L3
Tactic: rw [r, H]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
⊢ List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [(x, b)]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
        (reduce L1) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
have cases : ∀ (x_1 : List (α × Bool)) (r : reduce L1 = x_1),
  List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [(x, b)]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
        x_1 =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
Tactic: cases r : reduce L1 with
    | nil =>
      dsimp; intro h
      exfalso
      have := congr_arg List.length h
      grind
    | cons hd tail =>
      obtain ⟨y, c⟩ := hd
      dsimp only
      split_ifs with h <;> intro H
      · rw [H] at r
        exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
      rcases L2 with (_ | ⟨a, L2⟩)
      · injections; subst_vars
        simp at h
      · refine @reduce.not _ L1 L2 L3 x' b' ?_
        rw [List.cons_append] at H
        injection H with _ H
        rw [r, H]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
b c : List (α × Bool)
h : Relation.ReflTransGen Red.Step (reduce L₁) b
H1 : Red.Step b c
H2 : reduce L₁ = b
⊢ reduce L₁ = c
have tail : ∀ {L₁_1 L₂ : List (α × Bool)} {x : α} {b : Bool},
  Relation.ReflTransGen Red.Step (reduce L₁) (L₁_1 ++ (x, b) :: (x, !b) :: L₂) →
    ∀ (H2 : reduce L₁ = L₁_1 ++ (x, b) :: (x, !b) :: L₂), reduce L₁ = L₁_1 ++ L₂
Tactic: obtain ⟨L4, L5, x, b⟩ := H1
Cleared hypotheses: b, c, h, H1, H2
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : Red (reduce L₁) L₂
⊢ reduce L₁ = L₂
have refl : reduce L₁ = reduce L₁
Tactic: induction H with
  | refl => rfl
  | tail _ H1 H2 =>
    obtain ⟨L4, L5, x, b⟩ := H1
    exact reduce.not H2
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : Red (reduce L₁) L₂
refl : reduce L₁ = reduce L₁
⊢ reduce L₁ = L₂
have tail : ∀ {b c : List (α × Bool)},
  Relation.ReflTransGen Red.Step (reduce L₁) b → ∀ (H1 : Red.Step b c) (H2 : reduce L₁ = b), reduce L₁ = c
Tactic: induction H with
  | refl => rfl
  | tail _ H1 H2 =>
    obtain ⟨L4, L5, x, b⟩ := H1
    exact reduce.not H2
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ (x * y).toWord = reduce (x.toWord ++ y.toWord)
have rw : (mk x.toWord * mk y.toWord).toWord = reduce ((mk x.toWord).toWord ++ (mk y.toWord).toWord)
Tactic: rw [← mk_toWord (x := x), ← mk_toWord (x := y)]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (x ^ n).toWord = reduce (List.replicate n x.toWord).flatten
have rw : (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten
Tactic: rw [← mk_toWord (x := x)]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).toWord = List.replicate n (a, true)
have rw : Quot.lift (r := Red.Step) reduce sorry (mk (List.replicate n (a, true))) = List.replicate n (a, true)
Tactic: rw [of, pow_mk, List.flatten_replicate_singleton, toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
⊢ reduce (invRev w) = invRev (reduce w)
have H : Red (reduce (invRev w)) (invRev (reduce w))
Tactic: apply reduce.min
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
⊢ Red (reduce (invRev w)) (invRev (reduce w))
have H : Red (invRev (reduce (invRev w))) (reduce w)
Tactic: rw [← red_invRev_iff, invRev_invRev]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)
have H : Red w (invRev (reduce (invRev w)))
Tactic: apply Red.reduce_left
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
⊢ Red w (invRev (reduce (invRev w)))
have this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
Tactic: have : Red (invRev (invRev w)) (invRev (reduce (invRev w))) := reduce.red.invRev
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))
have H : ∀ (this : Red w (invRev (reduce (invRev w)))), Red w (invRev (reduce (invRev w)))
Tactic: rwa [invRev_invRev] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
⊢ x⁻¹.toWord = invRev x.toWord
have mk : ∀ (L : List (α × Bool)), toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
Tactic: rcases x with ⟨L⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
have mk : (mk L)⁻¹.toWord = invRev (mk L).toWord
Tactic: rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
mk : (FreeGroup.mk L)⁻¹.toWord = invRev (FreeGroup.mk L).toWord
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
have mk₁ : (FreeGroup.mk (invRev L)).toWord = invRev (FreeGroup.mk L).toWord
Tactic: rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
mk : (FreeGroup.mk L)⁻¹.toWord = invRev (FreeGroup.mk L).toWord
mk₁ : (FreeGroup.mk (invRev L)).toWord = invRev (FreeGroup.mk L).toWord
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
have mk₂ : reduce (invRev L) = invRev (FreeGroup.mk L).toWord
Tactic: rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
mk : (FreeGroup.mk L)⁻¹.toWord = invRev (FreeGroup.mk L).toWord
mk₁ : (FreeGroup.mk (invRev L)).toWord = invRev (FreeGroup.mk L).toWord
mk₂ : reduce (invRev L) = invRev (FreeGroup.mk L).toWord
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
have mk₃ : reduce (invRev L) = invRev (reduce L)
Tactic: rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
mk : (FreeGroup.mk L)⁻¹.toWord = invRev (FreeGroup.mk L).toWord
mk₁ : (FreeGroup.mk (invRev L)).toWord = invRev (FreeGroup.mk L).toWord
mk₂ : reduce (invRev L) = invRev (FreeGroup.mk L).toWord
mk₃ : reduce (invRev L) = invRev (reduce L)
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
have mk₄ : invRev (reduce L) = invRev (reduce L)
Tactic: rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)
have rw : reduce (reduce L₁ ++ reduce L₂) = (mk (L₁ ++ L₂)).toWord
Tactic: rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
rw : reduce (reduce L₁ ++ reduce L₂) = (mk (L₁ ++ L₂)).toWord
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)
have rw₁ : reduce (reduce L₁ ++ reduce L₂) = (mk L₁ * mk L₂).toWord
Tactic: rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
rw : reduce (reduce L₁ ++ reduce L₂) = (mk (L₁ ++ L₂)).toWord
rw₁ : reduce (reduce L₁ ++ reduce L₂) = (mk L₁ * mk L₂).toWord
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)
have rw₂ : reduce (reduce L₁ ++ reduce L₂) = reduce ((mk L₁).toWord ++ (mk L₂).toWord)
Tactic: rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
rw : reduce (reduce L₁ ++ reduce L₂) = (mk (L₁ ++ L₂)).toWord
rw₁ : reduce (reduce L₁ ++ reduce L₂) = (mk L₁ * mk L₂).toWord
rw₂ : reduce (reduce L₁ ++ reduce L₂) = reduce ((mk L₁).toWord ++ (mk L₂).toWord)
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)
have rw₃ : reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ (mk L₂).toWord)
Tactic: rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
rw : reduce (reduce L₁ ++ reduce L₂) = (mk (L₁ ++ L₂)).toWord
rw₁ : reduce (reduce L₁ ++ reduce L₂) = (mk L₁ * mk L₂).toWord
rw₂ : reduce (reduce L₁ ++ reduce L₂) = reduce ((mk L₁).toWord ++ (mk L₂).toWord)
rw₃ : reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ (mk L₂).toWord)
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)
have rw₄ : reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ reduce L₂)
Tactic: rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ (x * y).toWord <+ x.toWord ++ y.toWord
have refine : Red (x.toWord ++ y.toWord) (x * y).toWord
Tactic: refine Red.sublist ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ x * y = mk (x.toWord ++ y.toWord)
have rw : x * y = mk x.toWord * mk y.toWord
Tactic: rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
rw : x * y = mk x.toWord * mk y.toWord
⊢ x * y = mk (x.toWord ++ y.toWord)
have rw₁ : x * y = x * mk y.toWord
Tactic: rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
rw : x * y = mk x.toWord * mk y.toWord
rw₁ : x * y = x * mk y.toWord
⊢ x * y = mk (x.toWord ++ y.toWord)
have rw₂ : x * y = x * y
Tactic: rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord
have this : x * y = mk (x.toWord ++ y.toWord)
Tactic: have : x * y = FreeGroup.mk (x.toWord ++ y.toWord) := by
    rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord
have rw : Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
⊢ reduce L = L
have rw : Red L (reduce L)
Tactic: rw [← h.red_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : reduce L = L
⊢ IsReduced L
have rw : ∀ ⦃a b : α × Bool⦄ ⦃l₁ l₂ : List (α × Bool)⦄, L = l₁ ++ a :: b :: l₂ → a.1 = b.1 → a.2 = b.2
Tactic: rw [IsReduced, List.isChain_iff_forall_rel_of_append_cons_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ (x₁, x₂).2 = ((x₁, x₂).1, y₂).2
have rw : ((x₁, x₂).1, y₂).2 ≠ !(x₁, x₂).2
Tactic: rw [eq_comm, ← Bool.ne_not]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ (x * y).norm = (mk (x.toWord ++ y.toWord)).norm
have rw : (x * y).norm = (mk x.toWord * mk y.toWord).norm
Tactic: rw [← mul_mk, mk_toWord, mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
rw : (x * y).norm = (mk x.toWord * mk y.toWord).norm
⊢ (x * y).norm = (mk (x.toWord ++ y.toWord)).norm
have rw₁ : (x * y).norm = (x * mk y.toWord).norm
Tactic: rw [← mul_mk, mk_toWord, mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
rw : (x * y).norm = (mk x.toWord * mk y.toWord).norm
rw₁ : (x * y).norm = (x * mk y.toWord).norm
⊢ (x * y).norm = (mk (x.toWord ++ y.toWord)).norm
have rw₂ : (x * y).norm = (x * y).norm
Tactic: rw [← mul_mk, mk_toWord, mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).norm = n
have rw : (of a ^ n).toWord.length = n
Tactic: rw [norm, toWord_of_pow, List.length_replicate]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
rw : (of a ^ n).toWord.length = n
⊢ (of a ^ n).norm = n
have rw₁ : (List.replicate n (a, true)).length = n
Tactic: rw [norm, toWord_of_pow, List.length_replicate]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
rw : (of a ^ n).toWord.length = n
rw₁ : (List.replicate n (a, true)).length = n
⊢ (of a ^ n).norm = n
have rw₂ : n = n
Tactic: rw [norm, toWord_of_pow, List.length_replicate]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Nonempty α
⊢ Function.Surjective.{u_1 + 1, 1} (α := FreeGroup α) norm
have let : ∀ (a : α), Function.Surjective.{u_1 + 1, 1} (α := FreeGroup α) norm
Tactic: let ⟨a⟩ := ‹Nonempty α›
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
⊢ Eq (α := G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) ↔
    Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)
have this : I.goursatFst.Normal
Tactic: have := normal_goursatFst hI₁
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this : I.goursatFst.Normal
⊢ Eq (α := G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) ↔
    Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)
have this₁ : I.goursatSnd.Normal
Tactic: have := normal_goursatSnd hI₂
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ Eq (α := G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) ↔
    Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)
have rw : Eq (α := G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) ↔
  Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ Eq (α := G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) ↔
    Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)
have simp : (y.1 / x.1, 1) ∈ I ↔ (1, x.2 / y.2) ∈ I
Tactic: simp only [QuotientGroup.eq_iff_div_mem, mem_goursatFst, mem_goursatSnd]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ (y.1 / x.1, 1) ∈ I ↔ (1, x.2 / y.2) ∈ I
have mp : (y.1 / x.1, 1) ∈ I → (1, x.2 / y.2) ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
mp : (y.1 / x.1, 1) ∈ I → (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I ↔ (1, x.2 / y.2) ∈ I
have mpr : (1, x.2 / y.2) ∈ I → (y.1 / x.1, 1) ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
⊢ have this := ⋯;
  have this_1 := ⋯;
  ∃ (e : MulEquiv.{u_1, u_2} (G ⧸ I.goursatFst) (H ⧸ I.goursatSnd)),
    ((MonoidHom.prodMap (QuotientGroup.mk' I.goursatFst) (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph
have this : I.goursatFst.Normal
Tactic: have := normal_goursatFst hI₁
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
this : I.goursatFst.Normal
⊢ have this := ⋯;
  have this_1 := ⋯;
  ∃ (e : MulEquiv.{u_1, u_2} (G ⧸ I.goursatFst) (H ⧸ I.goursatSnd)),
    ((MonoidHom.prodMap (QuotientGroup.mk' I.goursatFst) (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph
have this₁ : I.goursatSnd.Normal
Tactic: have := normal_goursatSnd hI₂
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
⊢ Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
have simp : Eq.{u_1 + 1} (α := Subgroup ↥G') (map (MonoidHom.fst ↥G' ↥H') (P.prod Q).range) ⊤
Tactic: simp only [← MonoidHom.coe_fst, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
⊢ Eq.{u_1 + 1} (α := Subgroup ↥G') (map (MonoidHom.fst ↥G' ↥H') (P.prod Q).range) ⊤
have simp : Surjective (α := ↥I) (β := ↥G') (⇑P : (a : ↥I) → ↥G')
Tactic: simp only [← MonoidHom.range_comp, MonoidHom.fst_comp_prod, MonoidHom.range_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
⊢ ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup ↥G') (N : Subgroup ↥H') (x : M.Normal) (x_1 : N.Normal) (e :
    MulEquiv.{u_1, u_2} (↥G' ⧸ M) (↥H' ⧸ N)),
    I =
      map (G'.subtype.prodMap H'.subtype)
        (comap (MonoidHom.prodMap (QuotientGroup.mk' M) (QuotientGroup.mk' N)) e.toMonoidHom.graph)
have hI₁' : Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
Tactic: have hI₁' : Surjective (Prod.fst ∘ I'.subtype) := by
    simp only [← MonoidHom.coe_fst, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']
    simp only [← MonoidHom.range_comp, MonoidHom.fst_comp_prod, MonoidHom.range_eq_top]
    exact (MonoidHom.fst ..).subgroupMap_surjective I