awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u} (M := R) (↑p : R)
inst_3 : IsAdicComplete (R := R) 𝔭 R
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this_1 : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
this :
  Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
⊢ Function.Surjective (β := R♭) fun (x : 𝕎 R♭) ↦ x.coeff 0

Tactic:
WittVector.coeff_surjective 0

Premises used: WittVector.coeff_surjective, OfNat.ofNat
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u} (M := R) (↑p : R)
inst_3 : IsAdicComplete (R := R) 𝔭 R
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this_1 : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
this :
  Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
⊢ Function.Surjective (β := R♭) fun (x : 𝕎 R♭) ↦ x.coeff 0

Tactic:
exact WittVector.coeff_surjective 0

Premises used: WittVector.coeff_surjective, OfNat.ofNat
-- Module: Mathlib.RingTheory.Perfectoid.Untilt
Goal:
O : Type u_1
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u_1} (M := O) (↑p : O)
inst_3 : IsAdicComplete (R := O) (span {(↑p : O)}) O
x : PreTilt O p
⊢ Eq (α := HasQuotient.Quotient O (B := Ideal O) (span {(↑p : O)}))
    ((Ideal.Quotient.mk (span {(↑p : O)}) : (a : O) → O ⧸ span {(↑p : O)}) ((untilt : (a : PreTilt O p) → O) x) :
      HasQuotient.Quotient O (B := Ideal O) (span {(↑p : O)}))
    ((coeff 0 : (a : PreTilt O p) → ModP O p) x : ModP O p)

Tactic:
mk_teichmuller x

Premises used: Perfection.mk_teichmuller
-- Module: Mathlib.RingTheory.Perfectoid.Untilt
Goal:
O : Type u_1
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u_1} (M := O) (↑p : O)
inst_3 : IsAdicComplete (R := O) (span {(↑p : O)}) O
⊢ Eq (α := PreTilt O p → HasQuotient.Quotient O (B := Ideal O) (span {(↑p : O)}))
    (Function.comp (β := O) (⇑(Ideal.Quotient.mk (span {(↑p : O)})) : (a : O) → O ⧸ span {(↑p : O)})
      (⇑untilt : (a : PreTilt O p) → O))
    (⇑(coeff 0) : (a : PreTilt O p) → ModP O p)

Tactic:
mk_comp_teichmuller' ..

Premises used: Perfection.mk_comp_teichmuller', PreTilt
-- Module: Mathlib.RingTheory.Perfectoid.Untilt
Goal:
O : Type u_1
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u_1} (M := O) (↑p : O)
inst_3 : IsAdicComplete (R := O) (span {(↑p : O)}) O
x : PreTilt O p
n : ℕ
simp :
  Eq (α := O)
    ((untilt : (a : PreTilt O p) → O)
        ((⇑(RingEquiv.symm (frobeniusEquiv (PreTilt O p) p)) : (a : PreTilt O p) → PreTilt O p)^[n] x ^ p ^ n) :
      O)
    ((untilt : (a : PreTilt O p) → O) x : O)
⊢ HPow.hPow (α := O)
      ((untilt : (a : PreTilt O p) → O)
          ((⇑(RingEquiv.symm (frobeniusEquiv (PreTilt O p) p)) : (a : PreTilt O p) → PreTilt O p)^[n] x) :
        O)
      (p ^ n) =
    (untilt : (a : PreTilt O p) → O) x

Tactic:
simp only [← map_pow]

Premises used: map_pow
-- Module: Mathlib.RingTheory.Perfectoid.Untilt
Goal:
O : Type u_1
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u_1} (M := O) (↑p : O)
inst_3 : IsAdicComplete (R := O) (span {(↑p : O)}) O
x : PreTilt O p
n : ℕ
h : (⇑(RingEquiv.symm (frobeniusEquiv (PreTilt O p) p)) : (a : PreTilt O p) → PreTilt O p)^[n] x ^ p ^ n = x
⊢ Eq (α := O)
    ((untilt : (a : PreTilt O p) → O)
        ((⇑(RingEquiv.symm (frobeniusEquiv (PreTilt O p) p)) : (a : PreTilt O p) → PreTilt O p)^[n] x ^ p ^ n) :
      O)
    ((untilt : (a : PreTilt O p) → O) x : O)

Tactic:
congr
-- Module: Mathlib.RingTheory.Perfectoid.Untilt
Goal:
O : Type u_1
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u_1} (M := O) (↑p : O)
inst_3 : IsAdicComplete (R := O) (span {(↑p : O)}) O
x : PreTilt O p
n : ℕ
⊢ (⇑(RingEquiv.symm (frobeniusEquiv (PreTilt O p) p)) : (a : PreTilt O p) → PreTilt O p)^[n] x ^ p ^ n = x

Tactic:
simp
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoidWithOne (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
⊢ Eq (α := ⨂[R] (i : ι), A i) 1 ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x y : (i : ι) → A i
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) x) :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) y) :
      ⨂[R] (i : ι), A i)
    ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (x * y) : ⨂[R] (i : ι), A i)

Tactic:
simp only [mul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply', Pi.mul_def]

Premises used: LinearMap.mul_apply', PiTensorProduct.mul, PiTensorProduct.piTensorHomMap₂_tprod_tprod_tprod, Pi.mul_def
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x y : ⨂[R] (i : ι), A i
⊢ x * y =
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x y : (i : ι) → A i
⊢ HMul.hMul (α := ⨂[R] (i : ι), A i) (β := ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) x : ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) y : ⨂[R] (i : ι), A i) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (x * y)

Tactic:
mul_tprod_tprod x y

Premises used: PiTensorProduct.mul_tprod_tprod
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
a₁ a₂ a₃ : (i : ι) → A i
ha : SemiconjBy a₁ a₂ a₃
rw :
  HMul.hMul (α := ⨂[R] (i : ι), A i) (β := ⨂[R] (i : ι), A i)
      ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₁ : ⨂[R] (i : ι), A i)
      ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₂ : ⨂[R] (i : ι), A i) =
    HMul.hMul (α := ⨂[R] (i : ι), A i) (β := ⨂[R] (i : ι), A i)
      ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₃ : ⨂[R] (i : ι), A i)
      ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₁ : ⨂[R] (i : ι), A i)
rw₁ :
  (PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (a₁ * a₂) =
    HMul.hMul (α := ⨂[R] (i : ι), A i) (β := ⨂[R] (i : ι), A i)
      ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₃ : ⨂[R] (i : ι), A i)
      ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₁ : ⨂[R] (i : ι), A i)
rw₂ :
  Eq (α := ⨂[R] (i : ι), A i)
    ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (a₁ * a₂) : ⨂[R] (i : ι), A i)
    ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (a₃ * a₁) : ⨂[R] (i : ι), A i)
rw₃ rw₄ :
  Eq (α := ⨂[R] (i : ι), A i)
    ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (a₃ * a₁) : ⨂[R] (i : ι), A i)
    ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (a₃ * a₁) : ⨂[R] (i : ι), A i)
⊢ SemiconjBy (M := ⨂[R] (i : ι), A i)
    ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₁ : ⨂[R] (i : ι), A i)
    ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₂ : ⨂[R] (i : ι), A i)
    ((PiTensorProduct.tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₃ : ⨂[R] (i : ι), A i)

Tactic:
rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]

Premises used: SemiconjBy, PiTensorProduct.tprod_mul_tprod
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
a₁ a₂ : (i : ι) → A i
ha : Commute a₁ a₂
⊢ Commute (S := ⨂[R] (i : ι), A i) ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₁ : ⨂[R] (i : ι), A i)
    ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) a₂ : ⨂[R] (i : ι), A i)

Tactic:
ha.tprod

Premises used: SemiconjBy.tprod, Commute
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
r s : R
x y : (i : ι) → A i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) x : ⨂[R] (i : ι), A i) *
      HSMul.hSMul (β := ⨂[R] (i : ι), A i) s
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) y : ⨂[R] (i : ι), A i) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) (r * s)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (x * y) : ⨂[R] (i : ι), A i)

Tactic:
simp only [mul_def, map_smul, LinearMap.smul_apply, mul_tprod_tprod, mul_comm r s, mul_smul]

Premises used: LinearMap.smul_apply, PiTensorProduct.mul_def, PiTensorProduct.mul_tprod_tprod, mul_comm, SemigroupAction.mul_smul, map_smul
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
r : R
f : (i : ι) → A i
⊢ ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)

Tactic:
simp
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x y : ⨂[R] (i : ι), A i
h1 :
  ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      x =
    x
h2 :
  ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      y =
    y
⊢ ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      (x + y) =
    x + y

Tactic:
simp [map_add, h1, h2]

Premises used: map_add
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x : ⨂[R] (i : ι), A i
smul_tprod :
  ∀ (r : R) (f : (i : ι) → A i),
    ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)) =
      HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)
add :
  ∀ (x y : ⨂[R] (i : ι), A i)
    (h1 :
      ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          x =
        x)
    (h2 :
      ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          y =
        y),
    ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        (x + y) =
      x + y
⊢ ((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      x =
    x

Tactic:
induction x using PiTensorProduct.induction_on with
  | smul_tprod => simp
  | add _ _ h1 h2 => simp [map_add, h1, h2]

Premises used: map_add
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
r : R
f : (i : ι) → A i
⊢ (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
              ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)) :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)

Tactic:
simp
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x y : ⨂[R] (i : ι), A i
h1 :
  (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    x
h2 :
  (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) y :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    y
⊢ (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) (x + y) :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    x + y

Tactic:
simp [h1, h2]
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonAssocSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x : ⨂[R] (i : ι), A i
smul_tprod :
  ∀ (r : R) (f : (i : ι) → A i),
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
                ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)) :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
      HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) f : ⨂[R] (i : ι), A i)
add :
  ∀ (x y : ⨂[R] (i : ι), A i)
    (h1 :
      (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
              (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
        x)
    (h2 :
      (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) y :
              (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
        y),
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) (x + y) :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
      x + y
⊢ (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    x

Tactic:
induction x using PiTensorProduct.induction_on with
  | smul_tprod => simp
  | add _ _ h1 h2 => simp [h1, h2]
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x_1 y_1 z_1 : ⨂[R] (i : ι), A i
x y z : (i : ι) → A i
⊢ HMul.hMul (β := ⨂[R] (i : ι), A i)
      (HMul.hMul (α := ⨂[R] (i : ι), A i) (β := ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) x : ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) y : ⨂[R] (i : ι), A i))
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) z : ⨂[R] (i : ι), A i) =
    HMul.hMul (α := ⨂[R] (i : ι), A i)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) x : ⨂[R] (i : ι), A i)
      (HMul.hMul (α := ⨂[R] (i : ι), A i) (β := ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) y : ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) z : ⨂[R] (i : ι), A i))

Tactic:
simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z)

Premises used: mul_assoc, PiTensorProduct.tprod, congr_arg, DFunLike.coe, PiTensorProduct.tprod_mul_tprod
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
⊢ HSMul.hSMul (α := R') (β := ⨂[R] (i : ι), A i) 1 1 = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r s : R'
rw :
  s • HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 =
    s •
      HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
        (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) 1 :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          1)
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) (r * s) 1 =
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1) :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      (HSMul.hSMul (β := ⨂[R] (i : ι), A i) s 1)

Tactic:
rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply, mul_comm,
        mul_smul]

Premises used: LinearMap.smul_apply, mul_comm, LinearMap.map_smul_of_tower, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r s : R'
e_a :
  Eq (α := ⨂[R] (i : ι), A i) 1
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) 1 :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      1)
⊢ s • HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 =
    s •
      HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
        (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) 1 :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          1)

Tactic:
congr