awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)
have succ : ∀ (n : ℕ) (f : V ⊗[S] U ≃ₐ[V] Fin n → V),
  ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)
Tactic: obtain ⟨n, ⟨f⟩⟩ := hV.nonempty_algEquiv_fun
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)
have succ : Module.FaithfullyFlat R V
Tactic: refine ⟨V, inferInstance, inferInstance, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
succ : Module.FaithfullyFlat R V
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)
have succ₁ : Module.Finite R V
Tactic: refine ⟨V, inferInstance, inferInstance, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
succ : Module.FaithfullyFlat R V
succ₁ : Module.Finite R V
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)
have succ₂ : Etale R V
Tactic: refine ⟨V, inferInstance, inferInstance, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
succ : Module.FaithfullyFlat R V
succ₁ : Module.Finite R V
succ₂ : Etale R V
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)
have succ₃ : IsFiniteSplit V (V ⊗[R] S)
Tactic: refine ⟨V, inferInstance, inferInstance, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ Module.FaithfullyFlat R S
have h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
Tactic: apply Module.FaithfullyFlat.of_comap_surjective
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
have h : ∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p
Tactic: rw [← PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ Module.FaithfullyFlat R V
have this₁ : Module.FaithfullyFlat R S
Tactic: have : Module.FaithfullyFlat R S := by
        apply Module.FaithfullyFlat.of_comap_surjective
        rw [← PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]
        intro p
        simp [hn]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
⊢ Eq (α := Matrix (Fin h.dim) (Fin h.dim) R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R) fun (i j : Fin h.dim) ↦
        (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ))) :
      Matrix (Fin h.dim) (Fin h.dim) R)
have a : ∀ (i j : Fin h.dim),
  Eq (α := R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
        j :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
i j : Fin h.dim
⊢ Eq (α := R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
        j :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
have a : Eq (α := R)
  ((trace R S : (a : S) → R)
      (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
    R)
  ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
      (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
    R)
Tactic: rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
i j : Fin h.dim
a :
  Eq (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
⊢ Eq (α := R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
        j :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
have a₁ : Eq.{u_1 + 1} (α := R)
  ((trace R S : (a : S) → R)
      (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
    R)
  ((trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ))) : R)
Tactic: rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
i j : Fin h.dim
a :
  Eq (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ))) : R)
⊢ Eq (α := R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
        j :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
have a₂ : Eq.{u_1 + 1} (α := R)
  ((trace R S : (a : S) → R)
      (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
    R)
  ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
Tactic: rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]