awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 1 : A) ((g : (a : M) → A) 0 : A) = 1
have rw : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 1 : A) (0 : A) = 1
Tactic: rw [map_zero, map_one, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
rw : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 1 : A) (0 : A) = 1
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 1 : A) ((g : (a : M) → A) 0 : A) = 1
have rw₁ : HAdd.hAdd (α := A) 1 0 = 1
Tactic: rw [map_zero, map_one, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
rw : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 1 : A) (0 : A) = 1
rw₁ : HAdd.hAdd (α := A) 1 0 = 1
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 1 : A) ((g : (a : M) → A) 0 : A) = 1
have rw₂ : Eq.{u_2 + 1} (α := A) 1 1
Tactic: rw [map_zero, map_one, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) ((r₁ + 0) * (r₂ + 0)) : A)
      ((g : (a : M) → A) ((r₁ + 0) •> (0 + m₂) + (op r₂ + 0) •> (0 + m₁)) : A) =
    HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ + 0) : A) ((g : (a : M) → A) (0 + m₁) : A) *
      HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₂ + 0) : A) ((g : (a : M) → A) (0 + m₂) : A)
have simp : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
Tactic: simp only [add_zero, zero_add, add_mul, mul_add, hg]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((f : (a : R) → A) r₂ : A) +
        HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
have rw : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
Tactic: rw [← map_mul, map_add, add_comm (g _), add_assoc, hfg, hgf]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r₁ : R
m₁ : M
r₂ : R
m₂ : M
rw :
  HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((f : (a : R) → A) r₂ : A) +
        HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
have rw₁ : HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
    (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (r₁ •> m₂) : A) ((g : (a : M) → A) (m₁ <• r₂) : A)) =
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
Tactic: rw [← map_mul, map_add, add_comm (g _), add_assoc, hfg, hgf]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r₁ : R
m₁ : M
r₂ : R
m₂ : M
rw :
  HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
rw₁ :
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (r₁ •> m₂) : A) ((g : (a : M) → A) (m₁ <• r₂) : A)) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((f : (a : R) → A) r₂ : A) +
        HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
have rw₂ : HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
    (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (m₁ <• r₂) : A) ((g : (a : M) → A) (r₁ •> m₂) : A)) =
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
Tactic: rw [← map_mul, map_add, add_comm (g _), add_assoc, hfg, hgf]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r₁ : R
m₁ : M
r₂ : R
m₂ : M
rw :
  HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
rw₁ :
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (r₁ •> m₂) : A) ((g : (a : M) → A) (m₁ <• r₂) : A)) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
rw₂ :
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (m₁ <• r₂) : A) ((g : (a : M) → A) (r₁ •> m₂) : A)) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((f : (a : R) → A) r₂ : A) +
        HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
have rw₃ : HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
    (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (m₁ <• r₂) : A) ((g : (a : M) → A) (r₁ •> m₂) : A)) =
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
    (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A))
Tactic: rw [← map_mul, map_add, add_comm (g _), add_assoc, hfg, hgf]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
A : Type u_2
inst_10 : Semiring A
inst_11 : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r : R
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) 0 : A) = (f : (a : R) → A) r
have rw : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) r : A) (0 : A) = (f : (a : R) → A) r
Tactic: rw [map_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
A : Type u_2
inst_10 : Semiring A
inst_11 : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r : R
rw : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) r : A) (0 : A) = (f : (a : R) → A) r
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) 0 : A) = (f : (a : R) → A) r
have rw₁ : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r : A)
Tactic: rw [map_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
A : Type u_2
inst_10 : Semiring A
inst_11 : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
m : M
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 0 : A) ((g : (a : M) → A) m : A) = (g : (a : M) → A) m
have rw : HAdd.hAdd (α := A) (β := A) (0 : A) ((g : (a : M) → A) m : A) = (g : (a : M) → A) m
Tactic: rw [map_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
A : Type u_2
inst_10 : Semiring A
inst_11 : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
m : M
rw : HAdd.hAdd (α := A) (β := A) (0 : A) ((g : (a : M) → A) m : A) = (g : (a : M) → A) m
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 0 : A) ((g : (a : M) → A) m : A) = (g : (a : M) → A) m
have rw₁ : Eq.{u_2 + 1} (α := A) ((g : (a : M) → A) m : A) ((g : (a : M) → A) m : A)
Tactic: rw [map_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
⊢ Eq (α := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) ⊤
have refine : ∀ (x : tsze R M) (hx : Membership.mem (γ := Subalgebra S (tsze R M)) ⊤ x),
  Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) x
Tactic: refine top_unique fun x hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
x : tsze R M
⊢ Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) x
have rw : Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr))
  (inl x.fst + inr x.snd)
Tactic: rw [← x.inl_fst_add_inr_snd_eq]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
x : tsze R M
⊢ Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr))
    (inl x.fst + inr x.snd)
have refine_1 : Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr))
  (inl x.fst)
Tactic: refine add_mem ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
x : tsze R M
refine_1 :
  Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr))
    (inl x.fst)
⊢ Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr))
    (inl x.fst + inr x.snd)
have refine_2 : Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr))
  (inr x.snd)
Tactic: refine add_mem ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
A : Type u_2
inst_10 : Semiring A
inst_11 : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
⊢ AlgHom.range (lift f g hg hfg hgf) = f.range ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
have simp_rw : Subalgebra.map (lift f g hg hfg hgf) ⊤ =
  Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
Tactic: simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_range_inr, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, lift_comp_inlHom, ← Set.range_comp, Function.comp_def,
    lift_apply_inr, Algebra.map_top]