awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
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)
hg :
  Function.Surjective (β := HasQuotient.Quotient R (B := Ideal R) 𝔭) fun (x : R♭) ↦
    (PreTilt.coeff 0 : (a : R♭) → ModP R p) x
⊢ Function.Surjective.{u + 1, u + 1} (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
have hf : Function.Surjective (β := R♭) fun (x : 𝕎 R♭) ↦ x.coeff 0
Tactic: apply Function.Surjective.comp
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.Untilt (goal)
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 : ℕ
⊢ 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
have 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)
Tactic: simp only [← map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.Untilt (goal)
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 : ℕ
⊢ 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)
have h : (⇑(RingEquiv.symm (frobeniusEquiv (PreTilt O p) p)) : (a : PreTilt O p) → PreTilt O p)^[n] x ^ p ^ n = x
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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₃
⊢ 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)
have 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)
Tactic: rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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)
⊢ 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)
have 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)
Tactic: rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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)
⊢ 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)
have 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)
Tactic: rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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)
⊢ 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)
have 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)
Tactic: rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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
⊢ ((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
have 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)
Tactic: induction x using PiTensorProduct.induction_on with
  | smul_tprod => simp
  | add _ _ h1 h2 => simp [map_add, h1, h2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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)
⊢ ((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
have 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
Tactic: induction x using PiTensorProduct.induction_on with
  | smul_tprod => simp
  | add _ _ h1 h2 => simp [map_add, h1, h2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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
⊢ (((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
have 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)
Tactic: induction x using PiTensorProduct.induction_on with
  | smul_tprod => simp
  | add _ _ h1 h2 => simp [h1, h2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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)
⊢ (((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
have 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
Tactic: induction x using PiTensorProduct.induction_on with
  | smul_tprod => simp
  | add _ _ h1 h2 => simp [h1, h2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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'
⊢ 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)
have 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)
Tactic: rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply, mul_comm,
        mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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'
⊢ 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)
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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'
⊢ 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)
have e_a : 1 = HMul.hMul (α := ⨂[R] (i : ι), A i) 1 1
Tactic: change (1 : ⨂[R] i, A i) = 1 * 1
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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'
⊢ 1 = HMul.hMul (α := ⨂[R] (i : ι), A i) 1 1
have e_a : Eq (α := ⨂[R] (i : ι), A i) 1 1
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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 : R'
x : ⨂[R] (i : ι), A i
⊢ HMul.hMul (α := ⨂[R] (i : ι), A i)
      ((({ toFun := fun (x : R') ↦ HSMul.hSMul (β := ⨂[R] (i : ι), A i) x 1, map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ } :
              R' →+* ⨂[R] (i : ι), A i) :
            (a : R') → ⨂[R] (i : ι), A i)
          r :
        ⨂[R] (i : ι), A i)
      x =
    HMul.hMul (β := ⨂[R] (i : ι), A i) x
      ((({ toFun := fun (x : R') ↦ HSMul.hSMul (β := ⨂[R] (i : ι), A i) x 1, map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ } :
              R' →+* ⨂[R] (i : ι), A i) :
            (a : R') → ⨂[R] (i : ι), A i)
          r :
        ⨂[R] (i : ι), A i)
have simp : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 * x = x * HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1
Tactic: simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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 : R'
x : ⨂[R] (i : ι), A i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 * x = x * HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1
have change : Eq (α := ⨂[R] (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 1) :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      x :
    ⨂[R] (i : ι), A i)
  ((((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)
      (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1) :
    ⨂[R] (i : ι), A i)
Tactic: change mul _ _ = mul _ _