awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
⊢ Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)
have h : LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
  (S ⊗[R] S ∙ e)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
h :
  LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)
⊢ Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)
have h₁ : LE.le (α := Ideal (S ⊗[R] S)) (S ⊗[R] S ∙ e)
  (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
⊢ LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)
have h : ∀ (y : S), e ∣ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
Tactic: simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ht₂,
        Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
s : S
⊢ e ∣ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)
have h : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) = e * HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)
Tactic: use 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R
ha : a = fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
⊢ HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] x) (f.sum fun (i : I) (y : S) ↦ y ⊗ₜ[R] (b : (a : I) → S) i) =
    ∑ k ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) k : R) y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)
have rw : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (∑ i ∈ f.support,
    HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
  (∑ k ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
    Finsupp.sum (M := R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) k : R) y) :
        I →₀ R)
      fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
Tactic: rw [Finsupp.sum, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R
ha : a = fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (∑ k ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) k : R) y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
have subst : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (∑ i ∈ f.support,
    HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
  (∑
    k ∈
      f.support.biUnion fun (i : I) ↦
        Finsupp.support.{u_4, u_1} (M := R)
          ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
    Finsupp.sum (M := R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦
            HSMul.hSMul.{u_1, u_2, u_2} (α := R)
              (((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                      i :
                    (a : I) → R)
                  k :
                R)
              y) :
        I →₀ R)
      fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
Tactic: subst ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
| ∑ i ∈ f.support,
    HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
have simp : ∑ i ∈ f.support, (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i)
Tactic: simp only [TensorProduct.tmul_mul_tmul, one_mul, mul_comm x (b _),
      ← show ∀ i, Finsupp.linearCombination _ b (a i) = b i * x from
          fun _ ↦ b.linearCombination_repr _]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦
              HSMul.hSMul.{u_1, u_2, u_2} (α := R)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
have conv_lhs : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (∑ i ∈ f.support, (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i))
  (∑
    k ∈
      f.support.biUnion fun (i : I) ↦
        Finsupp.support.{u_4, u_1} (M := R)
          ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
    Finsupp.sum (M := R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦
            HSMul.hSMul.{u_1, u_2, u_2} (α := R)
              (((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                      i :
                    (a : I) → R)
                  k :
                R)
              y) :
        I →₀ R)
      fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
Tactic: conv_lhs =>
    simp only [TensorProduct.tmul_mul_tmul, one_mul, mul_comm x (b _),
      ← show ∀ i, Finsupp.linearCombination _ b (a i) = b i * x from
          fun _ ↦ b.linearCombination_repr _]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
| ∑ i ∈ f.support, (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i)
have simp : ∑ x ∈ f.support,
  ∑ x_1 ∈ (a x).support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
      (b : (a : I) → S) x_1
Tactic: simp only [Finsupp.linearCombination, Finsupp.coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Finsupp.sum, TensorProduct.tmul_sum,
    ← TensorProduct.smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i))
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦
              HSMul.hSMul.{u_1, u_2, u_2} (α := R)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
have conv_lhs : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (∑ x ∈ f.support,
    ∑ x_1 ∈ (a x).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
        (b : (a : I) → S) x_1)
  (∑
    k ∈
      f.support.biUnion fun (i : I) ↦
        Finsupp.support.{u_4, u_1} (M := R)
          ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
    Finsupp.sum (M := R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦
            HSMul.hSMul.{u_1, u_2, u_2} (α := R)
              (((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                      i :
                    (a : I) → R)
                  k :
                R)
              y) :
        I →₀ R)
      fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
Tactic: conv_lhs => simp only [Finsupp.linearCombination, Finsupp.coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Finsupp.sum, TensorProduct.tmul_sum,
    ← TensorProduct.smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
i : I
⊢ Eq (α := S ⊗[R] S)
    (Finsupp.sum
      (f.sum fun (i_1 : I) (y : S) ↦
        HSMul.hSMul (α := R) (β := I →₀ R) ((a i_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : I) (y : S) ↦
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
have rw : Eq (α := S ⊗[R] S)
  (f.sum fun (a_1 : I) (b_1 : S) ↦
    (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
  (f.sum fun (i_1 : I) (y : S) ↦
    Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
Tactic: rw [Finsupp.sum_sum_index]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
i : I
rw :
  Eq (α := S ⊗[R] S)
    (f.sum fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : I) (y : S) ↦
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
⊢ Eq (α := S ⊗[R] S)
    (Finsupp.sum
      (f.sum fun (i_1 : I) (y : S) ↦
        HSMul.hSMul (α := R) (β := I →₀ R) ((a i_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : I) (y : S) ↦
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
have h_zero : ∀ (a : I),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S ⊗[R] S) 0 ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) = 0
Tactic: rw [Finsupp.sum_sum_index]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
i : I
rw :
  Eq (α := S ⊗[R] S)
    (f.sum fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : I) (y : S) ↦
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
h_zero :
  ∀ (a : I),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S ⊗[R] S) 0 ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
      0
⊢ Eq (α := S ⊗[R] S)
    (Finsupp.sum
      (f.sum fun (i_1 : I) (y : S) ↦
        HSMul.hSMul (α := R) (β := I →₀ R) ((a i_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : I) (y : S) ↦
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
have h_add : ∀ (a : I) (b₁ b₂ : R),
  HSMul.hSMul (β := S ⊗[R] S) (b₁ + b₂) ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
    HSMul.hSMul (β := S ⊗[R] S) b₁ ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) +
      HSMul.hSMul (β := S ⊗[R] S) b₂ ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
Tactic: rw [Finsupp.sum_sum_index]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
i : I
⊢ Eq (α := S ⊗[R] S)
    (f.sum fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : I) (y : S) ↦
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
have e_g : Eq (α := I → S → S ⊗[R] S)
  (fun (a_1 : I) (b_1 : S) ↦
    (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
  fun (i_1 : I) (y : S) ↦
  Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
      (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
i : I
⊢ Eq (α := I → S → S ⊗[R] S)
    (fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    fun (i_1 : I) (y : S) ↦
    Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i_1 : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
have e_g : ∀ (j : I) (s : S),
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    ((HSMul.hSMul (α := R) (β := I →₀ R) ((a j : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) s : I →₀ R)).sum
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
Tactic: ext j s
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
i j : I
s : S
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    ((HSMul.hSMul (α := R) (β := I →₀ R) ((a j : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) s : I →₀ R)).sum
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
have e_g : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (i_1 : I) (a_1 : R) ↦
    HSMul.hSMul (β := S ⊗[R] S) (HMul.hMul (α := R) ((a j : (a : I) → R) i : R) a_1)
      ((b : (a : I) → S) i_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
  (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
      (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
Tactic: rw [Finsupp.sum_smul_index]