awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ IsHomeomorph (X := PrimeSpectrum (R ⊗[k] K)) (Y := PrimeSpectrum R) (comap (algebraMap R (R ⊗[k] K)))

Tactic:
isHomeomorph_comap _ (IsPurelyInseparable.exists_pow_mem_range_tensorProduct) ?_

Premises used: PrimeSpectrum.isHomeomorph_comap, IsPurelyInseparable.exists_pow_mem_range_tensorProduct
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ LE.le (α := Ideal R) ⊥ (nilradical R)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ := ringExpChar k
h : Eq (α := Ideal R) (RingHom.ker (F := R →+* R ⊗[k] K) (algebraMap R (R ⊗[k] K))) ⊥
convert_3 : OrderBot (Ideal R)
⊢ LE.le (α := Ideal R) (RingHom.ker (F := R →+* R ⊗[k] K) (algebraMap R (R ⊗[k] K))) (nilradical R)

Tactic:
convert! bot_le

Premises used: bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ Function.Injective (α := R) (β := R ⊗[k] K) (⇑(algebraMap R (R ⊗[k] K)) : (a : R) → R ⊗[k] K)

Tactic:
Algebra.TensorProduct.includeLeft_injective (S := R) (algebraMap k K).injective

Premises used: Algebra.algebraMap, Algebra.TensorProduct.includeLeft_injective, RingHom.injective, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ Function.Injective (α := R) (β := R ⊗[k] K) (⇑(algebraMap R (R ⊗[k] K)) : (a : R) → R ⊗[k] K)

Tactic:
exact Algebra.TensorProduct.includeLeft_injective (S := R) (algebraMap k K).injective

Premises used: Algebra.algebraMap, Algebra.TensorProduct.includeLeft_injective, RingHom.injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
h :
  ∀ (x : S),
    Eq (α := L ⊗[R] S)
      ((AlgHom.comp (B := K ⊗[R] S)
              (AlgHom.restrictScalars R
                (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S))
              Algebra.TensorProduct.includeRight :
            (a : S) → L ⊗[R] S)
          x :
        L ⊗[R] S)
      ((AlgHom.comp (B := K ⊗[R] S)
              (AlgHom.restrictScalars R
                (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp
                      (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
                  (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))))
              Algebra.TensorProduct.includeRight :
            (a : S) → L ⊗[R] S)
          x :
        L ⊗[R] S)
⊢ Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
x : S
⊢ Eq (α := L ⊗[R] S)
    ((AlgHom.comp (B := K ⊗[R] S)
            (AlgHom.restrictScalars R
              (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S))
            Algebra.TensorProduct.includeRight :
          (a : S) → L ⊗[R] S)
        x :
      L ⊗[R] S)
    ((AlgHom.comp (B := K ⊗[R] S)
            (AlgHom.restrictScalars R
              (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp
                    (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
                (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))))
            Algebra.TensorProduct.includeRight :
          (a : S) → L ⊗[R] S)
        x :
      L ⊗[R] S)

Tactic:
simp [e, e2]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
⊢ Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)

Tactic:
have heq : Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
      (e.symm.toAlgHom.comp e2.symm.toAlgHom).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) ((K ⊗[R] S) ⊗[K] L)) := by
    ext; simp [e, e2]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
heq :
  Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)
rw :
  IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap
      (AlgHom.toRingHom
        (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
          (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)))))
⊢ IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap (AlgHom.toRingHom (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)))

Tactic:
rw [heq]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
heq :
  Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)
simp :
  IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : L ⊗[K] (K ⊗[R] S) →+* L ⊗[R] S)
          (↑e2.symm : K ⊗[R] S ⊗[K] L →+* L ⊗[K] (K ⊗[R] S)))
        (algebraMap (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))))
⊢ IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap
      (AlgHom.toRingHom
        (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
          (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)))))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
    AlgEquiv.toAlgHom_toRingHom, IsScalarTower.coe_toAlgHom, comap_comp]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_toRingHom, IsScalarTower.coe_toAlgHom, AlgHom.toRingHom_eq_coe, PrimeSpectrum.comap_comp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
heq :
  Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)
⊢ IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : L ⊗[K] (K ⊗[R] S) →+* L ⊗[R] S)
          (↑e2.symm : K ⊗[R] S ⊗[K] L →+* L ⊗[K] (K ⊗[R] S)))
        (algebraMap (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))))

Tactic:
(isHomeomorph_comap_of_isPurelyInseparable K L (K ⊗[R] S)).comp <|
    (isHomeomorph_comap_of_bijective e2.symm.bijective).comp <|
    isHomeomorph_comap_of_bijective e.symm.bijective

Premises used: PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable, TensorProduct, IsHomeomorph.comp, PrimeSpectrum.isHomeomorph_comap_of_bijective
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
m : M
h :
  ∀ (a_1 : ι),
    Eq.{u_2 + 1} (α := A) ((((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a ⊗ₜ[R] m) : ι →₀ A) : (a : ι) → A) a_1 : A)
      ((HSMul.hSMul (β := ι →₀ A) a
              (Finsupp.mapRange (⇑(algebraMap R A) : (a : R) → A) ⋯ ((b.repr : (a : M) → ι →₀ R) m)) :
            (a : ι) → A)
          a_1 :
        A)
⊢ (basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a ⊗ₜ[R] m) =
    HSMul.hSMul (β := ι →₀ A) a (Finsupp.mapRange (⇑(algebraMap R A) : (a : R) → A) ⋯ ((b.repr : (a : M) → ι →₀ R) m))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
m : M
a_1 : ι
⊢ Eq.{u_2 + 1} (α := A) ((((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a ⊗ₜ[R] m) : ι →₀ A) : (a : ι) → A) a_1 : A)
    ((HSMul.hSMul (β := ι →₀ A) a
            (Finsupp.mapRange (⇑(algebraMap R A) : (a : R) → A) ⋯ ((b.repr : (a : M) → ι →₀ R) m)) :
          (a : ι) → A)
        a_1 :
      A)

Tactic:
simp [basisAux, ← Algebra.commutes, Algebra.smul_def]

Premises used: Algebra.TensorProduct.basisAux, Algebra.smul_def, Algebra.commutes
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
x : A ⊗[R] M
⊢ (basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (HSMul.hSMul (β := A ⊗[R] M) a 0) =
    HSMul.hSMul (β := ι →₀ A) a ((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
x_1 : A ⊗[R] M
x : A
y : M
⊢ (basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (HSMul.hSMul (β := A ⊗[R] M) a (x ⊗ₜ[R] y)) =
    HSMul.hSMul (β := ι →₀ A) a ((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (x ⊗ₜ[R] y) : ι →₀ A)

Tactic:
simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc]

Premises used: smul_assoc, Algebra.TensorProduct.basisAux_tmul, TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
x_1 x y : A ⊗[R] M
hx :
  (basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a • x) =
    HSMul.hSMul (β := ι →₀ A) a ((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) x : ι →₀ A)
hy :
  (basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a • y) =
    HSMul.hSMul (β := ι →₀ A) a ((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) y : ι →₀ A)
⊢ (basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a • (x + y)) =
    HSMul.hSMul (β := ι →₀ A) a ((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (x + y) : ι →₀ A)

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
m : M
⊢ (Basis.repr (basis A b) : (a : A ⊗[R] M) → ι →₀ A) (a ⊗ₜ[R] m) =
    HSMul.hSMul (β := ι →₀ A) a (Finsupp.mapRange (⇑(algebraMap R A) : (a : R) → A) ⋯ ((b.repr : (a : M) → ι →₀ R) m))

Tactic:
basisAux_tmul b _ _

Premises used: Algebra.TensorProduct.basisAux_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
i : ι
⊢ Eq (α := A ⊗[R] M)
    ((LinearEquiv.symm (Basis.repr (basis A b)) : (a : ι →₀ A) → A ⊗[R] M) (Finsupp.single i a) : A ⊗[R] M)
    (a ⊗ₜ[R] (b.repr.symm : (a : ι →₀ R) → M) (Finsupp.single i 1) : A ⊗[R] M)

Tactic:
simp [basis, Equiv.uniqueProd_symm_apply, basisAux]

Premises used: Equiv.uniqueProd_symm_apply, Algebra.TensorProduct.basisAux, Algebra.TensorProduct.basis
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
i : ι
⊢ Eq (α := A ⊗[R] M) ((basis A b : (a : ι) → A ⊗[R] M) i : A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) i : A ⊗[R] M)

Tactic:
basis_repr_symm_apply b 1 i

Premises used: Algebra.TensorProduct.basis_repr_symm_apply, OfNat.ofNat
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
i : ι
⊢ HSMul.hSMul (β := A ⊗[R] M) a ((basis A b : (a : ι) → A ⊗[R] M) i : A ⊗[R] M) = a ⊗ₜ[R] (b : (a : ι) → M) i

Tactic:
simpa using basis_repr_symm_apply b a i

Premises used: Algebra.TensorProduct.basis_repr_symm_apply
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
apply :
  ∀ (i : ι'),
    Eq (α := A ⊗[R] M)
      ((baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij) : (a : A ⊗[R] N) → A ⊗[R] M)
          ((basis A b' : (a : ι') → A ⊗[R] N) i) :
        A ⊗[R] M)
      ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij :
              A ⊗[R] N →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] N) → A ⊗[R] M)
          ((basis A b' : (a : ι') → A ⊗[R] N) i) :
        A ⊗[R] M)
⊢ Eq (α := A ⊗[R] N →ₗ[A] A ⊗[R] M) (baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij))
    ((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij)

Tactic:
apply (basis A b').ext

Premises used: Algebra.TensorProduct.basis, Module.Basis.ext
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
simp :
  (1 ⊗ₜ[R] (((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij : N →ₗ[R] M) : (a : N) → M) ((b' : (a : ι') → N) k : N) :
    A ⊗[R] M)
| ((baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij) : (a : A ⊗[R] N) → A ⊗[R] M)
      ((basis A b' : (a : ι') → A ⊗[R] N) k) :
    A ⊗[R] M)

Tactic:
simp only [basis_apply, baseChange_tmul]

Premises used: Algebra.TensorProduct.basis_apply, LinearMap.baseChange_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
conv_lhs :
  Eq (α := A ⊗[R] M)
    (1 ⊗ₜ[R] (((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij : N →ₗ[R] M) : (a : N) → M) ((b' : (a : ι') → N) k : N) :
      A ⊗[R] M)
    ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij :
            A ⊗[R] N →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) k) :
      A ⊗[R] M)
⊢ Eq (α := A ⊗[R] M)
    ((baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij) : (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) k) :
      A ⊗[R] M)
    ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij :
            A ⊗[R] N →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) k) :
      A ⊗[R] M)

Tactic:
conv_lhs => simp only [basis_apply, baseChange_tmul]

Premises used: Algebra.TensorProduct.basis_apply, LinearMap.baseChange_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
simp_rw :
  Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] if ij.2 = k then (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
    (if ij.2 = k then 1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
⊢ Eq (α := A ⊗[R] M)
    (1 ⊗ₜ[R] (((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij : N →ₗ[R] M) : (a : N) → M) ((b' : (a : ι') → N) k : N) :
      A ⊗[R] M)
    ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij :
            A ⊗[R] N →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) k) :
      A ⊗[R] M)

Tactic:
simp_rw [Basis.linearMap_apply_apply, basis_apply]

Premises used: Algebra.TensorProduct.basis_apply, Module.Basis.linearMap_apply_apply
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
isTrue :
  ij.2 = k → Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M)
isFalse : ¬ij.2 = k → Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] 0) 0
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] if ij.2 = k then (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
    (if ij.2 = k then 1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)

Tactic:
split
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
h : ij.2 = k
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M)

Tactic:
simp only [TensorProduct.tmul_zero]

Premises used: TensorProduct.tmul_zero
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
h : ¬ij.2 = k
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] 0) 0

Tactic:
simp only [TensorProduct.tmul_zero]

Premises used: TensorProduct.tmul_zero
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : DecidableEq ι
b : Basis ι R M
ij : ι × ι
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] M) (baseChange A ((b.end : (a : ι × ι) → End R M) ij))
    ((Basis.end (basis A b) : (a : ι × ι) → End A (A ⊗[R] M)) ij)

Tactic:
b.baseChange_linearMap A b ij

Premises used: Module.Basis.baseChange_linearMap
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R_1 : Type u_1
A_1 : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring A
inst_5 : Algebra R A
⊢ Free A (A ⊗[R] M)

Tactic:
Module.Free.of_basis <| Algebra.TensorProduct.basis A (Module.Free.chooseBasis R M)

Premises used: Module.Free.of_basis, Algebra.TensorProduct.basis, Module.Free.chooseBasis