awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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))
⊢ 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) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
  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]
-- 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)
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))
simp_rw₁ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → 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) (AlgHom.range (inlAlgHom S R M)) ⊔
    Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
  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]
-- 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)
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))
simp_rw₁ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₂ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → 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) (AlgHom.range (inlAlgHom S R M)) ⊔
    Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
  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]
-- 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)
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))
simp_rw₁ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₂ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₃ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → 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₄ : (AlgHom.comp (lift f g hg hfg hgf) (inlAlgHom S R M)).range ⊔
    Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
  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]
-- 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)
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))
simp_rw₁ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₂ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₃ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₄ :
  (AlgHom.comp (lift f g hg hfg hgf) (inlAlgHom S R M)).range ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → 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₅ : f.range ⊔ Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
  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]
-- 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)
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))
simp_rw₁ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₂ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₃ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₄ :
  (AlgHom.comp (lift f g hg hfg hgf) (inlAlgHom S R M)).range ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₅ :
  f.range ⊔ Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → 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₆ : f.range ⊔
    Algebra.adjoin S
      (Set.range.{u_2, v + 1} (ι := M)
        (Function.comp (β := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) inr)) =
  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]
-- 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)
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))
simp_rw₁ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₂ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₃ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₄ :
  (AlgHom.comp (lift f g hg hfg hgf) (inlAlgHom S R M)).range ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₅ :
  f.range ⊔ Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₆ :
  f.range ⊔
      Algebra.adjoin S
        (Set.range.{u_2, v + 1} (ι := M)
          (Function.comp (β := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → 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₇ : f.range ⊔ Algebra.adjoin S (Set.range fun (x : M) ↦ (lift f g hg hfg hgf : (a : tsze R M) → A) (inr x)) =
  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]
-- 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 : M →ₗ[R'] A //
      ∀ (x y : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) = 0 } ≃
    (tsze R' M →ₐ[R'] A)
have refine : { f : M →ₗ[R'] A // ∀ (x y : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) = 0 } ≃
  { fg : (R' →ₐ[R'] A) × (M →ₗ[R'] A) //
    (∀ (x y : M), HMul.hMul (α := A) (β := A) ((fg.2 : (a : M) → A) x : A) ((fg.2 : (a : M) → A) y : A) = 0) ∧
      (∀ (r : R') (x : M),
          (fg.2 : (a : M) → A) (r •> x) =
            HMul.hMul (α := A) (β := A) ((fg.1 : (a : R') → A) r : A) ((fg.2 : (a : M) → A) x : A)) ∧
        ∀ (r : R') (x : M),
          (fg.2 : (a : M) → A) (x <• r) =
            HMul.hMul (α := A) (β := A) ((fg.2 : (a : M) → A) x : A) ((fg.1 : (a : R') → A) r : A) }
Tactic: refine Equiv.trans ?_ liftEquiv
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inl r) : tsze R' N) (inl r : tsze R' N)
have rw : Eq (α := tsze R' N)
  ((((liftEquivOfComm :
              (a :
                  { f : M →ₗ[R'] tsze R' N //
                    ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                tsze R' M →ₐ[R'] tsze R' N)
            (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
              ∀ (x y : M),
                HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                    ((f : (a : M) → tsze R' N) y : tsze R' N) =
                  0)
              (inrHom R' N ∘ₗ f) sorry) :
          tsze R' M →ₐ[R'] tsze R' N) :
        (a : tsze R' M) → tsze R' N)
      (inl r) :
    tsze R' N)
  (inl r : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inl r) : tsze R' N) (inl r : tsze R' N)
have rw₁ : Eq (α := tsze R' N)
  ((lift (Algebra.ofId R' (tsze R' N))
          (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) sorry) :
            M →ₗ[R'] tsze R' N)
          sorry sorry sorry :
        (a : tsze R' M) → tsze R' N)
      (inl r) :
    tsze R' N)
  (inl r : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inl r) : tsze R' N) (inl r : tsze R' N)
have rw₂ : Eq (α := tsze R' N) ((Algebra.ofId R' (tsze R' N) : (a : R') → tsze R' N) r : tsze R' N) (inl r : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]