mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀
⊢ x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Goal state after:
case inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
⊢ 0 ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

case inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
x : N₀ˣ
⊢ ↑x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : NonemptyInterval α
h : s.toProd = t.toProd
⊢ s = t

Tactic:
by cases s; cases t; congr

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
f : (i : ι) → κ i → Interval α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
coe_iInf

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
⊢ (truncLT c) (x + y) = (truncLT c) x + (truncLT c) y

Tactic:
ext i
  by_cases h : i < c <;> simp [h]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop y.orderTop ≤ (x - y).orderTop

Tactic:
rw [sub_eq_add_neg, ← orderTop_neg (x := y)]
  exact min_orderTop_le_orderTop_add

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hlt : x < 0
hlt' : (ofLex x).leadingCoeff < 0
⊢ (ofLex (-x)).leadingCoeff = |(ofLex x).leadingCoeff|

Tactic:
abs_eq_neg_self.mpr hlt'.le,

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hlt : x < 0
hlt' : (ofLex x).leadingCoeff < 0
⊢ (ofLex (-x)).leadingCoeff = -(ofLex x).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

Tactic:
obtain hjlt | hjeq | hjgt := lt_trichotomy (WithTop.some j) (ofLex |x|).orderTop

Goal state after:
case inr.mp.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjlt : ↑j < (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

case inr.mp.inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjeq : ↑j = (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

case inr.mp.inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjgt : (ofLex |x|).orderTop < ↑j
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjlt : ↑j < (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

Tactic:
have hjlt' : j < (ofLex |y|).orderTop := h'.symm ▸ hjlt
      simp [coeff_eq_zero_of_lt_orderTop hjlt, coeff_eq_zero_of_lt_orderTop hjlt'] at hi

Goal state after:
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ Covariant α α (fun x1 x2 ↦ x1 * x2) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro _

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ : α
⊢ ∀ {n₁ n₂ : α},
    (fun x1 x2 ↦ x1 ≤ x2) n₁ n₂ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 * x2) m✝ n₁) ((fun x1 x2 ↦ x1 * x2) m✝ n₂)
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ Covariant α α (swap fun x1 x2 ↦ x1 * x2) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro _

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ : α
⊢ ∀ {n₁ n₂ : α},
    (fun x1 x2 ↦ x1 ≤ x2) n₁ n₂ →
      (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₁) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₂)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Subsingleton R
⊢ order 1 = 0

Tactic:
rw [Subsingleton.elim (1 : R⟦Γ⟧) 0, order_zero]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoidWithOne R
⊢ ↑0 = 0

Tactic:
by simp [← single_zero_natCast]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoidWithOne R
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
by simp [← single_zero_natCast]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
⊢ 0 • mk x = 0

Tactic:
| mk x =>

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
⊢ (n + 1) • mk x = n • mk x + mk x

Tactic:
| mk x =>

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
⊢ ⊤ + mk x = ⊤

Tactic:
| mk x =>

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
⊢ mk x ≠ ⊤ → IsAddLeftRegular (mk x)

Tactic:
| mk x =>

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x : R
⊢ 0 • mk x = 0

Tactic:
| mk x =>

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr.left
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ 0 + (↑y).orderTop = 0

Tactic:
hy.1,

Goal state after:
case inr.left
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ 0 + 0 = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range

Tactic:
by
  -- decompose `x` to `stratum`
  have hmem : x.val ∈ seed.baseEmbedding.domain := x.prop
  simp_rw [seed.domain_baseEmbedding] at hmem
  obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ _).mp hmem
  -- Truncating in the codomain is the same as truncating away some submodule
  let f' : Π₀ (i : FiniteArchimedeanClass M), seed.stratum i :=
    DFinsupp.mk f.support fun d ↦ if c.val ≤ d.val then 0 else f d.val
  refine ⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩
  · rw [seed.domain_baseEmbedding, ArchimedeanStrata.baseDomain,
      Submodule.mem_iSup_iff_exists_dfinsupp']
    use f'
  apply_fun ofLex
  rw [ofLex_toLex, LinearPMap.toFun_eq_coe]
  ext d
  rw [seed.coeff_baseEmbedding rfl]
  unfold f'
  obtain hdc | hdc := lt_or_ge d c
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc,
      seed.coeff_baseEmbedding hf.symm]
    apply congrArg
    have hcd : ¬ c.val ≤ d.val := not_le_of_gt hdc
    simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
    aesop
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc]
    have hcd : c.val ≤ d.val := hdc
    simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
    convert! LinearMap.map_zero _
    simp

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
⊢ (Function.support (f.evalCoeff x)).IsWF

Tactic:
rw [Set.isWF_iff_no_descending_seq]

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
⊢ ∀ (f_1 : ℕ → FiniteArchimedeanClass M), StrictAnti f_1 → ¬∀ (n : ℕ), f_1 n ∈ Function.support (f.evalCoeff x)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
hmem' : ∀ (n : ℕ), seq n ∈ Function.support (ofLex (↑↑f y)).coeff
hwf : True
⊢ ¬(ofLex (↑↑f y)).support.IsWF

Tactic:
rw [Set.isWF_iff_no_descending_seq]

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
hmem' : ∀ (n : ℕ), seq n ∈ Function.support (ofLex (↑↑f y)).coeff
hwf : True
⊢ ¬∀ (f_1 : ℕ → FiniteArchimedeanClass M), StrictAnti f_1 → ¬∀ (n : ℕ), f_1 n ∈ (ofLex (↑↑f y)).support
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
⊢ A = B ∨ B = ⊤

Tactic:
obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top (A.primeSpectrumEquiv.symm ⟨B, hle⟩)
  all_goals
    replace h := congr(primeSpectrumEquiv A $h)
    simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
by_cases h_2 : 1 + x = 0

Goal state after:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
h_2 : 1 + x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
⊢ x ∈ B
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : a • s = s
b : α
⊢ a • b ∈ s ↔ b ∈ s

pp: case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ a • s = s

Tactic:
· rw [← (smul_mem_smul_set_iff : a • b ∈ _ ↔ _), h]

Goal state after:
case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ a • s = s
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
x y : R
⊢ mk (FiniteElement.mk (f (x + y)) ⋯) = mk (FiniteElement.mk (f x) ⋯) + mk (FiniteElement.mk (f y) ⋯)

Tactic:
simp_rw [map_add]

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
x y : R
⊢ mk (FiniteElement.mk (f x + f y) ⋯) = mk (FiniteElement.mk (f x) ⋯) + mk (FiniteElement.mk (f y) ⋯)
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = evalEval x x✝

Tactic:
rw [← coe_evalEvalRingHom, evalEvalRingHom_eq, coe_eval₂RingHom]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : q = 0
⊢ 0 < 0 ↔ p.degree < q.degree

Tactic:
simp only [hp, hq, lt_self_iff_false]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial
R : Type u_2
inst✝ : CommRing R
n : ℕ
p : R[X]
⊢ (MvPolynomial.pderiv 0) ((equivMvPolynomial R) ((monomial n) p)) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs ((monomial n) p)))

Tactic:
| monomial n p =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (MvPolynomial.pderiv 1) ((equivMvPolynomial R) ((monomial n) p)) = (equivMvPolynomial R) (derivative ((monomial n) p))

Tactic:
| monomial n p =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
rcases subsingleton_or_nontrivial R with h | h

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Subsingleton R
⊢ (p.comp q).IsMonicOfDegree (m * n)

case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (m * n)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
⊢ StrictMono ⇑(LinearMap.codRestrict ⊤ LinearMap.id ⋯)

Tactic:
intro _

Goal state after:
case refine_1
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
a✝ : M
⊢ ∀ ⦃b : M⦄, a✝ < b → (LinearMap.codRestrict ⊤ LinearMap.id ⋯) a✝ < (LinearMap.codRestrict ⊤ LinearMap.id ⋯) b
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ p.mirror.coeff n = 0

Tactic:
exact coeff_eq_zero_of_lt_natTrailingDegree (by rwa [mirror_natTrailingDegree])

Goal state after:
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ 1 • x ^ 0 = 1 • x ^ 0

Tactic:
simp only [one_smul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ x * a • x ^ n = x * ((monomial n) a).smeval x

Tactic:
smeval_monomial

Goal state after:
case monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ x * a • x ^ n = x * a • x ^ n
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
by
  have hp0 : p ≠ 0 := by rintro rfl; rw [natDegree_zero] at hp2; cases hp2
  rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
      mul_comm, roots_C_mul]
  · exact inv_ne_zero (leadingCoeff_ne_zero.mpr hp0)
  · rwa [natDegree_mul_leadingCoeff_inv _ hp0]
  · rwa [natDegree_mul_leadingCoeff_inv _ hp0]

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)

Tactic:
by
  refine ⟨fun hp => ⟨hp.card_support_eq_three, fun k => hp.coeff_isUnit⟩, fun hp => ?_⟩
  obtain ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩ := card_support_eq_three.mp hp.1
  rw [support_trinomial hkm hmn hx hy hz] at hp
  replace hx := hp.2 k (mem_insert_self k {m, n})
  replace hy := hp.2 m (mem_insert_of_mem (mem_insert_self m {n}))
  replace hz := hp.2 n (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n)))
  simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz
  rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx
  rw [if_neg hkm.ne', if_neg hmn.ne] at hy
  rw [if_neg (hkm.trans hmn).ne', if_neg hmn.ne'] at hz
  simp_rw [mul_zero, zero_add, add_zero] at hx hy hz
  exact ⟨k, m, n, hkm, hmn, hx.unit, hy.unit, hz.unit, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
use 0
      rw [natDegree_zero]
      use Nat.zero_le _
      intro r ⟨p', hp⟩
      rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]

Goal state after: