mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S✝ : Type u_4
U : Type u_5
V✝ : Type u_6
α : Type u_7
inst✝⁷ : PartialOrder Γ
V : Type u_8
inst✝⁶ : Monoid R
inst✝⁵ : AddMonoid V
inst✝⁴ : DistribMulAction R V
S : Type u_9
inst✝³ : Monoid S
inst✝² : DistribMulAction S V
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
⊢ (r • s) • a = r • s • a

Tactic:
ext
    simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝ : V⟦Γ⟧
⊢ 0 • x✝ = 0

Tactic:
ext
    simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝¹ x✝ : Γ →₀ V
⊢ ofFinsupp (x✝¹ + x✝) = ofFinsupp x✝¹ + ofFinsupp x✝

Tactic:
ext
    simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝¹ : R
x✝ : Γ →₀ V
⊢ ofFinsupp (x✝¹ • x✝) = (RingHom.id R) x✝¹ • ofFinsupp x✝

Tactic:
ext
    simp

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

Goal state before:
pp: case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
hlt : 0 < x
⊢ 0 ≤ (ofLex x).leadingCoeff

Tactic:
exact (leadingCoeff_pos_iff.mpr hlt).le

Goal state after:
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 |y|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).leadingCoeff

Tactic:
leadingCoeff_of_ne_zero (by simpa using hx)

Goal state after:
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 |y|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).leadingCoeff
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex x).orderTop.untop ⋯)

Tactic:
leadingCoeff_of_ne_zero (by simpa using hx)

Goal state after:
Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex x).orderTop.untop ⋯)
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ x * (y ⊔ z) = x * y ⊔ x * z

Tactic:
rw [← iSup_pair, ← sSup_pair, mul_sSup_distrib]

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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
this : (seed.coeff (f.support.min' hsupport)) 0 < (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport))
⊢ (ofLex 0).coeff (f.support.min' hsupport) < (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport))

Tactic:
by
    simpa using! this

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

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

Tactic:
IH,

Goal state after:
case succ
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
IH : mk (x ^ n) = mk (y ^ n)
⊢ mk (y ^ n) + mk x = mk (y ^ n) + mk y
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
hm_lt : m < n + 1
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
refine ⟨m, hm_lt, ?_⟩

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
hm_lt : m < n + 1
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))
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✝¹² : AddCommMonoid Γ
inst✝¹¹ : PartialOrder Γ
inst✝¹⁰ : IsOrderedCancelAddMonoid Γ
inst✝⁹ : PartialOrder Γ'
inst✝⁸ : AddAction Γ Γ'
inst✝⁷ : IsOrderedCancelVAdd Γ Γ'
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Zero R
S : Type u_6
inst✝⁴ : Zero S
inst✝³ : SMul R S
inst✝² : SMulWithZero R V
inst✝¹ : SMulWithZero S V
inst✝ : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
⊢ (r • s) • a = r • s • a

Tactic:
ext
    simp

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : y ≈ z
⊢ z < x → x ≈ z

Tactic:
rw [← Quotient.eq_iff_equiv] at *

Goal state after:
case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : ⟦y⟧ = ⟦z⟧
⊢ z < x → ⟦x⟧ = ⟦z⟧
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single a) r ^ n * (single a) r = (single ((n + 1) • a)) (r ^ n * r)

Tactic:
IH,

Goal state after:
case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single (n • a)) (r ^ n) * (single a) r = (single ((n + 1) • a)) (r ^ n * r)
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inr.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≈ y
h₂ : y ≤ z
⊢ z < x → x ≈ z

Tactic:
rw [← Quotient.eq_iff_equiv] at *

Goal state after:
case inr.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : ⟦x⟧ = ⟦y⟧
h₂ : y ≤ z
⊢ z < x → ⟦x⟧ = ⟦z⟧
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✝⁵ : AddCommMonoid Γ
inst✝⁴ : PartialOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommSemiring R
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
x : A⟦Γ⟧
⊢ r • x = (C.comp (algebraMap R A)) r * x

Tactic:
ext
    simp

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
⊢ (0 ^ (n + 1)).order = (n + 1) • order 0

Tactic:
simp [pow_succ, succ_nsmul, order_pow, pow_ne_zero, *]

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : R⟦Γ⟧
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).order = (n + 1) • x.order

Tactic:
simp [pow_succ, succ_nsmul, order_pow, pow_ne_zero, *]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy : (i : ι) → A i
this : closure (Set.range fun s ↦ star s * s) = pi Set.univ fun i ↦ closure (Set.range fun s ↦ star s * s)
⊢ ∀ (x : (i : ι) → A i),
    (∀ (i : ι), x i ∈ closure (Set.range fun s ↦ star s * s)) →
      xy = xa + x → ∀ (i : ι), ∃ p ∈ closure (Set.range fun s ↦ star s * s), xy i = xa i + p

Tactic:
intro x h rfl i

Goal state after:
case refine_2
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa : (i : ι) → A i
this : closure (Set.range fun s ↦ star s * s) = pi Set.univ fun i ↦ closure (Set.range fun s ↦ star s * s)
x : (i : ι) → A i
h : ∀ (i : ι), x i ∈ closure (Set.range fun s ↦ star s * s)
i : ι
⊢ ∃ p ∈ closure (Set.range fun s ↦ star s * s), (xa + x) i = xa i + p
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
heq : ↑(k • y) - k • x = k • (↑y - x)
⊢ k • (↑y - x) ∈ ball K c

Tactic:
exact Submodule.smul_mem _ _ hy

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬A.valuation ↑a = 1 ↔ A.valuation ↑a < 1

Tactic:
exact (A.valuation_le_one a).lt_iff_ne.symm

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

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x ≤ 1
⊢ x ∈ B

Tactic:
le_iff_lt_or_eq

Goal state after:
case mp
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
⊢ x ∈ B
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a : WithTop α
⊢ 0 ≤ a.untop₀ ↔ 0 ≤ a

Tactic:
by
  cases a with
  | top => tauto
  | coe a => simp

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
h : a.untop₀ ≤ b.untop₀
⊢ a ≤ b

Tactic:
by
  lift a to α using ha
  by_cases hb : b = ⊤
  · simp_all
  lift b to α using hb
  simp_all

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure ↑(upperClosure (s * t)))

Tactic:
UpperSet.upperClosure

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure (s * t))
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
⊢ p.IsMonicOfDegree n ↔ p.natDegree ≤ n ∧ p.coeff n = 1

Tactic:
simp only [isMonicOfDegree_iff']
  refine ⟨fun ⟨H₁, H₂⟩ ↦ ⟨H₁.le, H₁ ▸ Monic.coeff_natDegree H₂⟩, fun ⟨H₁, H₂⟩ ↦ ⟨?_, ?_⟩⟩
  · exact natDegree_eq_of_le_of_coeff_ne_zero H₁ <| H₂ ▸ one_ne_zero
  · exact monic_of_natDegree_le_of_coeff_eq_one n H₁ H₂

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n

Tactic:
exact natTrailingDegree_le_of_ne_zero hp

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

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n

Tactic:
exact natTrailingDegree_le_of_ne_zero hp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ (X ^ m).homogenize n = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)

Tactic:
X_pow_eq_monomial,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ ((monomial m) 1).homogenize n = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), if R a y then IsChain R (a :: destutter' R y l) else IsChain R (destutter' R a l)
⊢ IsChain R (destutter' R a (b :: c :: l))

Tactic:
IH,

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), if R a y then IsChain R (a :: destutter' R y l) else True
⊢ IsChain R (destutter' R a (b :: c :: l))
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ if R a b then if R b c then IsChain R (a :: b :: destutter' R c l) else IsChain R (a :: destutter' R b l)
  else if R a c then IsChain R (a :: destutter' R c l) else IsChain R (destutter' R a l)

Tactic:
IH,

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ if R a b then if R b c then IsChain R (a :: b :: destutter' R c l) else IsChain R (a :: destutter' R b l)
  else if R a c then IsChain R (a :: destutter' R c l) else True
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✝ : IsScalarTower R S S
m n✝ n : ℕ
a : R
⊢ ((monomial n) a).smeval x * x ^ m * x ^ n✝ = ((monomial n) a).smeval x * (x ^ m * x ^ n✝)

Tactic:
rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (0 + v + if m = n then w else 0) = v

Tactic:
if_neg hmn.ne,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ 0 + v + 0 = v
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ #p.support = 3

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
  exact card_support_trinomial hkm hmn u.ne_zero v.ne_zero w.ne_zero

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ∑ i_1 ∈ s, r i_1 * b i_1 %ₘ g i * ∏ x ∈ s, g x +
      ∑ x ∈ s,
        ((r x * b x /ₘ g i + r x * a x /ₘ g x) * (g i * ∏ x ∈ s, g x) +
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k)

Tactic:
← Finset.sum_add_distrib

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ∑ x ∈ s,
      (r x * b x %ₘ g i * ∏ x ∈ s, g x +
        ((r x * b x /ₘ g i + r x * a x /ₘ g x) * (g i * ∏ x ∈ s, g x) +
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k))
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ (aeval r) (sumIDeriv p) = eval r (sumIDeriv (map (algebraMap R A) p))

Tactic:
by
  rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]

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

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + k ∉ Set.Ioo (n + k) (n + n)

Tactic:
exact fun h => h.1.ne rfl

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

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => h.1.ne rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
⊢ P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length

Tactic:
simp [h₅, h₆, natDegree_mul, add_comm 1]

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

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
have hn : n = n' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ←
      hp, ← natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq,
      trinomial_natDegree hkm' hmn' z.ne_zero]

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
hn : n = n'
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ (fun u ↦
        { toFun := fun z ↦ z.re • 1 + z.im • ↑u, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
          commutes' := ⋯ })
      ((fun f ↦ ⟨f ω, ⋯⟩) f) =
    f

Tactic:
ext
    simp

Goal state after: