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
apply : LT.lt (α := (p : PrimeSpectrum R) → ℕ) 0 (Module.rankAtStalk S)
⊢ Nontrivial S

Tactic:
apply Module.nontrivial_of_rankAtStalk_pos (R := R)

Premises used: Module.nontrivial_of_rankAtStalk_pos
-- 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
⊢ LT.lt (α := (p : PrimeSpectrum R) → ℕ) 0 (Module.rankAtStalk S)

Tactic:
simp [hn]
-- 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
⊢ Nontrivial S

Tactic:
have : Nontrivial S := by
      apply Module.nontrivial_of_rankAtStalk_pos (R := R)
      simp [hn]
-- 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 : Nontrivial S
succ :
  ∀ (U : Type u) (w : CommRing U) (w_1 : Algebra S U) (e : S ⊗[R] S ≃ₐ[S] 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)
⊢ ∃ (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 ⟨U, _, _, ⟨e⟩⟩ := Algebra.FormallyUnramified.exists_algEquiv_prod R S

Premises used: Algebra.FormallyUnramified.exists_algEquiv_prod
-- 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 : 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)
⊢ IsScalarTower S (S × U) U

Tactic:
have : IsScalarTower S (S × U) U := IsScalarTower.of_algebraMap_eq' rfl
-- 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 : IsScalarTower S (S × U) U
⊢ Etale S (S × U)

Tactic:
have : Etale S (S × U) := Etale.of_equiv e
-- 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 : Etale S (S × U)
⊢ Etale S U

Tactic:
.comp S (S × U) U

Premises used: Algebra.Etale.comp, Prod
-- 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 : Etale S (S × U)
⊢ Etale S U

Tactic:
exact .comp S (S × U) U
-- 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 : IsScalarTower S (S × U) U
⊢ Etale S U

Tactic:
have : Etale S U := by
      have : Etale S (S × U) := Etale.of_equiv e
      exact .comp S (S × U) U
-- 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 : Etale S U
⊢ Module.Finite S (S × U)

Tactic:
have : Module.Finite S (S × U) := Module.Finite.equiv e.toLinearEquiv
-- 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 : Module.Finite S (S × U)
⊢ Module.Finite (S × U) U

Tactic:
have : Module.Finite (S × U) U :=
        Module.Finite.of_surjective (Algebra.linearMap (S × U) U) (RingHom.snd S U).surjective
-- 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 (S × U)
this : Module.Finite (S × U) U
⊢ Module.Finite S U

Tactic:
Module.Finite.trans (S × U) _

Premises used: Module.Finite.trans, Prod
-- 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 (S × U)
this : Module.Finite (S × U) U
⊢ Module.Finite S U

Tactic:
exact Module.Finite.trans (S × U) _

Premises used: Module.Finite.trans, Prod
-- 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 : Etale S U
⊢ Module.Finite S U

Tactic:
have : Module.Finite S U := by
      have : Module.Finite S (S × U) := Module.Finite.equiv e.toLinearEquiv
      have : Module.Finite (S × U) U :=
        Module.Finite.of_surjective (Algebra.linearMap (S × U) U) (RingHom.snd S U).surjective
      exact Module.Finite.trans (S × U) _
-- 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 : Module.Finite S U
p : PrimeSpectrum S
⊢ Module.rankAtStalk (S × U) p = n + 1

Tactic:
simp [Module.rankAtStalk_eq_of_equiv e.symm.toLinearEquiv, Module.rankAtStalk_baseChange, hn]

Premises used: AlgEquiv.symm, Module.rankAtStalk_baseChange, Module.rankAtStalk_eq_of_equiv, AlgEquiv.toLinearEquiv
-- 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 : Module.Finite S U
⊢ ∀ (p : PrimeSpectrum S), Module.rankAtStalk (S × U) p = n + 1

Tactic:
have (p : PrimeSpectrum S) : Module.rankAtStalk (R := S) (S × U) p = n + 1 := by
      simp [Module.rankAtStalk_eq_of_equiv e.symm.toLinearEquiv, Module.rankAtStalk_baseChange, hn]
-- 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 : ∀ (p : PrimeSpectrum S), Module.rankAtStalk (S × U) p = n + 1
⊢ ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1

Tactic:
simp_rw [Module.rankAtStalk_prod , Module.rankAtStalk_self, Pi.add_apply, Pi.one_apply] at this

Premises used: Pi.one_apply, Pi.add_apply, Module.rankAtStalk_prod, Module.rankAtStalk_self
-- 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_1 : 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 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
h : ∀ (p : PrimeSpectrum S), Module.rankAtStalk U p = (↑n : (p : PrimeSpectrum S) → ℕ) p
⊢ Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n : (p : PrimeSpectrum S) → ℕ)

Tactic:
ext p
-- 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_1 : 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 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
p : PrimeSpectrum S
h : Module.rankAtStalk U p = n
⊢ Module.rankAtStalk U p = (↑n : (p : PrimeSpectrum S) → ℕ) p

Tactic:
simp only [Pi.natCast_def, Nat.cast_id]

Premises used: Nat.cast_id, Pi.natCast_def
-- 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 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
p : PrimeSpectrum S
⊢ Module.rankAtStalk U p = n

Tactic:
grind
-- 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 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
⊢ Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n : (p : PrimeSpectrum S) → ℕ)

Tactic:
have : Module.rankAtStalk (R := S) U = n := by
      ext p
      simp only [Pi.natCast_def, Nat.cast_id]
      grind
-- 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) → ℕ)
succ :
  ∀ (V : Type u) (w_2 : CommRing V) (w_3 : Algebra S V),
    Module.FaithfullyFlat S V →
      Module.Finite S V →
        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)
⊢ ∃ (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 ⟨V, _, _, _, _, _, hV⟩ := ih this