awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
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) (↑0 : (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)
have h : IsFiniteSplit R (R ⊗[R] S)
Tactic: use R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
Goal:
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) (↑0 : (p : PrimeSpectrum R) → ℕ)
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S
have hn₁ : Subsingleton S
Tactic: rw [Nat.cast_zero, Module.rankAtStalk_eq_zero_iff_subsingleton] at hn
Cleared hypotheses: hn, e
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
Goal:
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) (↑0 : (p : PrimeSpectrum R) → ℕ)
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R (R ⊗[R] S)
have this : IsFiniteSplit R S
Tactic: have : IsFiniteSplit R S := by
      rw [Nat.cast_zero, Module.rankAtStalk_eq_zero_iff_subsingleton] at hn
      exact of_subsingleton_top
-- 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) → ℕ)
⊢ ∃ (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 : Subsingleton 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)
Tactic: cases subsingleton_or_nontrivial R
-- 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) → ℕ)
succ :
  Subsingleton 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)
⊢ ∃ (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₁ : Nontrivial 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)
Tactic: cases subsingleton_or_nontrivial R
-- 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 : Subsingleton 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)
have h : IsFiniteSplit R (R ⊗[R] S)
Tactic: use R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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 : Subsingleton R
⊢ IsFiniteSplit R (R ⊗[R] S)
have this : IsFiniteSplit R S
Tactic: have : IsFiniteSplit R S := .of_subsingleton
-- 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
⊢ Nontrivial S
have apply : LT.lt (α := (p : PrimeSpectrum R) → ℕ) 0 (Module.rankAtStalk S)
Tactic: apply Module.nontrivial_of_rankAtStalk_pos (R := R)
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
⊢ ∃ (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 this : Nontrivial S
Tactic: have : Nontrivial S := by
      apply Module.nontrivial_of_rankAtStalk_pos (R := R)
      simp [hn]
-- 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 : Nontrivial 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)
have 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)
Tactic: obtain ⟨U, _, _, ⟨e⟩⟩ := Algebra.FormallyUnramified.exists_algEquiv_prod R S
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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)
⊢ ∃ (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 this₁ : IsScalarTower S (S × U) U
Tactic: have : IsScalarTower S (S × U) U := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
have this₁ : Etale S (S × U)
Tactic: have : Etale S (S × U) := Etale.of_equiv e
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
⊢ ∃ (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 this₁ : Etale S U
Tactic: have : Etale S U := by
      have : Etale S (S × U) := Etale.of_equiv e
      exact .comp S (S × U) U
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
have this₁ : Module.Finite S (S × U)
Tactic: have : Module.Finite S (S × U) := Module.Finite.equiv e.toLinearEquiv
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
⊢ ∃ (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 this₁ : 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) _
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
⊢ ∃ (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 this₁ : ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
⊢ ∃ (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 this₁ : ∀ (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
Cleared hypotheses: this
-- 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 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
⊢ Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n : (p : PrimeSpectrum S) → ℕ)
have h : ∀ (p : PrimeSpectrum S), Module.rankAtStalk U p = (↑n : (p : PrimeSpectrum S) → ℕ) p
Tactic: ext p
-- 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 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
p : PrimeSpectrum S
⊢ Module.rankAtStalk U p = (↑n : (p : PrimeSpectrum S) → ℕ) p
have h : Module.rankAtStalk U p = n
Tactic: simp only [Pi.natCast_def, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
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
⊢ ∃ (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 this₁ : 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
-- 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) → ℕ)
⊢ ∃ (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 : ∀ (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)
Tactic: obtain ⟨V, _, _, _, _, _, hV⟩ := ih this