awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Graph
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

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])
-- Module: Mathlib.Algebra.Group.Graph
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
rw rw₁ : Eq.{u_3 + 1} (α := I) ((e₁ : (a : H) → I) h : I) ((e₁ : (a : H) → I) h : I)
⊢ (e₂ : (a : I) → H) ((e₁ : (a : H) → I) h : I) = h

Tactic:
rw [← he₁₂]
-- Module: Mathlib.Algebra.Group.Graph
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
rw rw₁ : Eq.{u_2 + 1} (α := H) ((e₂ : (a : I) → H) i : H) ((e₂ : (a : I) → H) i : H)
⊢ (e₁ : (a : H) → I) ((e₂ : (a : I) → H) i : H) = i

Tactic:
rw [he₁₂]
-- Module: Mathlib.Algebra.Group.Graph
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
⊢ ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph

Tactic:
exact ⟨
  { toFun := e₁
    map_mul' := e₁.map_mul'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩
-- Module: Mathlib.Algebra.Group.Graph
Goal:
H : Type u_2
I : Type u_3
inst : Monoid H
inst_1 : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (α := ↥G) (β := H) (comp (β := H × I) Prod.fst (⇑G.subtype : (a : ↥G) → H × I))
⊢ ∃ (f : H →* I), G = f.mgraph

Tactic:
simpa using MonoidHom.exists_mrange_eq_mgraph hG₁.surjective
    fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hG₁.injective h)

Premises used: Function.comp, Function.Bijective.injective, congr_arg, Function.Bijective.surjective, Submonoid.subtype, MonoidHom.exists_mrange_eq_mgraph, Prod.snd, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Graph
Goal:
H : Type u_2
I : Type u_3
inst : Monoid H
inst_1 : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (α := ↥G) (β := H) (comp (β := H × I) Prod.fst (⇑G.subtype : (a : ↥G) → H × I))
hG₂ : Bijective (α := ↥G) (β := I) (comp (β := H × I) Prod.snd (⇑G.subtype : (a : ↥G) → H × I))
⊢ ∃ (e : H ≃* I), G = e.toMonoidHom.mgraph

Tactic:
simpa using MonoidHom.exists_mulEquiv_mrange_eq_mgraph hG₁.surjective hG₂.surjective
    fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, Function.Bijective.injective, Function.Bijective.surjective, Iff.trans, Iff.symm, MonoidHom.exists_mulEquiv_mrange_eq_mgraph
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : Group I
f : G →* H
x : G × H
⊢ x ∈ f.mgraph.carrier → x⁻¹ ∈ f.mgraph.carrier

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
x : G × H
⊢ x ∈ f.graph ↔ (f : (a : G) → H) x.1 = x.2

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
⊢ f.graph = (MonoidHom.prod (id G) f).range

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : Group 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), f.range = f'.graph

Tactic:
simpa [SetLike.ext_iff] using exists_mrange_eq_mgraph hf₁ hf

Premises used: SetLike.ext_iff, MonoidHom.exists_mrange_eq_mgraph
-- Module: Mathlib.Algebra.Group.Graph
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : Group 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), f.range = e.toMonoidHom.graph

Tactic:
simpa [SetLike.ext_iff] using exists_mulEquiv_mrange_eq_mgraph hf₁ hf₂ hf

Premises used: SetLike.ext_iff, MonoidHom.exists_mulEquiv_mrange_eq_mgraph
-- Module: Mathlib.Algebra.Group.Graph
Goal:
H : Type u_2
I : Type u_3
inst : Group H
inst_1 : Group I
G : Subgroup (H × I)
hG₁ : Bijective (α := ↥G) (β := H) (comp (β := H × I) Prod.fst (⇑G.subtype : (a : ↥G) → H × I))
⊢ ∃ (f : H →* I), G = f.graph

Tactic:
simpa [SetLike.ext_iff] using Submonoid.exists_eq_mgraph hG₁

Premises used: Submonoid.exists_eq_mgraph, SetLike.ext_iff
-- Module: Mathlib.Algebra.Group.Graph
Goal:
H : Type u_2
I : Type u_3
inst : Group H
inst_1 : Group I
G : Subgroup (H × I)
hG₁ : Bijective (α := ↥G) (β := H) (comp (β := H × I) Prod.fst (⇑G.subtype : (a : ↥G) → H × I))
hG₂ : Bijective (α := ↥G) (β := I) (comp (β := H × I) Prod.snd (⇑G.subtype : (a : ↥G) → H × I))
⊢ ∃ (e : H ≃* I), G = e.toMonoidHom.graph

Tactic:
simpa [SetLike.ext_iff] using Submonoid.exists_mulEquiv_eq_mgraph hG₁ hG₂

Premises used: SetLike.ext_iff, Submonoid.exists_mulEquiv_eq_mgraph
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
⊢ Eq.{u_1 + 1} (α := (a : α) → α) (⇑invMonoidHom : (a : α) → α) Inv.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a : α
⊢ (invMonoidHom : (a : α) → α) a = a⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
h :
  ∀ (x : α),
    Eq (α := α) ((MonoidHom.comp invMonoidHom invMonoidHom : (a : α) → α) x : α) ((MonoidHom.id α : (a : α) → α) x : α)
⊢ Eq (α := α →* α) (MonoidHom.comp invMonoidHom invMonoidHom) (MonoidHom.id α)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
x : α
⊢ Eq (α := α) ((MonoidHom.comp invMonoidHom invMonoidHom : (a : α) → α) x : α) ((MonoidHom.id α : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
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 : One M
inst_1 : MulOneClass N
f g : OneHom M N
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 1 : N) ((g : (a : M) → N) 1 : N) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_8
N : Type u_9
inst : One M
inst_1 : MulOneClass N
f g : OneHom M N
⊢ (⇑(f * g) : (a : M) → N) = HMul.hMul (α := (a : M) → N) (⇑f : (a : M) → N) (⇑g : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_8
N : Type u_9
inst : One M
inst_1 : MulOneClass N
f g : OneHom M N
x : M
⊢ (f * g : (a : M) → N) x = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : One M
inst_1 : One N
inst_2 : MulOneClass P
g₁ g₂ : OneHom N P
f : OneHom M N
⊢ (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
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 : One M
inst_1 : InvOneClass N
f : OneHom M N
⊢ Eq.{u_3 + 1} (α := N) (((f : (a : M) → N) 1)⁻¹ : N) (1 : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_8
N : Type u_9
inst : One M
inst_1 : InvOneClass N
f : OneHom M N
⊢ Eq (α := (a : M) → N) (⇑f⁻¹ : (a : M) → N) (⇑f : (a : M) → N)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_8
N : Type u_9
inst : One M
inst_1 : InvOneClass N
f : OneHom M N
x : M
⊢ Eq.{u_9 + 1} (α := N) ((f⁻¹ : (a : M) → N) x : N) (((f : (a : M) → N) x)⁻¹ : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : One M
inst_1 : One N
inst_2 : InvOneClass P
g : OneHom N P
f : OneHom M N
⊢ g⁻¹.comp f = (g.comp f)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
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 : One M
inst_1 : DivisionMonoid N
f g : OneHom M N
⊢ HDiv.hDiv (α := N) (β := N) ((f : (a : M) → N) 1 : N) ((g : (a : M) → N) 1 : N) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_8
N : Type u_9
inst : One M
inst_1 : DivisionMonoid N
f g : OneHom M N
⊢ (⇑(f / g) : (a : M) → N) = HDiv.hDiv (α := (a : M) → N) (⇑f : (a : M) → N) (⇑g : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_8
N : Type u_9
inst : One M
inst_1 : DivisionMonoid N
f g : OneHom M N
x : M
⊢ (f / g : (a : M) → N) x = HDiv.hDiv (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : One M
inst_1 : One N
inst_2 : DivisionMonoid P
g₁ g₂ : OneHom N P
f : OneHom M N
⊢ (g₁ / g₂).comp f = g₁.comp f / g₂.comp f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
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)
rw₄ 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)
⊢ 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)

Tactic:
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]

Premises used: mul_assoc, mul_right_comm, MulHom.map_mul, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_8
N : Type u_9
inst : Mul M
inst_1 : CommSemigroup N
f g : M →ₙ* N
x : M
⊢ (f * g : (a : M) → N) x = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : CommSemigroup P
g₁ g₂ : N →ₙ* P
f : M →ₙ* N
⊢ (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
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)
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
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:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
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)
rw₄ rw₅ : Eq.{u_9 + 1} (α := H) 1 1
⊢ Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)

Tactic:
rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]

Premises used: map_mul, map_one, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
⊢ Function.Injective.{u_8 + 1, u_9 + 1} (α := G) (β := H) (⇑f : (a : G) → H) ↔
    ∀ (a : G), Eq.{u_9 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) ↔ a = 1

Tactic:
(injective_iff_map_eq_one f).trans <|
    forall_congr' fun _ => ⟨fun h => ⟨h, fun H => H.symm ▸ map_one f⟩, Iff.mp⟩

Premises used: Eq.rec, map_one, Iff.intro, Iff.mp, forall_congr', Iff.trans, Eq.symm, injective_iff_map_eq_one
-- Module: Mathlib.Algebra.Group.Hom.Basic
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 * y) = f x * (f (HMul.hMul (α := G) 1 1⁻¹ * y⁻¹))⁻¹

Tactic:
simp only [one_mul, inv_one, ← map_div, inv_inv]

Premises used: inv_one, inv_inv, one_mul
-- Module: Mathlib.Algebra.Group.Hom.Basic
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 * y) = f x * (f (HMul.hMul (α := G) 1 1⁻¹ * y⁻¹))⁻¹

Tactic:
{ simp only [one_mul, inv_one, ← map_div, inv_inv] }

Premises used: inv_one, inv_inv, one_mul
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
simp : f x * (f 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y
⊢ f x * (f (HMul.hMul (α := G) 1 1⁻¹ * y⁻¹))⁻¹ = f x * f y

Tactic:
simp only [map_div]
-- Module: Mathlib.Algebra.Group.Hom.Basic
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 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y

Tactic:
simp only [mul_inv_cancel, one_mul, inv_inv]

Premises used: inv_inv, mul_inv_cancel, one_mul
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
simp : f x * (f 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y
⊢ f x * (f (HMul.hMul (α := G) 1 1⁻¹ * y⁻¹))⁻¹ = f x * f y

Tactic:
{ simp only [map_div]
          simp only [mul_inv_cancel, one_mul, inv_inv] }

Premises used: inv_inv, mul_inv_cancel, one_mul
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
G : Type u_5
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)⁻¹
⊢ (⇑(ofMapMulInv f map_div) : (a : G) → H) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
simpa only [div_eq_mul_inv] using hf

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
G : Type u_5
inst : Group G
H : Type u_8
inst_1 : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ (⇑(ofMapDiv f hf) : (a : G) → H) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) 1 : N) ((g : (a : M) → N) 1 : N) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
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
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)
rw₄ 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)
⊢ 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)

Tactic:
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]

Premises used: mul_assoc, mul_right_comm, DFunLike.coe, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
inst : MulOneClass M
inst_1 : CommMonoid N
f g : M →* N
x : M
⊢ (f * g : (a : M) → N) x = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : MulOneClass P
g₁ g₂ : M →* N
f : P →* M
⊢ (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
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)
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
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:
simp