awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (span R t) x
⊢ Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)

Tactic:
(span S t).smul_mem k (span_le_restrictScalars R S t hx)

Premises used: iInf, Set.Mem, Set.iInter, setOf, Submodule.span_le_restrictScalars, Submodule.span, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (span R t) x
⊢ Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)

Tactic:
exact (span S t).smul_mem k (span_le_restrictScalars R S t hx)

Premises used: Submodule.span_le_restrictScalars, Submodule.span, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
a : Set R
⊢ Eq (α := Submodule R S) (span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) (map (Algebra.linearMap R S) (span R a))

Tactic:
(Submodule.span_image <| Algebra.linearMap R S).trans rfl

Premises used: Algebra.linearMap, Submodule.span_image, rfl, Eq.trans
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
T : Type u_2
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
a : Set S
⊢ Eq (α := Submodule R T) (span R ((⇑(algebraMap S T) : (a : S) → T) '' a))
    (map
      ((↑R :
          {S M : Type u_1} →
            {M₂ : Type u_2} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Algebra.linearMap S T))
      (span R a))

Tactic:
(Submodule.span_image <| (Algebra.linearMap S T).restrictScalars R).trans rfl

Premises used: LinearMap.restrictScalars, Algebra.linearMap, Submodule.span_image, rfl, Eq.trans
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
T : Type u_2
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
x : S
a : Set S
hx : Membership.mem (γ := Submodule R S) (span R a) x
rw :
  ∃ (y : S),
    Membership.mem (γ := Submodule R S) (span R a) y ∧
      Eq.{u_2 + 1} (α := T)
        (((↑R :
                  {S M : Type u_1} →
                    {M₂ : Type u_2} →
                      [inst : Semiring R] →
                        [inst_7 : Semiring S] →
                          [inst_8 : AddCommMonoid M] →
                            [inst_9 : AddCommMonoid M₂] →
                              [inst_10 : Module R M] →
                                [inst_11 : Module R M₂] →
                                  [inst_12 : Module S M] →
                                    [inst_13 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (Algebra.linearMap S T) :
              (a : S) → T)
            y :
          T)
        ((algebraMap S T : (a : S) → T) x : T)
⊢ Membership.mem.{u_2, u_2} (α := T) (γ := Submodule R T) (span R ((⇑(algebraMap S T) : (a : S) → T) '' a))
    ((algebraMap S T : (a : S) → T) x : T)

Tactic:
rw [span_algebraMap_image_of_tower, mem_map]

Premises used: Submodule.mem_map, Submodule.span_algebraMap_image_of_tower
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
T : Type u_2
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
x : S
a : Set S
hx : Membership.mem (γ := Submodule R S) (span R a) x
⊢ ∃ (y : S),
    Membership.mem (γ := Submodule R S) (span R a) y ∧
      Eq.{u_2 + 1} (α := T)
        (((↑R :
                  {S M : Type u_1} →
                    {M₂ : Type u_2} →
                      [inst : Semiring R] →
                        [inst_7 : Semiring S] →
                          [inst_8 : AddCommMonoid M] →
                            [inst_9 : AddCommMonoid M₂] →
                              [inst_10 : Module R M] →
                                [inst_11 : Module R M₂] →
                                  [inst_12 : Module S M] →
                                    [inst_13 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (Algebra.linearMap S T) :
              (a : S) → T)
            y :
          T)
        ((algebraMap S T : (a : S) → T) x : T)

Tactic:
⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
T : Type u_2
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
x : S
a : Set S
hx : Membership.mem (γ := Submodule R S) (span R a) x
⊢ ∃ (y : S),
    Membership.mem (γ := Submodule R S) (span R a) y ∧
      Eq.{u_2 + 1} (α := T)
        (((↑R :
                  {S M : Type u_1} →
                    {M₂ : Type u_2} →
                      [inst : Semiring R] →
                        [inst_7 : Semiring S] →
                          [inst_8 : AddCommMonoid M] →
                            [inst_9 : AddCommMonoid M₂] →
                              [inst_10 : Module R M] →
                                [inst_11 : Module R M₂] →
                                  [inst_12 : Module S M] →
                                    [inst_13 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (Algebra.linearMap S T) :
              (a : S) → T)
            y :
          T)
        ((algebraMap S T : (a : S) → T) x : T)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : IsDomain A
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : Module B M
inst_10 : IsScalarTower R A M
inst_11 : IsScalarTower R B M
inst_12 : SMulCommClass A B M
inst_13 : Module.IsTorsionFree A M
x : A
hx : x ≠ 0
⊢ Function.Injective.{v₁ + 1, v₁ + 1} (α := M) (β := M)
    (⇑((lsmul R B M : (a : A) → Module.End B M) x : Module.End B M) : (a : M) → M)

Tactic:
smul_right_injective M hx

Premises used: smul_right_injective
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
M : Submonoid R
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
⊢ Eq (α := Submonoid B) (algebraMapSubmonoid B (algebraMapSubmonoid A M)) (algebraMapSubmonoid B M)

Tactic:
algebraMapSubmonoid_map_eq _ (IsScalarTower.toAlgHom R A B)

Premises used: IsScalarTower.toAlgHom, Algebra.algebraMapSubmonoid_map_eq, Submonoid.map, Algebra.algebraMapSubmonoid
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
this_1 : Semiring α := e.semiring
this : SMul R α := Equiv.smul R e
r : R
x : α
⊢ Eq.{u_2 + 1} (α := α)
    ((e.symm : (a : β) → α)
        (HMul.hMul (α := β) (β := β)
          ((e : (a : α) → β) ((e.symm : (a : β) → α) ((algebraMap R β : (a : R) → β) r : β) : α) : β)
          ((e : (a : α) → β) x : β)) :
      α)
    ((e.symm : (a : β) → α)
        (HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β)
          ((e : (a : α) → β) ((e.symm : (a : β) → α) ((algebraMap R β : (a : R) → β) r : β) : α) : β)) :
      α)

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
this_1 : Semiring α := e.semiring
this : SMul R α := Equiv.smul R e
r : R
x : α
⊢ Eq.{u_2 + 1} (α := α) ((e.symm : (a : β) → α) (HSMul.hSMul (β := β) r ((e : (a : α) → β) x : β)) : α)
    ((e.symm : (a : β) → α)
        (HMul.hMul (α := β) (β := β)
          ((e : (a : α) → β) ((e.symm : (a : β) → α) ((algebraMap R β : (a : R) → β) r : β) : α) : β)
          ((e : (a : α) → β) x : β)) :
      α)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
r : R
⊢ Eq.{u_2 + 1} (α := α) ((algebraMap R α : (a : R) → α) r : α)
    ((e.symm : (a : β) → α) ((algebraMap R β : (a : R) → β) r : β) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
semiring : Semiring α := e.semiring
algebra : Algebra R α := Equiv.algebra R e
⊢ Type (max u_3 u_2)

Tactic:
exact α ≃ₐ[R] β
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
semiring : Semiring α := e.semiring
algebra : Algebra R α := Equiv.algebra R e
r : R
a :
  Eq.{u_2 + 1} (α := α)
    ((e.symm : (a : β) → α) ((RingEquiv.toEquiv e.ringEquiv).toFun ((algebraMap R α : (a : R) → α) r)) : α)
    ((e.symm : (a : β) → α) ((algebraMap R β : (a : R) → β) r : β) : α)
⊢ (RingEquiv.toEquiv e.ringEquiv).toFun ((algebraMap R α : (a : R) → α) r) = (algebraMap R β : (a : R) → β) r

Tactic:
apply e.symm.injective

Premises used: Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
semiring : Semiring α := e.semiring
algebra : Algebra R α := Equiv.algebra R e
r : R
⊢ Eq.{u_2 + 1} (α := α)
    ((e.symm : (a : β) → α) ((RingEquiv.toEquiv e.ringEquiv).toFun ((algebraMap R α : (a : R) → α) r)) : α)
    ((e.symm : (a : β) → α) ((algebraMap R β : (a : R) → β) r : β) : α)

Tactic:
simp only [RingEquiv.toEquiv_eq_coe, toFun_as_coe, EquivLike.coe_coe, ringEquiv_apply,
          symm_apply_apply, algebraMap_def]

Premises used: Equiv.symm_apply_apply, Equiv.toFun_as_coe, RingEquiv.toEquiv_eq_coe, Equiv.algebraMap_def, Equiv.ringEquiv_apply, EquivLike.coe_coe
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
semiring : Semiring α := e.semiring
algebra : Algebra R α := Equiv.algebra R e
⊢ α ≃ₐ[R] β

Tactic:
exact
    { Equiv.ringEquiv e with
      commutes' := fun r => by
        apply e.symm.injective
        simp only [RingEquiv.toEquiv_eq_coe, toFun_as_coe, EquivLike.coe_coe, ringEquiv_apply,
          symm_apply_apply, algebraMap_def] }

Premises used: Equiv.ringEquiv
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((algEquiv R e : (a : α) → β) a : β) ((e : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
b : β
this_1 : Semiring α := e.semiring
this : Algebra R α := Equiv.algebra R e
⊢ Prop

Tactic:
exact (algEquiv R e).symm b = e.symm b

Premises used: AlgEquiv.symm, Equiv.algEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
b : β
⊢ Eq.{u_2 + 1} (α := α) ((AlgEquiv.symm (algEquiv R e) : (a : β) → α) b : α) ((e.symm : (a : β) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
x : Unitization R A
⊢ mk x.toProd = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
x : R × A
⊢ (mk x).toProd = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
⊢ Function.Injective (α := Unitization R A) toProd

Tactic:
equiv.injective

Premises used: Unitization.equiv, Equiv.injective
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
⊢ Function.Surjective (α := Unitization R A) toProd

Tactic:
equiv.surjective

Premises used: Unitization.equiv, Equiv.surjective
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
⊢ Function.Bijective (α := Unitization R A) toProd

Tactic:
equiv.bijective

Premises used: Equiv.bijective, Unitization.equiv
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
⊢ Function.Injective (α := R × A) mk

Tactic:
equiv.symm.injective

Premises used: Unitization.equiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
⊢ Function.Surjective (α := R × A) mk

Tactic:
equiv.symm.surjective

Premises used: Unitization.equiv, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
⊢ Function.Bijective (α := R × A) mk

Tactic:
equiv.symm.bijective

Premises used: Equiv.bijective, Unitization.equiv, Equiv.symm
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
x y : Unitization R A
⊢ x.toProd = y.toProd ↔ x = y

Tactic:
toProd_injective.eq_iff

Premises used: Function.Injective.eq_iff, Unitization.toProd_injective
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero A
r : R
⊢ (toProd (inl r)).1 = r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero A
r : R
⊢ Eq.{u_2 + 1} (α := A) (toProd (inl r)).2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero R
a : A
⊢ Eq.{u_1 + 1} (α := R) (toProd (↑a : Unitization R A)).1 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero R
a : A
⊢ (toProd (↑a : Unitization R A)).2 = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero A
⊢ Function.Injective (α := R) (β := Unitization R A) inl

Tactic:
Function.LeftInverse.injective (g := Prod.fst ∘ toProd) <| fst_inl _

Premises used: Function.LeftInverse.injective, Unitization.fst_inl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero R
⊢ Function.Injective (α := A) (β := Unitization R A) inr

Tactic:
Function.LeftInverse.injective (g := Prod.snd ∘ toProd) <| snd_inr _

Premises used: Function.LeftInverse.injective, Unitization.snd_inr
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero R
x y : A
⊢ Eq (α := Unitization R A) (↑x : Unitization R A) (↑y : Unitization R A) ↔ x = y

Tactic:
inr_injective.eq_iff

Premises used: Function.Injective.eq_iff, Unitization.inr_injective
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Zero A
x y : R
⊢ Eq (α := Unitization R A) (inl x) (inl y) ↔ x = y

Tactic:
inl_injective.eq_iff

Premises used: Unitization.inl_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A_1 : Type u_2
𝕜 : Type u_3
A : Type u_4
inst : Nontrivial 𝕜
inst_1 : Nonempty A
⊢ Nontrivial (Unitization 𝕜 A)

Tactic:
equiv.nontrivial

Premises used: Equiv.nontrivial, Unitization.equiv
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A_1 : Type u_2
𝕜 : Type u_3
A : Type u_4
inst : Nonempty 𝕜
inst_1 : Nontrivial A
⊢ Nontrivial (Unitization 𝕜 A)

Tactic:
equiv.nontrivial

Premises used: Equiv.nontrivial, Unitization.equiv
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Zero R
inst_1 : Zero A
⊢ Eq (α := R × A) (toProd 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Add R
inst_1 : Add A
x₁ x₂ : Unitization R A
⊢ (x₁ + x₂).toProd = x₁.toProd + x₂.toProd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Neg R
inst_1 : Neg A
x : Unitization R A
⊢ (-x).toProd = -x.toProd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
inst : SMul S R
inst_1 : SMul S A
s : S
x : Unitization R A
⊢ (s • x).toProd = s • x.toProd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
T : Type u_1
S : Type u_2
R : Type u_3
A : Type u_4
inst : SMul T R
inst_1 : SMul T A
inst_2 : SMul S R
inst_3 : SMul S A
inst_4 : SMul T S
inst_5 : IsScalarTower T S R
inst_6 : IsScalarTower T S A
⊢ IsScalarTower T S (Unitization R A)

Tactic:
equiv.isScalarTower T S

Premises used: Unitization.equiv, Equiv.isScalarTower
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
T : Type u_1
S : Type u_2
R : Type u_3
A : Type u_4
inst : SMul T R
inst_1 : SMul T A
inst_2 : SMul S R
inst_3 : SMul S A
inst_4 : SMulCommClass T S R
inst_5 : SMulCommClass T S A
⊢ SMulCommClass T S (Unitization R A)

Tactic:
equiv.smulCommClass T S

Premises used: Unitization.equiv, Equiv.smulCommClass
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
T : Type u_1
S : Type u_2
R : Type u_3
A : Type u_4
inst : SMul S R
inst_1 : SMul S A
inst_2 : SMul.{u_2, u_3} Sᵐᵒᵖ R
inst_3 : SMul.{u_2, u_4} Sᵐᵒᵖ A
inst_4 : IsCentralScalar S R
inst_5 : IsCentralScalar S A
⊢ IsCentralScalar S (Unitization R A)

Tactic:
equiv.isCentralScalar S

Premises used: Unitization.equiv, Equiv.isCentralScalar
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Add R
inst_1 : Add A
⊢ AddEquiv.toEquiv (addEquiv R A) = equiv

Tactic:
rfl

Premises used: Unitization.equiv, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid A
inst_3 : Module S R
inst_4 : Module S A
⊢ Eq (α := Unitization R A ≃+ R × A) (LinearEquiv.toAddEquiv (linearEquiv S R A)) (addEquiv R A)

Tactic:
rfl

Premises used: Unitization.addEquiv, Unitization.equiv, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Zero R
inst_1 : Zero A
⊢ Eq.{u_3 + 1} (α := R) (toProd 0).1 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Zero R
inst_1 : Zero A
⊢ Eq.{u_4 + 1} (α := A) (toProd 0).2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Add R
inst_1 : Add A
x₁ x₂ : Unitization R A
⊢ (x₁ + x₂).toProd.1 = x₁.toProd.1 + x₂.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Add R
inst_1 : Add A
x₁ x₂ : Unitization R A
⊢ (x₁ + x₂).toProd.2 = x₁.toProd.2 + x₂.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Neg R
inst_1 : Neg A
x : Unitization R A
⊢ (-x).toProd.1 = -x.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Neg R
inst_1 : Neg A
x : Unitization R A
⊢ (-x).toProd.2 = -x.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
inst : SMul S R
inst_1 : SMul S A
s : S
x : Unitization R A
⊢ (s • x).toProd.1 = s • x.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
inst : SMul S R
inst_1 : SMul S A
s : S
x : Unitization R A
⊢ (s • x).toProd.2 = s • x.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Zero R
inst_1 : Zero A
⊢ Eq (α := Unitization R A) (inl 0) 0

Tactic:
rfl

Premises used: Unitization.inl, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Add R
inst_1 : AddZeroClass A
r₁ r₂ : R
⊢ inl (r₁ + r₂) = HAdd.hAdd (α := Unitization R A) (inl r₁) (inl r₂)

Tactic:
Unitization.ext rfl (add_zero 0).symm

Premises used: Unitization.ext, add_zero, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Neg R
inst_1 : AddGroup A
r : R
⊢ Eq (α := Unitization R A) (inl (-r)) (-inl r)

Tactic:
Unitization.ext rfl neg_zero.symm

Premises used: Unitization.ext, Eq.symm, neg_zero, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : AddGroup R
inst_1 : AddGroup A
r₁ r₂ : R
⊢ inl (r₁ - r₂) = HSub.hSub (α := Unitization R A) (inl r₁) (inl r₂)

Tactic:
Unitization.ext rfl (sub_zero 0).symm

Premises used: sub_zero, Unitization.ext, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
inst : Zero A
inst_1 : SMul S R
inst_2 : SMulZeroClass S A
s : S
r : R
⊢ inl (s • r) = HSMul.hSMul (β := Unitization R A) s (inl r)

Tactic:
Unitization.ext rfl (smul_zero s).symm

Premises used: Unitization.ext, smul_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : Zero R
inst_1 : Zero A
⊢ Eq (α := Unitization R A) (↑0 : Unitization R A) 0

Tactic:
rfl

Premises used: Unitization.inr, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : AddZeroClass R
inst_1 : Add A
m₁ m₂ : A
⊢ (↑(m₁ + m₂) : Unitization R A) = HAdd.hAdd (α := Unitization R A) (↑m₁ : Unitization R A) (↑m₂ : Unitization R A)

Tactic:
Unitization.ext (add_zero 0).symm rfl

Premises used: Unitization.ext, add_zero, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : AddGroup R
inst_1 : Neg A
m : A
⊢ Eq (α := Unitization R A) (↑(-m) : Unitization R A) (-(↑m : Unitization R A))

Tactic:
Unitization.ext neg_zero.symm rfl

Premises used: Unitization.ext, Eq.symm, neg_zero, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : AddGroup R
inst_1 : AddGroup A
m₁ m₂ : A
⊢ (↑(m₁ - m₂) : Unitization R A) = HSub.hSub (α := Unitization R A) (↑m₁ : Unitization R A) (↑m₂ : Unitization R A)

Tactic:
Unitization.ext (sub_zero 0).symm rfl

Premises used: sub_zero, Unitization.ext, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
inst : Zero R
inst_1 : SMulZeroClass S R
inst_2 : SMul S A
r : S
m : A
⊢ (↑(r • m) : Unitization R A) = HSMul.hSMul (β := Unitization R A) r (↑m : Unitization R A)

Tactic:
Unitization.ext (smul_zero _).symm rfl

Premises used: Unitization.ext, smul_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_3
A : Type u_4
inst : AddZeroClass R
inst_1 : AddZeroClass A
x : Unitization R A
⊢ inl x.toProd.1 + (↑x.toProd.2 : Unitization R A) = x

Tactic:
Unitization.ext (add_zero x.fst) (zero_add x.snd)

Premises used: Unitization.ext, zero_add, Prod.fst, Unitization.toProd, add_zero, Prod.snd