awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 g : tsze R M →ₐ[S] A
hinl : f.comp (inlAlgHom S R M) = g.comp (inlAlgHom S R M)
hinr :
  Eq (α := M →ₗ[S] A)
    (f.toLinearMap ∘ₗ
      (↑S :
          {S_1 : Type u} →
            {M : Type v} →
              {M₂ : Type (max u v)} →
                [inst : Semiring S] →
                  [inst_12 : Semiring S_1] →
                    [inst_13 : AddCommMonoid M] →
                      [inst_14 : AddCommMonoid M₂] →
                        [inst_15 : Module S M] →
                          [inst_16 : Module S M₂] →
                            [inst_17 : Module S_1 M] →
                              [inst_18 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (inrHom R M))
    (g.toLinearMap ∘ₗ
      (↑S :
          {S_1 : Type u} →
            {M : Type v} →
              {M₂ : Type (max u v)} →
                [inst : Semiring S] →
                  [inst_12 : Semiring S_1] →
                    [inst_13 : AddCommMonoid M] →
                      [inst_14 : AddCommMonoid M₂] →
                        [inst_15 : Module S M] →
                          [inst_16 : Module S M₂] →
                            [inst_17 : Module S_1 M] →
                              [inst_18 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (inrHom R M))
⊢ f = g

Tactic:
AlgHom.toLinearMap_injective <|
    linearMap_ext (AlgHom.congr_fun hinl) (LinearMap.congr_fun hinr)

Premises used: TrivSqZeroExt.linearMap_ext, AlgHom.toLinearMap_injective, LinearMap.congr_fun, AlgHom.congr_fun
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := A) 1 1
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 1 : A) ((g : (a : M) → A) 0 : A) = 1

Tactic:
rw [map_zero, map_one, add_zero]

Premises used: map_zero, map_one, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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)
⊢ 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)

Tactic:
simp only [add_zero, zero_add, add_mul, mul_add, hg]

Premises used: add_mul, zero_add, mul_add, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)
x : tsze R M
⊢ (lift f g hg hfg hgf : (a : tsze R M) → A) x =
    HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) x.fst : A) ((g : (a : M) → A) x.snd : A)

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r : A)
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) 0 : A) = (f : (a : R) → A) r

Tactic:
rw [map_zero, add_zero]

Premises used: map_zero, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) ((g : (a : M) → A) m : A) ((g : (a : M) → A) m : A)
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) 0 : A) ((g : (a : M) → A) m : A) = (g : (a : M) → A) m

Tactic:
rw [map_zero, zero_add]

Premises used: map_zero, zero_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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.comp (lift f g hg hfg hgf) (inlAlgHom S R M) = f

Tactic:
AlgHom.ext <| lift_apply_inl f g hg hfg hgf

Premises used: AlgHom.ext, TrivSqZeroExt.lift_apply_inl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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.toLinearMap (lift f g hg hfg hgf) ∘ₗ
      (↑S :
          {S_1 : Type u} →
            {M : Type v} →
              {M₂ : Type (max u v)} →
                [inst : Semiring S] →
                  [inst_12 : Semiring S_1] →
                    [inst_13 : AddCommMonoid M] →
                      [inst_14 : AddCommMonoid M₂] →
                        [inst_15 : Module S M] →
                          [inst_16 : Module S M₂] →
                            [inst_17 : Module S_1 M] →
                              [inst_18 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (inrHom R M) =
    g

Tactic:
LinearMap.ext <| lift_apply_inr f g hg hfg hgf

Premises used: LinearMap.ext, TrivSqZeroExt.lift_apply_inr
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 (α := tsze R M →ₐ[S] tsze R M)
    (lift (inlAlgHom S R M)
      ((↑S :
          {S_1 : Type u} →
            {M : Type v} →
              {M₂ : Type (max u v)} →
                [inst : Semiring S] →
                  [inst_10 : Semiring S_1] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module S M] →
                          [inst_14 : Module S M₂] →
                            [inst_15 : Module S_1 M] →
                              [inst_16 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (inrHom R M))
      ⋯ ⋯ ⋯)
    (AlgHom.id S (tsze R M))

Tactic:
algHom_ext' (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)

Premises used: TrivSqZeroExt.lift_comp_inrHom, TrivSqZeroExt.lift_comp_inlHom, TrivSqZeroExt.algHom_ext'
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)) ⊤

Tactic:
top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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
⊢ Eq (α := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) ⊤

Tactic:
refine top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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)
⊢ Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) x

Tactic:
rw [← x.inl_fst_add_inr_snd_eq]

Premises used: TrivSqZeroExt.inl_fst_add_inr_snd_eq
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)

Tactic:
add_mem ?_ ?_

Premises used: Set.Mem, AddMemClass.add_mem
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)
refine_2 :
  Membership.mem (γ := Subalgebra S (tsze R M)) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr))
    (inr x.snd)
⊢ 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:
refine add_mem ?_ ?_

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)

Tactic:
le_sup_left (α := Subalgebra S _) <| Set.mem_range_self x.fst

Premises used: Set.mem_range_self, le_sup_left, TrivSqZeroExt.fst
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)

Tactic:
exact le_sup_left (α := Subalgebra S _) <| Set.mem_range_self x.fst

Premises used: Set.mem_range_self, le_sup_left, TrivSqZeroExt.fst
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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))
    (inr x.snd)

Tactic:
le_sup_right (α := Subalgebra S _) <| Algebra.subset_adjoin <| Set.mem_range_self x.snd

Premises used: Set.mem_range_self, TrivSqZeroExt.snd, Algebra.subset_adjoin, le_sup_right
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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))
    (inr x.snd)

Tactic:
exact le_sup_right (α := Subalgebra S _) <| Algebra.subset_adjoin <| Set.mem_range_self x.snd

Premises used: Set.mem_range_self, TrivSqZeroExt.snd, Algebra.subset_adjoin, le_sup_right
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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) }
⊢ { 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)

Tactic:
refine Equiv.trans ?_ liftEquiv

Premises used: Equiv.trans, TrivSqZeroExt.liftEquiv
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 :
  { f : M →ₗ[R'] A // ∀ (x y : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) = 0 }
r : R'
x : M
⊢ ((Algebra.ofId R' A, (↑f : M →ₗ[R'] A)).2 : (a : M) → A) (r •> x) =
    HMul.hMul (α := A) (β := A) (((Algebra.ofId R' A, (↑f : M →ₗ[R'] A)).1 : (a : R') → A) r : A)
      (((Algebra.ofId R' A, (↑f : M →ₗ[R'] A)).2 : (a : M) → A) x : A)

Tactic:
simp [Algebra.smul_def, Algebra.ofId_apply]

Premises used: Algebra.ofId_apply, Algebra.smul_def
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 :
  { f : M →ₗ[R'] A // ∀ (x y : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) = 0 }
r : R'
x : M
⊢ ((Algebra.ofId R' A, (↑f : M →ₗ[R'] A)).2 : (a : M) → A) (x <• r) =
    HMul.hMul (α := A) (β := A) (((Algebra.ofId R' A, (↑f : M →ₗ[R'] A)).2 : (a : M) → A) x : A)
      (((Algebra.ofId R' A, (↑f : M →ₗ[R'] A)).1 : (a : R') → A) r : A)

Tactic:
simp [Algebra.smul_def, Algebra.ofId_apply, Algebra.commutes]

Premises used: Algebra.ofId_apply, Algebra.smul_def, Algebra.commutes
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 } ≃
    { 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:
exact {
    toFun := fun f => ⟨(Algebra.ofId _ _, f.val), f.prop,
      fun r x => by simp [Algebra.smul_def, Algebra.ofId_apply],
      fun r x => by simp [Algebra.smul_def, Algebra.ofId_apply, Algebra.commutes]⟩
    invFun := fun fg => ⟨fg.val.2, fg.prop.1⟩ }