mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝³ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this✝ : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
this : IsLocalization.AtPrime R₁ P
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat

Tactic:
have h : Function.Bijective (algebraMap R₂ R₁) :=
    (Localization.algEquiv P.primeCompl R₁).bijective

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝³ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this✝ : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
this : IsLocalization.AtPrime R₁ P
h : Function.Bijective ⇑(algebraMap R₂ R₁)
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r

pp: case add_single.hD
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ Function.Injective ⇑toLex

pp: case add_single.hadd
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ), toLex (a1 + a2) = toLex a1 + toLex a2

Tactic:
ih

Goal state after:
case add_single
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ r = r

case add_single.hD
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ Function.Injective ⇑toLex

case add_single.hadd
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ), toLex (a1 + a2) = toLex a1 + toLex a2
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
⊢ ∃ d, (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0

Tactic:
by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ (coeff m) φ = 0

Tactic:
coeff_of_lt_order

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ 0 = 0

case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ ↑(Finsupp.degree m) < φ.order
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
⊢ a.1 + a.2 = k ∧ a.1 < k ∧ ¬0 < a.1 → a = (0, k)

Tactic:
rintro ⟨ha, ⟨_, ha0⟩⟩

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left✝ : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, k)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.C a * ∏ a, MvPolynomial.X a ^ v a))).natDegree = ∑ i, r i * v i

Tactic:
simp only [Fin.prod_univ_succ, Fin.sum_univ_succ, map_mul, map_prod, map_pow,
    AlgEquiv.ofAlgHom_apply, MvPolynomial.aeval_C, MvPolynomial.aeval_X, if_pos, Fin.succ_ne_zero,
    ite_false, one_smul, map_add, finSuccEquiv_X_zero, finSuccEquiv_X_succ, algebraMap_eq]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a) *
        (Polynomial.X ^ v 0 *
          ∏ x, (Polynomial.C (MvPolynomial.X x) + Polynomial.X ^ up ^ ↑x.succ) ^ v x.succ)).natDegree =
    up ^ ↑0 * v 0 + ∑ i, up ^ ↑i.succ * v i.succ
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittOne p 0 = 1

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittOne, wittStructureRat, xInTermsOfW_zero, map_one, bind₁_X_right,
    map_wittStructureInt]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case succ
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m : ℕ
ih : ∀ (n : ℕ), (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + m)) f
n : ℕ
⊢ (coeffMonoidHom M p (n + 1)) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + (m + 1))) f

Tactic:
ih

Goal state after:
case succ
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m : ℕ
ih : ∀ (n : ℕ), (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + m)) f
n : ℕ
⊢ (coeffMonoidHom M p (n + 1 + m)) f = (coeffMonoidHom M p (n + (m + 1))) f
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n✝ n : ℕ
ih : (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
⊢ (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f

Tactic:
ih

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n✝ n : ℕ
ih : (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
⊢ (coeffMonoidHom M p m) f = (coeffMonoidHom M p m) f
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m✝ m : ℕ
ih : (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f
⊢ (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f

Tactic:
ih

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m✝ m : ℕ
ih : (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f
⊢ (coeffMonoidHom M p n) f = (coeffMonoidHom M p n) f
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ ((⇑verschiebung)^[n] x).coeff m' = 0

Tactic:
ih

Goal state after:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ 0 = 0

case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : v ↑p = 0
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

pp: case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : ¬v ↑p = 0
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

Tactic:
· rw [hvp]; exact zero_le

Goal state after:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : ¬v ↑p = 0
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
n : ℕ
hfn : (coeff n) f ≠ 0
h : ∃ n, (coeff n) f ≠ 0
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff n) f) ^ p ^ n

Tactic:
valAux,

Goal state after:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
n : ℕ
hfn : (coeff n) f ≠ 0
h : ∃ n, (coeff n) f ≠ 0
⊢ (if h : ∃ n, (coeff n) f ≠ 0 then ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h else 0) =
    ModP.preVal K v O p ((coeff n) f) ^ p ^ n
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ ((⇑frobenius)^[i] x).coeff k ^ p = x.coeff k ^ p ^ (i + 1)

Tactic:
ih

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ (x.coeff k ^ p ^ i) ^ p = x.coeff k ^ p ^ (i + 1)
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this✝ : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i ↦ ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i ↦ ¬P i) x) = (ghostComponent n) x

Tactic:
apply_fun aeval x.coeff at this
    simpa only [map_add, aeval_bind₁, ← coeff_select]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : Fin n
⊢ coeff i 0 = 0

Tactic:
change coeff i (truncateFun _ 0 : TruncatedWittVector p n R) = 0

Goal state after:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : Fin n
⊢ coeff i (truncateFun n 0) = 0
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case neg
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
hn : ¬P n
⊢ 0 = x.coeff n

Tactic:
rw [(h n).resolve_right hn]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ constantCoeff (subst (f - 1) (log A)) = 0

Tactic:
have h : MvPowerSeries.constantCoeff (f - 1 : A⟦X⟧) = 0 := by
    rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
h : MvPowerSeries.constantCoeff (f - 1) = 0
⊢ constantCoeff (subst (f - 1) (log A)) = 0
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
inst✝ : FaithfullyFlat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsRegular M rs
⊢ ⊤ ≠ Ideal.ofList (List.map (⇑(algebraMap R S)) rs) • ⊤

Tactic:
rw [← Ideal.map_ofList]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
inst✝ : FaithfullyFlat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsRegular M rs
⊢ ⊤ ≠ Ideal.map (algebraMap R S) (Ideal.ofList rs) • ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

Tactic:
coeff_of_lt_order p.1 ?_

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ 0 * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ ↑p.1 < ((map (IsLocalRing.residue A)) g).order
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this✝ : IsSimpleModule R ↥(inclusion hN).range
this : IsSemisimpleModule R ↥(⨆ i ∈ s, i)
⊢ ⨆ a ∈ s, comap (⨆ i ∈ s, i).subtype a = ⊤

Tactic:
biSup_comap_subtype_eq_top

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this✝ : IsSimpleModule R ↥(inclusion hN).range
this : IsSemisimpleModule R ↥(⨆ i ∈ s, i)
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
⊢ Disjoint ↑pc ↑p

Tactic:
simpa [pc, q] using! Set.disjoint_image_left.mpr
      (Set.disjoint_compl_left_iff_subset.mpr (fun _ a ↦ a))

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ IsSemisimpleRing R ∧ (∀ (N : Submodule R R), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R

Tactic:
isFullyInvariant_iff_isTwoSided,

Goal state after:
case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Ring R
left✝¹ : IsSemisimpleRing R
right✝ : Nontrivial R
x✝ : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left✝ : ∀ (N : Submodule R R), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤
⊢ IsSimpleRing R ∧ IsArtinianRing R

Tactic:
isFullyInvariant_iff_isTwoSided,

Goal state after:
case refine_2
R : Type u
inst✝ : Ring R
left✝¹ : IsSemisimpleRing R
right✝ : Nontrivial R
x✝ : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left✝ : ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ IsSimpleRing R ∧ IsArtinianRing R
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
by
  have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun
  refine ⟨n, hn, S, hS, ⟨.trans (.opOp R₀ R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
  exact .trans (.moduleEndSelf R₀) <| .trans (e.conjAlgEquiv R₀) (endVecAlgEquivMatrixEnd ..)

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_algEquiv_matrix_end_mulOpposite R₀ R

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Ring R
inst✝³ : Algebra R₀ R
inst✝² : IsSimpleRing R
inst✝¹ : IsArtinianRing R
inst✝ : Module.Finite R₀ R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_algEquiv_matrix_end_mulOpposite R₀ R

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Ring R
inst✝³ : Algebra R₀ R
inst✝² : IsSimpleRing R
inst✝¹ : IsArtinianRing R
inst✝ : Module.Finite R₀ R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ Ideal.map (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp

Tactic:
Ideal.map_le_iff_le_comap

Goal state after:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ v.supp ≤ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp