awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TotallySplit
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)
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)
⊢ ∃ (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

Premises used: Algebra.IsFiniteSplit.nonempty_algEquiv_fun
-- Module: Mathlib.RingTheory.TotallySplit
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)

Tactic:
⟨V, inferInstance, inferInstance, ?_, ?_, ?_, ?_⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.RingTheory.TotallySplit
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
succ₃ : IsFiniteSplit V (V ⊗[R] S)
⊢ ∃ (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:
refine ⟨V, inferInstance, inferInstance, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.TotallySplit
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_1 : 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)
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
⊢ Module.FaithfullyFlat R S

Tactic:
apply Module.FaithfullyFlat.of_comap_surjective

Premises used: Module.FaithfullyFlat.of_comap_surjective
-- Module: Mathlib.RingTheory.TotallySplit
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_1 : 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)
h : ∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p
⊢ Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))

Tactic:
rw [← PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]

Premises used: PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective
-- Module: Mathlib.RingTheory.TotallySplit
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)
p : PrimeSpectrum R
⊢ 0 < Module.rankAtStalk S p

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.TotallySplit
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

Tactic:
have : Module.FaithfullyFlat R S := by
        apply Module.FaithfullyFlat.of_comap_surjective
        rw [← PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]
        intro p
        simp [hn]
-- Module: Mathlib.RingTheory.TotallySplit
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_6 : 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)
this : Module.FaithfullyFlat R S
⊢ Module.FaithfullyFlat R V

Tactic:
Module.FaithfullyFlat.trans R S V

Premises used: Module.FaithfullyFlat.trans
-- Module: Mathlib.RingTheory.TotallySplit
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_6 : 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)
this : Module.FaithfullyFlat R S
⊢ Module.FaithfullyFlat R V

Tactic:
exact Module.FaithfullyFlat.trans R S V

Premises used: Module.FaithfullyFlat.trans
-- Module: Mathlib.RingTheory.TotallySplit
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.Finite R V

Tactic:
Module.Finite.trans S V

Premises used: Module.Finite.trans