mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
⊢ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hI2 : I ^ 2 = 0
⊢ IsUnit ↑(2 - 1)!

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ Coe.ringHom ⟨dpow' p n ↑x, ⋯⟩ = (RatAlgebra.dividedPowers ⊤).dpow n (Coe.ringHom x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ (dividedPowers hI2).dpow n a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ DividedPowers (Ideal.span {↑p})

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
hp : IsNilpotent ↑p
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
⊢ (dividedPowers hp hIp).dpow n a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
p : ℕ
inst✝² : CharP A p
inst✝¹ : Fact (Nat.Prime p)
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
⊢ (dividedPowers A p hIp).dpow n a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hinj : Injective ⇑Coe.ringHom
⊢ Coe.ringHom ⟨dpow' p n ↑x, ⋯⟩ = (↑n !)⁻¹ʳ * Coe.ringHom x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
x : R
hx : x ∈ I
⊢ dpow I n x = (↑n !)⁻¹ʳ * x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ ↑n ! = ↑n ! • 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (dividedPowers p).dpow n x = if hx : x ∈ Ideal.span {↑p} then ⟨dpow' p n ↑x, ⋯⟩ else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
this : (↑n !)⁻¹ * ↑n ! = 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ʳ • x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ hI.IsSubDPIdeal (span S) ↔ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ ↑((dividedPowers p).dpow n x) = if x_1 : x ∈ Ideal.span {↑p} then (↑n !)⁻¹ʳ * ↑x ^ n else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
I : Ideal R
inst✝¹ : DecidablePred fun x ↦ x ∈ I
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (dividedPowers I).dpow n x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
⊢ hI.IsSubDPIdeal (J ⊔ K)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ hI.IsSubDPIdeal (iSup J)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
⊢ IsNilpotent x ↔ IsNilpotent x.fst

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsNilpotent (inl r) ↔ IsNilpotent r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : M
⊢ inr x ^ 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : M
⊢ IsNilpotent (inr x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ hI.IsSubDPIdeal (I ⊓ ⨅ i, J i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ hJ.IsSubDPIdeal (Ideal.map f K)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
⊢ IsUnit a ∨ IsNilpotent a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a : TrivSqZeroExt R M
⊢ IsUnit a ∨ IsNilpotent a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
p q : hI.SubDPIdeal
h : (fun s ↦ ↑s.carrier) p = (fun s ↦ ↑s.carrier) q
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₁
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ ε ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
x : R[ε]
⊢ IsNilpotent x ↔ ε ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
h : a + b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
⊢ IsRegular M rs'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
⊢ ∀ x ∈ I, ε ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ ε * r = fst r • ε

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
⊢ fst r ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
⊢ ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I • J
⊢ hI.dpow m x ∈ I • J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⊥
⊢ hI.dpow x✝ x ∈ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
inst✝⁴ : IsLocalRing R
L : Type u_8
inst✝³ : AddCommGroup L
inst✝² : Module R L
inst✝¹ : Module.Finite R L
inst✝ : Nontrivial L
x : R
mem : x ∈ maximalIdeal R
⊢ Nontrivial (QuotSMulTop x L)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x : A
hx : x ∈ ⨅ s ∈ insert ⊤ S, s.carrier
⊢ x ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⨅ s ∈ insert ⊤ S, s.carrier
⊢ hI.dpow x✝ x ∈ ⨅ s ∈ insert ⊤ S, s.carrier

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i ⊆ ↑I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ hI.IsSubDPIdeal (sSup ((fun J ↦ J.carrier) '' S))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
h : (fun J ↦ ⟨J.carrier, ⋯⟩) J = (fun J ↦ ⟨J.carrier, ⋯⟩) J'
⊢ J = J'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ ⟨(J ⊔ J').carrier, ⋯⟩ = ⟨J.carrier, ⋯⟩ ⊔ ⟨J'.carrier, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ ⟨(J ⊓ J').carrier, ⋯⟩ = ⟨J.carrier, ⋯⟩ ⊓ ⟨J'.carrier, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
⊢ ↑(⨆ (_ : J ∈ S), ⟨J.carrier, ⋯⟩) = ⨆ (_ : J ∈ S), ↑⟨J.carrier, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
⊢ I = ⊥ ∨ I = Ideal.span {ε} ∨ I = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
⊢ (Ideal.span {ε}).IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
⊢ Submodule.IsPrincipal I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
a : K[ε]ˣ
⊢ ↑a * (↑a⁻¹ * b) = b ∨ b * (↑a⁻¹ * b) = ↑a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ a * (↑b⁻¹ * a) = ↑b ∨ ↑b * (↑b⁻¹ * a) = a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
⊢ CompleteLattice hI.SubDPIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
this : ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x
⊢ ∃ c, ε * x * c = ε * y ∨ ε * y * c = ε * x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsFiniteSplit R S
⊢ IsFiniteSplit T (T ⊗[R] S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
ι : Type u_4
inst✝ : Finite ι
⊢ ∃ n, Nonempty ((ι → R) ≃ₐ[R] Fin n → R)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
S' : Type u_4
inst✝² : CommRing S'
inst✝¹ : Algebra R S'
e : S ≃ₐ[R] S'
inst✝ : IsFiniteSplit R S
⊢ IsFiniteSplit R S'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Subsingleton R
⊢ IsFiniteSplit R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit R S
⊢ Module.Free R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit R S
⊢ Module.FinitePresentation R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit R S
⊢ Etale R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
inst✝⁴ : Field k
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsFiniteSplit k R
p : Ideal R
inst✝ : p.IsPrime
⊢ Function.Bijective ⇑(algebraMap k (R ⧸ p))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
f : R →ₐ[k] k
⊢ (fun p ↦ (↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm).comp (Ideal.Quotient.mkₐ k p.asIdeal))
      ((fun f ↦ { asIdeal := RingHom.ker f, isPrime := ⋯ }) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ (fun f ↦ { asIdeal := RingHom.ker f, isPrime := ⋯ })
      ((fun p ↦ (↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm).comp (Ideal.Quotient.mkₐ k p.asIdeal)) p) =
    p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
inst✝² : IsSepClosed k
inst✝¹ : EssFiniteType k R
inst✝ : FormallyEtale k R
⊢ IsFiniteSplit k R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑0
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x✝ : ℕ
hn : x✝ ≠ 0
⊢ hI.dpow x✝ 0 ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ WeaklyEtale (ULift.{u₁, u_1} R) (ULift.{u₂, u_2} S) ↔ WeaklyEtale R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Etale R S
⊢ (TensorProduct.lmul' R).Flat

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
⊢ TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
⊢ Nontrivial S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
⊢ (TensorProduct.lmul' T).Flat

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this : IsScalarTower S (S × U) U
⊢ Etale S U

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
⊢ TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R) =
    (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
        (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝¹ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝ : IsScalarTower S (S × U) U
this : Etale S U
⊢ Module.Finite S U

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝² : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝¹ : IsScalarTower S (S × U) U
this✝ : Etale S U
this : Module.Finite S U
p : PrimeSpectrum S
⊢ Module.rankAtStalk (S × U) p = n + 1

Tactic:
by

Goal state after: