awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ∀ (x : A), Eq.{w + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)
⊢ f = g

Tactic:
coe_injective <| funext h

Premises used: funext, NonUnitalAlgHom.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : f = g
x : A
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)

Tactic:
h ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A → B
h₁ : ∀ (m : R) (x : A), f (m • x) = HSMul.hSMul.{u₁, w, w} (α := S) ((φ : (a : R) → S) m : S) (f x)
h₂ : { toFun := f, map_smul' := h₁ : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := f, map_smul' := h₁ : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := f, map_smul' := h₁ : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun x +
        { toFun := f, map_smul' := h₁ : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun (x * y) =
      { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun x *
        { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun y
⊢ (⇑{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₛₙₐ[φ] B } : (a : A) → B) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ :
  ∀ (m : R) (x : A),
    (f : (a : A) → B) (m • x) =
      HSMul.hSMul.{u₁, w, w} (α := S) (β := B) ((φ : (a : R) → S) m : S) ((f : (a : A) → B) x : B)
h₂ :
  { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
          MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
      0 =
    0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
            MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          x +
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          y
h₄ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun y
⊢ { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₛₙₐ[φ] B } = f

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
⊢ Eq (α := A →ₙ+ B) { toFun := (⇑f : (a : A) → B), map_add' := ⋯ } (↑f : A →ₙ+ B)

Tactic:
rfl

Premises used: AddHomClass.toAddHom, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
⊢ f.toDistribMulActionHom = (↑f : A →ₑ+[φ] B)

Tactic:
rfl

Premises used: DistribMulActionSemiHomClass.toDistribMulActionHom, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
⊢ f.toMulHom = (↑f : A →ₙ* B)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₑ+[φ] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₙ* B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₑ+[φ] B) (↑f : A →ₑ+[φ] B) (↑g : A →ₑ+[φ] B)
h₁ : ∀ (a : A), Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₑ+[φ] B) (↑f : A →ₑ+[φ] B) (↑g : A →ₑ+[φ] B)
a : A
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
DistribMulActionHom.congr_fun h a

Premises used: DistribMulActionHom.congr_fun
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₑ+[φ] B) (↑f : A →ₑ+[φ] B) (↑g : A →ₑ+[φ] B)
a : A
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
exact DistribMulActionHom.congr_fun h a

Premises used: DistribMulActionHom.congr_fun
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₙ* B) (↑f : A →ₙ* B) (↑g : A →ₙ* B)
h₁ : ∀ (a : A), Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₙ* B) (↑f : A →ₙ* B) (↑g : A →ₙ* B)
a : A
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
DFunLike.congr_fun h a

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₙ* B) (↑f : A →ₙ* B) (↑g : A →ₙ* B)
a : A
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
exact DFunLike.congr_fun h a

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ :
  ∀ (m : R) (x : A),
    (f : (a : A) → B) (m • x) =
      HSMul.hSMul.{u₁, w, w} (α := S) (β := B) ((φ : (a : R) → S) m : S) ((f : (a : A) → B) x : B)
h₂ :
  { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
          MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
      0 =
    0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
            MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          x +
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          y
h₄ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun y
⊢ (↑{ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₛₙₐ[φ] B } :
      A →ₑ+[φ] B) =
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ :
  ∀ (m : R) (x : A),
    (f : (a : A) → B) (m • x) =
      HSMul.hSMul.{u₁, w, w} (α := S) (β := B) ((φ : (a : R) → S) m : S) ((f : (a : A) → B) x : B)
h₂ :
  { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
          MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
      0 =
    0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
            MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          x +
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          y
h₄ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₑ+[φ] B }.toFun y
⊢ (↑{ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₛₙₐ[φ] B } :
      A →ₙ* B) =
    { toFun := (⇑f : (a : A) → B), map_mul' := h₄ : A →ₙ* B }

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
c : R
x : A
⊢ (f : (a : A) → B) (c • x) =
    HSMul.hSMul.{u₁, w, w} (α := S) (β := B) ((φ : (a : R) → S) c : S) ((f : (a : A) → B) x : B)

Tactic:
map_smulₛₗ _ _ _

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
x y : A
⊢ (f : (a : A) → B) (x + y) = HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)

Tactic:
map_add _ _ _

Premises used: map_add
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
x y : A
⊢ (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)

Tactic:
map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f : A →ₛₙₐ[φ] B
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
⊢ Eq (α := (a : A) → A) (⇑(NonUnitalAlgHom.id R A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
⊢ ∀ (x y : A),
    MulActionHom.toFun.{u, u₁, v, w} (M := R) (N := S) (φ := (⇑φ : (a : R) → S)) (DistribMulActionHom.toMulActionHom 0)
        (x * y) =
      HMul.hMul (α := B)
        (MulActionHom.toFun.{u, u₁, v, w} (M := R) (N := S) (φ := (⇑φ : (a : R) → S))
          (DistribMulActionHom.toMulActionHom 0) x)
        (MulActionHom.toFun.{u, u₁, v, w} (M := R) (N := S) (φ := (⇑φ : (a : R) → S))
          (DistribMulActionHom.toMulActionHom 0) y)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
⊢ Eq (α := (a : A) → B) (⇑0 : (a : A) → B) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
⊢ Eq.{v + 1} (α := (a : A) → A) (⇑1 : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
a : A
⊢ Eq.{w + 1} (α := B) ((0 : (a : A) → B) a : B) (0 : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
a : A
⊢ (1 : (a : A) → A) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
ψ : S →* T
χ : R →* T
f : B →ₛₙₐ[ψ] C
g : A →ₛₙₐ[φ] B
inst_9 : φ.CompTriple ψ χ
⊢ Eq (α := (a : A) → C) (⇑(f.comp g) : (a : A) → C)
    (Function.comp.{v + 1, w + 1, w₁ + 1} (β := B) (⇑f : (a : B) → C) (⇑g : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
ψ : S →* T
χ : R →* T
f : B →ₛₙₐ[ψ] C
g : A →ₛₙₐ[φ] B
inst_9 : φ.CompTriple ψ χ
x : A
⊢ Eq.{w₁ + 1} (α := C) ((f.comp g : (a : A) → C) x : C) ((f : (a : B) → C) ((g : (a : A) → B) x : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
B₁ : Type u_2
inst_3 : NonUnitalNonAssocSemiring B₁
inst_4 : DistribMulAction R B₁
f : A →ₙₐ[R] B₁
g : B₁ → A
h₁ : Function.LeftInverse g (⇑f : (a : A) → B₁)
h₂ : Function.RightInverse g (⇑f : (a : A) → B₁)
⊢ (⇑(f.inverse g h₁ h₂) : (a : B₁) → A) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
simp : g 0 = 0
⊢ MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) 0 = 0

Tactic:
simp only [MulHom.toFun_eq_coe, MulHom.inverse_apply]

Premises used: MulHom.inverse_apply, MulHom.toFun_eq_coe
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
rw : g ((f : (a : A) → B) 0) = 0
rw₁ rw₂ : Eq.{v + 1} (α := A) 0 0
⊢ g 0 = 0

Tactic:
rw [← f.map_zero, h₁]

Premises used: NonUnitalAlgHom.map_zero
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
simp : g (x + y) = g x + g y
⊢ MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) (x + y) =
    MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) x + MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) y

Tactic:
simp only [MulHom.toFun_eq_coe, MulHom.inverse_apply]

Premises used: MulHom.inverse_apply, MulHom.toFun_eq_coe
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
rw : g (HAdd.hAdd (α := B) ((f : (a : A) → B) (g x) : B) y) = g ((f : (a : A) → B) (g x)) + g y
rw₁ :
  g (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) (g x) : B) ((f : (a : A) → B) (g y) : B)) =
    g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₂ : g ((f : (a : A) → B) (g x + g y)) = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₃ : g x + g y = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₄ : g x + g y = g x + g ((f : (a : A) → B) (g y))
rw₅ rw₆ : g x + g y = g x + g y
⊢ g (x + y) = g x + g y

Tactic:
rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂]

Premises used: map_add
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
φ' : S →* R
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
⊢ (⇑(f.inverse' g k h₁ h₂) : (a : B) → A) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
inst_11 : DistribMulAction R B
inst_12 : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
c : R
x : A
⊢ Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) (c • x) =
    HSMul.hSMul (α := R) (β := B × C) ((MonoidHom.id R : (a : R) → R) c : R)
      (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) x : B × C)

Tactic:
simp only [Function.prod_apply, map_smul, MonoidHom.id_apply, Prod.smul_mk]

Premises used: MonoidHom.id_apply, Function.prod_apply, Prod.smul_mk, map_smul