mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
⊢ ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f

Tactic:
obtain ⟨m₁, m₂, _, _, hm₁m₂⟩ := (not_isLocalRing_tfae.out 0 2).mp h
  let e := Ideal.quotientInfEquivQuotientProd m₁ m₂ <| Ideal.isCoprime_of_isMaximal hm₁m₂
  let f := e.toRingHom.comp <| Ideal.Quotient.mk (m₁ ⊓ m₂)
  use R ⧸ m₁, R ⧸ m₂, Ideal.Quotient.field m₁, Ideal.Quotient.field m₂, f
  apply Function.Surjective.comp e.surjective Ideal.Quotient.mk_surjective

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i (sumSMulX c)
⊢ IsUnit r

Tactic:
apply hc_gcd

Goal state after:
case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i (sumSMulX c)
⊢ ∀ (i : n), r ∣ c i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ ∃ f, Valued.v f = Valued.v x

Tactic:
use RatFunc.X ^ (-log (Valued.v x))

Goal state after:
case h
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ Valued.v (RatFunc.X ^ (-(Valued.v x).log)) = Valued.v x
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = 0

Tactic:
restrict₀_eq_zero_iff

Goal state after:
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(MonoidWithZeroHom.ofClass Valued.v) x = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y, f (x, y) =
    ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)

Tactic:
refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a) ∈ {a ∈ antidiagonal k | a.1 < k}

case refine_2
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, a.1 ∈ range k

case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a).1 = a

case refine_4
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, (a.1, k - a.1) = a

case refine_5
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, ∑ x ∈ powersetCard a univ, ∑ y, f (x, y) = ∑ A ∈ powersetCard (a, k - a).1 univ, ∑ j, f (A, j)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ antidiagonal k
x : σ
x✝ : x ∈ univ
⊢ ∑ x_1 ∈ powersetCard a.1 univ, ((-1) ^ #x_1 * ∏ a ∈ x_1, X a) * X x ^ (k - #x_1) =
    ∑ i ∈ powersetCard a.1 univ, ((-1) ^ a.1 * ∏ a ∈ i, X a) * X x ^ a.2

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ antidiagonal k
x : σ
x✝ : x ∈ univ
s : Finset σ
hs : s ∈ powersetCard a.1 univ
⊢ ((-1) ^ #s * ∏ a ∈ s, X a) * X x ^ (k - #s) = ((-1) ^ a.1 * ∏ a ∈ s, X a) * X x ^ a.2
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ∑ a ∈ antidiagonal k with a.1 < k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ t ∈ pairs σ k with #t.1 < k, weight σ R k t

Tactic:
by
  rw [← sum_congr rfl (fun a ha ↦ esymm_mul_psum_summand_to_weight σ R k a (mem_filter.mp ha).left),
    sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum σ R k]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
this : Commute (diagonal fun x ↦ r) (single i i 1)
⊢ single i i 1 • r • x = r • single i i 1 • x

Tactic:
← smul_assoc r,

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
this : Commute (diagonal fun x ↦ r) (single i i 1)
⊢ single i i 1 • r • x = (r • single i i 1) • x
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
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
m : σ →₀ ℕ
hm : p • m = n
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

Tactic:
rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
not_le : ¬p • m ≤ p • n
⊢ (if p • m ≤ p • n then (coeff (p • m)) ((expand p hp) φ) else 0) =
    MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
if_neg not_le,

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
not_le : ¬p • m ≤ p • n
⊢ 0 = MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) ((trunc' R n) φ))
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
⊢ degreeOf 0 ((T f) ((MvPolynomial.monomial v) a)) = ∑ i, r i * v i

Tactic:
by
  rw [← natDegree_finSuccEquiv, monomial_eq, Finsupp.prod_pow v fun a ↦ X a]
  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]
  have h (i : Fin n) :
      (Polynomial.C (X (R := k) i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0 :=
    pow_ne_zero (v i.succ) (leadingCoeff_ne_zero.mp <| by simp [add_comm, leadingCoeff_X_pow_add_C])
  rw [natDegree_mul (by simp [ha]) (mul_ne_zero (by simp) (Finset.prod_ne_zero_iff.mpr
    (fun i _ ↦ h i))), natDegree_mul (by simp) (Finset.prod_ne_zero_iff.mpr (fun i _ ↦ h i)),
    natDegree_prod _ _ (fun i _ ↦ h i), natDegree_finSuccEquiv, degreeOf_C]
  simpa only [natDegree_pow, zero_add, natDegree_X, mul_one, Fin.val_zero, pow_zero, one_mul,
    add_right_inj] using Finset.sum_congr rfl (fun i _ ↦ by
    rw [add_comm (Polynomial.C _), natDegree_X_pow_add_C, mul_comm])

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ wittPolynomial p R n = ∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i)

Tactic:
apply sum_congr rfl
  rintro i -
  rw [monomial_eq, Finsupp.prod_single_index]
  rw [pow_zero]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I =
    Ideal.map (↑(MvPolynomial.finSuccEquiv k n).symm) (Ideal.map (MvPolynomial.finSuccEquiv k n) (Ideal.map (T f) I))

Tactic:
set g := (finSuccEquiv k n)

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
⊢ Ideal.map (T f) I = Ideal.map (↑g.symm) (Ideal.map g (Ideal.map (T f) I))
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ I = Ideal.map ((T f).symm.toRingEquiv.toRingHom.comp ↑(T f)) I

Tactic:
by
      have : (T f).symm.toRingEquiv.toRingHom.comp (T f) = RingHom.id _ :=
        RingEquiv.symm_toRingHom_comp_toRingHom _
      rw [this, Ideal.map_id]

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ (map f) x = 0 ↔ ∀ (n : ℕ), f (x.coeff n) = 0

Tactic:
refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
  · apply_fun (·.coeff n) at h
    simpa using h
  · ext n
    simpa using h n

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
⊢ x.2 < n + 1

Tactic:
obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
hx' : x ∈ ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
⊢ x.2 < n + 1
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ (↑p ^ i).coeff i = 1

Tactic:
induction i with

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
j : ℕ
hj : j ≠ 0
⊢ (↑p ^ 0).coeff j = 0

Tactic:
rw [pow_zero, one_coeff_eq_of_pos]

Goal state after:
case zero.hn
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
j : ℕ
hj : j ≠ 0
⊢ 0 < j
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
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
⊢ (↑p ^ (i + 1)).coeff j = 0

Tactic:
| succ i hi =>

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

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

Tactic:
induction i with

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

Goal state before:
pp: case refine_3
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 : ℕ
⊢ (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i ↦ ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n

Tactic:
simp only [wittPolynomial_eq_sum_C_mul_X_pow, selectPoly, map_sum, map_pow, map_mul,
    bind₁_X_right, bind₁_C_right, ← Finset.sum_add_distrib, ← mul_add]

Goal state after:
case refine_3
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 : ℕ
⊢ ∑ x ∈ Finset.range (n + 1),
      C ↑p ^ x * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) =
    ∑ x ∈ Finset.range (n + 1), C ↑p ^ x * X x ^ p ^ (n - x)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0

Tactic:
have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring

Goal state after:
case succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsDomain R[X] ↔ IsDomain R ∧ IsCancelAdd R

Tactic:
simp_rw [isDomain_iff_cancelMulZero_and_nontrivial, nontrivial_iff,
    Polynomial.isCancelMulZero_iff, and_right_comm]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case p1
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (match d - rootMultiplicity 1 p - 1 + 1 with
        | 0 => 0
        | d.succ =>
          ∑ i ∈ (q * (-1) ^ rootMultiplicity 1 p).support,
            (q * (-1) ^ rootMultiplicity 1 p).coeff i • preHilbertPoly F d i).coeff
      (d - rootMultiplicity 1 p - 1) ≠
    0

Tactic:
· have : (fun (x : ℕ) (a : F) => a) = fun x a => a * 1 ^ x := by simp only [one_pow, mul_one]
    simp only [finsetSum_coeff, coeff_smul, smul_eq_mul, coeff_preHilbertPoly_self,
      ← Finset.sum_mul, ← sum_def _ (fun _ a => a), this, ← eval_eq_sum, eval_mul, eval_pow,
      eval_neg, eval_one, _root_.mul_eq_zero, pow_eq_zero_iff', neg_eq_zero, one_ne_zero, ne_eq,
      false_and, or_false, inv_eq_zero, cast_eq_zero, not_or]
    exact ⟨(not_iff_not.2 dvd_iff_isRoot).1 hq2, factorial_ne_zero _⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ c = a * x1 * x2

Tactic:
simpa [leadingCoeff, hp_natDegree, p, hroots, mul_assoc, add_comm x1] using
    coeff_eq_esymm_roots_of_card hp_roots_card (k := 0) (by simp [hp_natDegree])

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp : (f.rootSet S).ncard ≤ (⇑π '' f.rootSet S).ncard + 1
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
Set.ncard_le_ncard_image_add_one_iff

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
P : { P // P.FG }
u : ↥↑P ⊗[R] N
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) P) u) =
    (rTensor N (↑P).subtype) u

Tactic:
suffices (Submodule.FG.rTensor.directLimit R M N).toLinearMap.comp
      (Module.DirectLimit.of R {P : Submodule R M // P.FG} (fun P ↦ P.val ⊗[R] N)
        (fun _ _ hPQ ↦ rTensor N (Submodule.inclusion hPQ)) P)
      = rTensor N (Submodule.subtype P.val) by
    exact DFunLike.congr_fun this u
  ext p n
  simp [Submodule.FG.rTensor.directLimit, Submodule.FG.directLimit]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (1 + X).logOf = log A

Tactic:
logOf_eq,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ subst (1 + X - 1) (log A) = log A
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = f.toFun' S (1 ⊗ₜ[R] x)

Tactic:
rw [ground_apply]
  convert! f.isCompat_apply' (Algebra.algHom R R S) (1 ⊗ₜ[R] x)
  · simp only [includeRight_lid]
  · rw [rTensor_tmul, toLinearMap_apply, map_one]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
⊢ (map (Ideal.Quotient.mk I)) ↑f * (map (Ideal.Quotient.mk I)) h ≠ 0

Tactic:
← Polynomial.polynomial_map_coe,

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
⊢ ↑(Polynomial.map (Ideal.Quotient.mk I) f) * (map (Ideal.Quotient.mk I)) h ≠ 0
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
refine ⟨fun ⟨_, _⟩ ↦ ?_, fun ⟨_, _, _⟩ ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

case refine_2
R : Type u
inst✝ : Ring R
x✝ : IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
left✝¹ : IsSemisimpleRing R
left✝ : IsIsotypic R R
right✝ : Nontrivial R
⊢ IsSimpleRing R ∧ IsArtinianRing R
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
inst✝ : IsSemisimpleModule R M
m : Submodule R M
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s

Tactic:
refine ⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩ ⊆ isotypicComponents R M

case refine_2
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ m = sSup (Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩)

case refine_3
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
⊢ (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
remainder

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)

Tactic:
simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ AddCommute o₁ o₂ ↔ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
refine ⟨fun hcomm ↦ ?_, ?_⟩

Goal state after:
case refine_1
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

case refine_2
o₁ o₂ : Ordinal.{u_1}
⊢ (∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂) → AddCommute o₁ o₂
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
n₁ n₂ : ℕ
⊢ AddCommute (o * ↑n₁) (o * ↑n₂)

Tactic:
addCommute_iff_eq,

Goal state after:
case refine_2
o : Ordinal.{u_1}
n₁ n₂ : ℕ
⊢ o * ↑n₁ + o * ↑n₂ = o * ↑n₂ + o * ↑n₁
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ Monotone (lfpApprox f)

Tactic:
intro x₁

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ : α
⊢ ∀ ⦃b : α⦄, x₁ ≤ b → lfpApprox f x₁ ≤ lfpApprox f b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
hba : b ≤ a
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
| inr hba =>

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : IsMin a
⊢ IsOpen[inst✝³] {a}

Tactic:
convert! isOpen_Iio (a := Order.succ a) using 1

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : IsMin a
⊢ {a} = Iio (Order.succ a)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case hc
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ 0 < ω

Tactic:
exact omega0_pos

Goal state after: