awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
⊢ ∃ (f' : H →* I), mrange f = f'.mgraph
have obtain : ∀ (f' : H → I) (hf' : Set.range (ι := G) (⇑f : (a : G) → H × I) = graphOn f' univ),
  ∃ (f' : H →* I), mrange f = f'.mgraph
Tactic: obtain ⟨f', hf'⟩ := exists_range_eq_graphOn_univ hf₁ hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (hypothesis)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : Set.range (ι := G) (⇑f : (a : G) → H × I) = graphOn f' univ
⊢ ∃ (f' : H →* I), mrange f = f'.mgraph
have hf'₁ : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
Tactic: simp only [Set.ext_iff, Set.mem_range, mem_graphOn, mem_univ, true_and, Prod.forall] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y
have simp_rw : ∀ (x x_1 : G),
  f'
      (HMul.hMul (α := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x)
        (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x_1)) =
    f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x) *
      f' (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I) x_1)
Tactic: simp_rw [hf₁.forall]
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ (y : G), (f : (a : G) → H × I) y = (a, b)) ↔ f' a = b
⊢ ∃ (f' : H →* I), mrange f = f'.mgraph
have h : Eq (α := Submonoid (H × I)) (mrange f) (mgraph { toFun := f', map_one' := sorry, map_mul' := sorry })
Tactic: use
  { toFun := f'
    map_one' := (hf' _ _).1 ⟨1, map_one _⟩
    map_mul' := by
      simp_rw [hf₁.forall]
      rintro g₁ g₂
      exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩ }
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
⊢ ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph
have obtain : ∀ (e₁ : H →* I) (he₁ : mrange f = e₁.mgraph), ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph
Tactic: obtain ⟨e₁, he₁⟩ := f.exists_mrange_eq_mgraph hf₁ fun _ _ ↦ (hf _ _).1
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph
have obtain : ∀ (e₂ : I →* H) (he₂ : mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) = e₂.mgraph),
  ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph
Tactic: obtain ⟨e₂, he₂⟩ := (MulEquiv.prodComm.toMonoidHom.comp f).exists_mrange_eq_mgraph (by simpa) <|
    by simp [hf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) = e₂.mgraph
h : H
i : I
⊢ (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
have rw : ∀ (he₁ : ∀ (x : H × I), Membership.mem (γ := Submonoid (H × I)) (mrange f) x ↔ x ∈ e₁.mgraph) (e₂ : I →* H)
  (he₂ :
    ∀ (x : I × H),
      Membership.mem (γ := Submonoid (I × H))
          (mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f)) x ↔
        x ∈ e₂.mgraph)
  (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
Tactic: rw [SetLike.ext_iff] at he₁ he₂
Cleared hypotheses: he₁, e₂, he₂, h, i
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (hypothesis)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) = e₂.mgraph
⊢ ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph
have he₁₂ : ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
Tactic: have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [SetLike.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
h : H
⊢ (e₂ : (a : I) → H) ((e₁ : (a : H) → I) h : I) = h
have rw : Eq.{u_3 + 1} (α := I) ((e₁ : (a : H) → I) h : I) ((e₁ : (a : H) → I) h : I)
Tactic: rw [← he₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Graph (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Monoid G
inst_1 : Monoid H
inst_2 : Monoid I
f : G →* H × I
hf₁ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_3 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (F := G →* I × H) (comp (MulEquiv.toMonoidHom MulEquiv.prodComm) f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
i : I
⊢ (e₁ : (a : H) → I) ((e₂ : (a : I) → H) i : H) = i
have rw : Eq.{u_2 + 1} (α := H) ((e₂ : (a : I) → H) i : H) ((e₂ : (a : I) → H) i : H)
Tactic: rw [he₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
inst : DivisionCommMonoid α
⊢ Eq (α := α →* α) (MonoidHom.comp invMonoidHom invMonoidHom) (MonoidHom.id α)
have h : ∀ (x : α),
  Eq (α := α) ((MonoidHom.comp invMonoidHom invMonoidHom : (a : α) → α) x : α) ((MonoidHom.id α : (a : α) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : Mul M
inst_1 : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw : HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) (x * y) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : Mul M
inst_1 : CommSemigroup N
f g : M →ₙ* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
    HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : Mul M
inst_1 : CommSemigroup N
f g : M →ₙ* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
      HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₂ : HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) x : N))
    ((g : (a : M) → N) y : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : Mul M
inst_1 : CommSemigroup N
f g : M →ₙ* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
      HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₂ :
  HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
        ((g : (a : M) → N) x : N))
      ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₃ : HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) x : N))
    ((g : (a : M) → N) y : N) =
  HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
      ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : Mul M
inst_1 : CommSemigroup N
f g : M →ₙ* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
      HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₂ :
  HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
        ((g : (a : M) → N) x : N))
      ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₃ :
  HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
        ((g : (a : M) → N) x : N))
      ((g : (a : M) → N) y : N) =
    HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
        ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₄ : HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
      ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) y : N) =
  HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
      ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : Mul M
inst_1 : CommSemigroup N
inst_2 : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
have h : ∀ (x : M), Eq.{u_4 + 1} (α := P) ((g.comp (f₁ * f₂) : (a : M) → P) x : P) ((g.comp f₁ * g.comp f₂ : (a : M) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
F : Type u_7
G : Type u_8
H : Type u_9
inst : Group G
inst_1 : MulOneClass H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
h : ∀ (a : G), Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x y : G
hxy : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)
have rw : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y⁻¹ : H) = 1
Tactic: rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
F : Type u_7
G : Type u_8
H : Type u_9
inst : Group G
inst_1 : MulOneClass H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
h : ∀ (a : G), Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x y : G
hxy : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
rw : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y⁻¹ : H) = 1
⊢ Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)
have rw₁ : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) y : H) ((f : (a : G) → H) y⁻¹ : H) = 1
Tactic: rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
F : Type u_7
G : Type u_8
H : Type u_9
inst : Group G
inst_1 : MulOneClass H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
h : ∀ (a : G), Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x y : G
hxy : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
rw : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y⁻¹ : H) = 1
rw₁ : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) y : H) ((f : (a : G) → H) y⁻¹ : H) = 1
⊢ Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)
have rw₂ : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (y * y⁻¹) : H) (1 : H)
Tactic: rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
F : Type u_7
G : Type u_8
H : Type u_9
inst : Group G
inst_1 : MulOneClass H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
h : ∀ (a : G), Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x y : G
hxy : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
rw : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y⁻¹ : H) = 1
rw₁ : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) y : H) ((f : (a : G) → H) y⁻¹ : H) = 1
rw₂ : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (y * y⁻¹) : H) (1 : H)
⊢ Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)
have rw₃ : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) 1 : H) (1 : H)
Tactic: rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
F : Type u_7
G : Type u_8
H : Type u_9
inst : Group G
inst_1 : MulOneClass H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
h : ∀ (a : G), Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x y : G
hxy : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
rw : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y⁻¹ : H) = 1
rw₁ : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) y : H) ((f : (a : G) → H) y⁻¹ : H) = 1
rw₂ : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (y * y⁻¹) : H) (1 : H)
rw₃ : Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) 1 : H) (1 : H)
⊢ Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)
have rw₄ : Eq.{u_9 + 1} (α := H) 1 1
Tactic: rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H_1 : Type u_6
F : Type u_7
inst : Group G
H : Type u_8
inst_1 : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (HMul.hMul (α := G) 1 1⁻¹ * y⁻¹))⁻¹ = f x * f y
have simp : f x * (f 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y
Tactic: simp only [map_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H_1 : Type u_6
F : Type u_7
inst : Group G
H : Type u_8
inst_1 : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (HMul.hMul (α := G) 1 1⁻¹ * y⁻¹))⁻¹ = f x * f y
have simp : f x * (f 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y
Tactic: { simp only [map_div]
          simp only [mul_inv_cancel, one_mul, inv_inv] }
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : MulOneClass M
inst_1 : CommMonoid N
f g : M →* N
x y : M
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw : HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) (x * y) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]