awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
R_1 : Type u_1
inst_1 : CommRing R_1
I_1 : Ideal R_1
inst_2 : CharP.{u_1} (R_1 ⧸ I_1) p_1
inst_3 : IsAdicComplete I_1 R_1
p : ℕ
inst_4 : Fact (Nat.Prime p)
R : Type u_2
inst_5 : CommRing R
I : Ideal R
inst_6 : CharP.{u_2} (R ⧸ I) p
inst_7 : IsAdicComplete I R
h :
  ∀ (x : Perfection R p),
    Eq (α := R)
      ((((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) :
                  (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
                (MonoidHom.comp (N := Perfection (R ⧸ I) p)
                  ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
                      (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
                    (teichmuller p I))
                  (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I))) :
              Perfection R p →* R) :
            (a : Perfection R p) → R)
          x :
        R)
      ((((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) :
                  (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
                (MonoidHom.id (Perfection R p)) :
              Perfection R p →* R) :
            (a : Perfection R p) → R)
          x :
        R)
⊢ Eq (α := Perfection R p →* R)
    ((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) : (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
        (MonoidHom.comp (N := Perfection (R ⧸ I) p)
          ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
              (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
            (teichmuller p I))
          (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I))) :
      Perfection R p →* R)
    ((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) : (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
        (MonoidHom.id (Perfection R p)) :
      Perfection R p →* R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
R_1 : Type u_1
inst_1 : CommRing R_1
I_1 : Ideal R_1
inst_2 : CharP.{u_1} (R_1 ⧸ I_1) p_1
inst_3 : IsAdicComplete I_1 R_1
p : ℕ
inst_4 : Fact (Nat.Prime p)
R : Type u_2
inst_5 : CommRing R
I : Ideal R
inst_6 : CharP.{u_2} (R ⧸ I) p
inst_7 : IsAdicComplete I R
x : Perfection R p
⊢ Eq (α := R)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) :
                (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
              (MonoidHom.comp (N := Perfection (R ⧸ I) p)
                ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
                    (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
                  (teichmuller p I))
                (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I))) :
            Perfection R p →* R) :
          (a : Perfection R p) → R)
        x :
      R)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) :
                (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
              (MonoidHom.id (Perfection R p)) :
            Perfection R p →* R) :
          (a : Perfection R p) → R)
        x :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
R_1 : Type u_1
inst_1 : CommRing R_1
I_1 : Ideal R_1
inst_2 : CharP.{u_1} (R_1 ⧸ I_1) p_1
inst_3 : IsAdicComplete I_1 R_1
p : ℕ
inst_4 : Fact (Nat.Prime p)
R : Type u_2
inst_5 : CommRing R
I : Ideal R
inst_6 : CharP.{u_2} (R ⧸ I) p
inst_7 : IsAdicComplete I R
h :
  ∀ (x : Perfection (R ⧸ I) p),
    Eq (α := R ⧸ I)
      ((((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
                  (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
                (MonoidHom.comp (N := Perfection R p)
                  (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I) : Perfection R p →* Perfection (R ⧸ I) p)
                  ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
                      (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
                    (teichmuller p I))) :
              Perfection (R ⧸ I) p →* R ⧸ I) :
            (a : Perfection (R ⧸ I) p) → R ⧸ I)
          x :
        R ⧸ I)
      ((((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
                  (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
                (MonoidHom.id (Perfection (R ⧸ I) p)) :
              Perfection (R ⧸ I) p →* R ⧸ I) :
            (a : Perfection (R ⧸ I) p) → R ⧸ I)
          x :
        R ⧸ I)
⊢ Eq (α := Perfection (R ⧸ I) p →* R ⧸ I)
    ((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
          (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
        (MonoidHom.comp (N := Perfection R p)
          (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I) : Perfection R p →* Perfection (R ⧸ I) p)
          ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
              (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
            (teichmuller p I))) :
      Perfection (R ⧸ I) p →* R ⧸ I)
    ((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
          (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
        (MonoidHom.id (Perfection (R ⧸ I) p)) :
      Perfection (R ⧸ I) p →* R ⧸ I)

Tactic:
ext
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
R_1 : Type u_1
inst_1 : CommRing R_1
I_1 : Ideal R_1
inst_2 : CharP.{u_1} (R_1 ⧸ I_1) p_1
inst_3 : IsAdicComplete I_1 R_1
p : ℕ
inst_4 : Fact (Nat.Prime p)
R : Type u_2
inst_5 : CommRing R
I : Ideal R
inst_6 : CharP.{u_2} (R ⧸ I) p
inst_7 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
⊢ Eq (α := R ⧸ I)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
                (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
              (MonoidHom.comp (N := Perfection R p)
                (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I) : Perfection R p →* Perfection (R ⧸ I) p)
                ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
                    (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
                  (teichmuller p I))) :
            Perfection (R ⧸ I) p →* R ⧸ I) :
          (a : Perfection (R ⧸ I) p) → R ⧸ I)
        x :
      R ⧸ I)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
                (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
              (MonoidHom.id (Perfection (R ⧸ I) p)) :
            Perfection (R ⧸ I) p →* R ⧸ I) :
          (a : Perfection (R ⧸ I) p) → R ⧸ I)
        x :
      R ⧸ I)

Tactic:
simp
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection R p
n : ℕ
⊢ Eq (α := R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I)
        ((quotientMulEquiv p I : (a : Perfection R p) → Perfection (R ⧸ I) p) x) :
      R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) ((coeffMonoidHom R p n : (a : Perfection R p) → R) x) : R ⧸ I)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
⊢ Eq (α := R)
    ((coeffMonoidHom R p 0 : (a : Perfection R p) → R)
        ((MulEquiv.symm (quotientMulEquiv p I) : (a : Perfection (R ⧸ I) p) → Perfection R p) x : Perfection R p) :
      R)
    ((teichmuller₀ p I : (a : Perfection (R ⧸ I) p) → R) x : R)

Tactic:
simp [quotientMulEquiv]

Premises used: Perfection.quotientMulEquiv
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A
y : M
⊢ (liftBaseChange A l : (a : A ⊗[R] M) → N) (x ⊗ₜ[R] y) = HSMul.hSMul (β := N) x ((l : (a : M) → N) y : N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
y : M
⊢ Eq.{u_3 + 1} (α := N) ((liftBaseChange A l : (a : A ⊗[R] M) → N) (1 ⊗ₜ[R] y) : N) ((l : (a : M) → N) y : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_4
M : Type u_2
N : Type u_3
A : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : A ⊗[R] M →ₗ[A] N
x : M
⊢ Eq.{u_3 + 1} (α := N)
    (((((LinearEquiv.symm (liftBaseChangeEquiv A) : (A ⊗[R] M →ₗ[A] N) ≃ₗ[A] M →ₗ[R] N) :
                (a : A ⊗[R] M →ₗ[A] N) → M →ₗ[R] N)
              l :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((l : (a : A ⊗[R] M) → N) (1 ⊗ₜ[R] x) : N)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
P : Type u_1
inst_9 : AddCommMonoid P
inst_10 : Module A P
inst_11 : Module R P
inst_12 : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
a :
  ∀ (x : M),
    Eq.{u_1 + 1} (α := P)
      ((((AlgebraTensorModule.curry (l' ∘ₗ liftBaseChange A l) : A →ₗ[A] M →ₗ[R] P) : (a : A) → M →ₗ[R] P) 1 :
            (a : M) → P)
          x :
        P)
      ((((AlgebraTensorModule.curry
                    (liftBaseChange A
                      ((↑R :
                            {S : Type u_2} →
                              {M : Type u_5} →
                                {M₂ : Type u_1} →
                                  [inst : Semiring R] →
                                    [inst_13 : Semiring S] →
                                      [inst_14 : AddCommMonoid M] →
                                        [inst_15 : AddCommMonoid M₂] →
                                          [inst_16 : Module R M] →
                                            [inst_17 : Module R M₂] →
                                              [inst_18 : Module S M] →
                                                [inst_19 : Module S M₂] →
                                                  [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          l' ∘ₗ
                        l)) :
                  A →ₗ[A] M →ₗ[R] P) :
                (a : A) → M →ₗ[R] P)
              1 :
            (a : M) → P)
          x :
        P)
⊢ Eq (α := A ⊗[R] M →ₗ[A] P) (l' ∘ₗ liftBaseChange A l)
    (liftBaseChange A
      ((↑R :
            {S : Type u_2} →
              {M : Type u_5} →
                {M₂ : Type u_1} →
                  [inst : Semiring R] →
                    [inst_13 : Semiring S] →
                      [inst_14 : AddCommMonoid M] →
                        [inst_15 : AddCommMonoid M₂] →
                          [inst_16 : Module R M] →
                            [inst_17 : Module R M₂] →
                              [inst_18 : Module S M] →
                                [inst_19 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          l' ∘ₗ
        l))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
P : Type u_1
inst_9 : AddCommMonoid P
inst_10 : Module A P
inst_11 : Module R P
inst_12 : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
x : M
⊢ Eq.{u_1 + 1} (α := P)
    ((((AlgebraTensorModule.curry (l' ∘ₗ liftBaseChange A l) : A →ₗ[A] M →ₗ[R] P) : (a : A) → M →ₗ[R] P) 1 :
          (a : M) → P)
        x :
      P)
    ((((AlgebraTensorModule.curry
                  (liftBaseChange A
                    ((↑R :
                          {S : Type u_2} →
                            {M : Type u_5} →
                              {M₂ : Type u_1} →
                                [inst : Semiring R] →
                                  [inst_13 : Semiring S] →
                                    [inst_14 : AddCommMonoid M] →
                                      [inst_15 : AddCommMonoid M₂] →
                                        [inst_16 : Module R M] →
                                          [inst_17 : Module R M₂] →
                                            [inst_18 : Module S M] →
                                              [inst_19 : Module S M₂] →
                                                [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        l' ∘ₗ
                      l)) :
                A →ₗ[A] M →ₗ[R] P) :
              (a : A) → M →ₗ[R] P)
            1 :
          (a : M) → P)
        x :
      P)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
a : LE.le (α := Submodule A N) (range (M := A ⊗[R] M) (liftBaseChange A l)) (Submodule.span A (↑l.range : Set N))
a₁ : LE.le (α := Submodule A N) (Submodule.span A (↑l.range : Set N)) (range (M := A ⊗[R] M) (liftBaseChange A l))
⊢ Eq (α := Submodule A N) (range (M := A ⊗[R] M) (liftBaseChange A l)) (Submodule.span A (↑l.range : Set N))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A ⊗[R] M
a :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) 0 : N)
a₁ :
  ∀ (x : A) (y : M),
    Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
      ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
a₂ :
  ∀ (x y : A ⊗[R] M),
    Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
        ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N) →
      Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
          ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N) →
        Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
          ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x + y) : N)
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)

Tactic:
induction x using TensorProduct.induction_on
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) 0 : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A
y : M
a :
  Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    (HSMul.hSMul (β := N) x ((l : (a : M) → N) y : N))
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)

Tactic:
rw [LinearMap.liftBaseChange_tmul]

Premises used: LinearMap.liftBaseChange_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A
y : M
⊢ Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    (HSMul.hSMul (β := N) x ((l : (a : M) → N) y : N))

Tactic:
Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)

Premises used: Exists.intro, Submodule.subset_span, rfl, Submodule.smul_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A
y : M
⊢ Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    (HSMul.hSMul (β := N) x ((l : (a : M) → N) y : N))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x y : A ⊗[R] M
h :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
h_1 :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N)
a :
  Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    (HAdd.hAdd (α := N) (β := N) ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
      ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N))
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x + y) : N)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x y : A ⊗[R] M
h :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
h_1 :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N)
⊢ Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    (HAdd.hAdd (α := N) (β := N) ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
      ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N))

Tactic:
add_mem ‹_› ‹_›

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x y : A ⊗[R] M
h :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
h_1 :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N)
⊢ Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    (HAdd.hAdd (α := N) (β := N) ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
      ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N))

Tactic:
exact add_mem ‹_› ‹_›

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
a : (↑l.range : Set N) ⊆ (↑(range (M := A ⊗[R] M) (liftBaseChange A l)) : Set N)
⊢ LE.le (α := Submodule A N) (Submodule.span A (↑l.range : Set N)) (range (M := A ⊗[R] M) (liftBaseChange A l))

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : M
⊢ Eq.{u_3 + 1} (α := N) ((liftBaseChange A l : (a : A ⊗[R] M) → N) (1 ⊗ₜ[R] x) : N) ((l : (a : M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : M
⊢ Membership.mem (α := N) (↑(range (M := A ⊗[R] M) (liftBaseChange A l)) : Set N) ((l : (a : M) → N) x : N)

Tactic:
exact ⟨1 ⊗ₜ x, by simp⟩
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
⊢ Eq (α := A ⊗[R] B) 1 (1 ⊗ₜ[R] 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
⊢ Eq (α := A ⊗[R] B) ((↑0 : A) ⊗ₜ[R] 1) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
⊢ (↑(n + 1) : A) ⊗ₜ[R] 1 = HAdd.hAdd (α := A ⊗[R] B) ((↑n : A) ⊗ₜ[R] 1) 1

Tactic:
simp [add_tmul, one_def]

Premises used: TensorProduct.add_tmul, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
⊢ Eq (α := A ⊗[R] B) (↑n : A ⊗[R] B) ((↑n : A) ⊗ₜ[R] 1)

Tactic:
rfl

Premises used: rfl