awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Finite
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)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              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) k : S ⊗[R] S))
      (f.sum fun (i : 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)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
apply :
  ∀ x_1 ∈ f.support,
    Eq.{u_2 + 1} (α := S ⊗[R] S)
      (∑ x ∈ (a x_1).support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x_1 : (a : I) → R) x : R) ((f : (a : I) → S) x_1 : S) ⊗ₜ[R]
          (b : (a : I) → S) x)
      (∑
        x_2 ∈
          f.support.biUnion fun (i : I) ↦
            Finsupp.support.{u_4, u_1} (M := R)
              ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_1 : S) x) : I →₀ R) : (a : I) → R)
                x_2 :
              R)
            ((f : (a : I) → S) x_1 : S) ⊗ₜ[R]
          (b : (a : I) → S) x_2)
⊢ 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)
    (∑ x_1 ∈ f.support,
      ∑
        x_2 ∈
          f.support.biUnion fun (i : I) ↦
            Finsupp.support.{u_4, u_1} (M := R)
              ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_1 : S) x) : I →₀ R) : (a : I) → R)
                x_2 :
              R)
            ((f : (a : I) → S) x_1 : S) ⊗ₜ[R]
          (b : (a : I) → S) x_2)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Unramified.Finite
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)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              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) k : S ⊗[R] S))
      (f.sum fun (i : 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)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
⊢ (a i).support ⊆
    f.support.biUnion fun (i : I) ↦
      Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))

Tactic:
Finset.subset_biUnion_of_mem (fun i ↦ (a i).support) hi

Premises used: Set.Mem, setOf, Finsupp.support, Finset.subset_biUnion_of_mem
-- Module: Mathlib.RingTheory.Unramified.Finite
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)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              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) k : S ⊗[R] S))
      (f.sum fun (i : 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)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
⊢ (a i).support ⊆
    f.support.biUnion fun (i : I) ↦
      Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))

Tactic:
exact Finset.subset_biUnion_of_mem (fun i ↦ (a i).support) hi

Premises used: Finsupp.support, Finset.subset_biUnion_of_mem
-- Module: Mathlib.RingTheory.Unramified.Finite
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)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              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) k : S ⊗[R] S))
      (f.sum fun (i : 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)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
⊢ ∀ (x_1 x_2 : I),
    ¬Eq.{u_2 + 1} (α := S) ((f : (a : I) → S) x_2 : S) (0 : S) →
      ¬Eq.{u_1 + 1} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_2 : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            (0 : R) →
        Eq.{u_1 + 1} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            (0 : R) →
          Eq (α := S ⊗[R] S)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
                  ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) :
                        (a : I) → R)
                      x_1 :
                    R)
                  ((f : (a : I) → S) i : S) ⊗ₜ[R]
                (b : (a : I) → S) x_1 :
              S ⊗[R] S)
            (0 : S ⊗[R] S)

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.Unramified.Finite
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)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              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) k : S ⊗[R] S))
      (f.sum fun (i : 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)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support,
    Eq (α := S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) x_1 : R) ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)

Tactic:
fun _ _ ↦ rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Unramified.Finite
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)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              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) k : S ⊗[R] S))
      (f.sum fun (i : 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)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support,
    Eq (α := S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) x_1 : R) ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)

Tactic:
exact fun _ _ ↦ rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
s : S
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * elem R S = 0

Tactic:
(iff_exists_tensorProduct.mp inferInstance).choose_spec.1 s

Premises used: Exists.choose_spec, Algebra.FormallyUnramified.elem, inferInstance, And.left, Iff.mp, Algebra.FormallyUnramified.iff_exists_tensorProduct
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
s : S
rw : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) - HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S) = 0
rw₁ : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * elem R S = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := S ⊗[R] S) 0 0
⊢ HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) = HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S)

Tactic:
rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem]

Premises used: sub_eq_zero, Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem, sub_mul
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
⊢ Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (elem R S) : S) (1 : S)

Tactic:
(iff_exists_tensorProduct.mp inferInstance).choose_spec.2

Premises used: Exists.choose_spec, Algebra.FormallyUnramified.elem, inferInstance, And.right, Iff.mp, Algebra.FormallyUnramified.iff_exists_tensorProduct
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
h :
  Eq (α := S ⊗[R] S) (elem R S)
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
⊢ ∃ (a : I →₀ S), Eq (α := S ⊗[R] S) (elem R S) (a.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)

Tactic:
use b'.repr (elem R S)

Premises used: Algebra.FormallyUnramified.elem, Module.Basis.repr, DFunLike.coe
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
rw :
  Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (a : S) ↦
    HSMul.hSMul (β := S ⊗[R] S) a ((b' : (a : I) → S ⊗[R] S) i : S ⊗[R] S)
| elem R S

Tactic:
rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]

Premises used: Algebra.FormallyUnramified.elem, Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
h :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (a : S) ↦
      HSMul.hSMul (β := S ⊗[R] S) a ((b' : (a : I) → S ⊗[R] S) i : S ⊗[R] S))
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
⊢ Eq (α := S ⊗[R] S) (elem R S)
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)

Tactic:
conv_lhs => rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]

Premises used: Algebra.FormallyUnramified.elem, Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
h :
  ∀ (x : I) (i : S),
    HSMul.hSMul (β := S ⊗[R] S) i ((b' : (a : I) → S ⊗[R] S) x : S ⊗[R] S) = i ⊗ₜ[R] (b : (a : I) → S) x
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (a : S) ↦
      HSMul.hSMul (β := S ⊗[R] S) a ((b' : (a : I) → S ⊗[R] S) i : S ⊗[R] S))
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)

Tactic:
congr! with _ i x
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
x : I
i : S
⊢ HSMul.hSMul (β := S ⊗[R] S) i ((b' : (a : I) → S ⊗[R] S) x : S ⊗[R] S) = i ⊗ₜ[R] (b : (a : I) → S) x

Tactic:
simp [b', Basis.tensorProduct, TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul', Module.Basis.tensorProduct
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
have :
  ∀ (f : I →₀ S) (hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)),
    Module.Finite R S
⊢ Module.Finite R S

Tactic:
have ⟨f, hf⟩ : ∃ (a : I →₀ S), elem R S = a.sum (fun i x ↦ x ⊗ₜ b i) := by
    let b' := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
    use b'.repr (elem R S)
    conv_lhs => rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]
    congr! with _ i x
    simp [b', Basis.tensorProduct, TensorProduct.smul_tmul']
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
fg_top : Submodule.FG.{u_1, u_2} (R := R) (M := S) ⊤
⊢ Module.Finite R S

Tactic:
constructor
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
h :
  Eq (α := Submodule R S)
    (Submodule.span R
      (↑(Finset.image₂ (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
            f.support f.support) :
        Set S))
    ⊤
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := S) ⊤

Tactic:
use Finset.image₂ (fun i j ↦ f i * b j) f.support f.support

Premises used: HMul.hMul, Finsupp.support, DFunLike.coe, Finset.image₂
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
h :
  LE.le (α := Submodule R S) ⊤
    (Submodule.span R
      (↑(Finset.image₂ (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
            f.support f.support) :
        Set S))
⊢ Eq (α := Submodule R S)
    (Submodule.span R
      (↑(Finset.image₂ (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
            f.support f.support) :
        Set S))
    ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
j : I
hj : j ∉ f.support
⊢ Eq (α := I →₀ R)
    ((fun (j : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S)) : I →₀ R)) j) 0

Tactic:
simp [Finsupp.notMem_support_iff.mp hj]

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj : j ∉ f.support.biUnion fun (i : I) ↦ (a i).support
⊢ ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)

Tactic:
simp only [Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_exists, not_and,
      not_not] at hj

Premises used: Finsupp.mem_support_iff, Classical.not_not, not_exists, ne_eq, not_and, Finset.mem_biUnion