mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ limsup s atTop = {ω | Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun x ↦ r) ω) atTop atTop}

Tactic:
← Nat.cofinite_eq_atTop,

Goal state after:
α : Type u_1
R : Type u_2
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ limsup s cofinite = {ω | Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun x ↦ r) ω) atTop atTop}
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b c : MulArchimedeanOrder M
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
by
    intro ⟨m, hm⟩ ⟨n, hn⟩
    use m * n
    rw [pow_mul]
    exact hn.trans (pow_le_pow_left' hm n)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x | τ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g (τ i)

Tactic:
obtain rfl | hxy := eq_or_ne x y

Goal state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx hy : x ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) x
hfxy : f x < f x
τ : Perm ι := Equiv.trans (Equiv.swap x x) σ
hτs : {x | τ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g (τ i)

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x | τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
⊢ ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g (τ i)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
c : MulArchimedeanClass M
hA : c ≠ ⊤
⊢ a ∈ c.ballSubgroup ↔ c < mk a

Tactic:
simp [hA]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : (i : ι) → AddCommMonoid (π i)
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → SMulZeroClass α (π i)
inst✝ : (i : ι) → CeilDiv α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
⊢ (fun i ↦ f i ⌈/⌉ a) = 0

Tactic:
ext i; exact ceilDiv_of_nonpos ha _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f✝ : ι →₀ β
a✝ a : α
ha : a ≤ 0
f : ι →₀ β
⊢ mapRange (fun x ↦ x ⌈/⌉ a) ⋯ f = 0

Tactic:
ext i; exact ceilDiv_of_nonpos ha _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
rw [← sub_pos] at hb

Goal state after:
case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
p q : GroupCone G
h : (fun C ↦ C.carrier) p = (fun C ↦ C.carrier) q
⊢ p = q

Tactic:
cases p; cases q; congr; exact SetLike.ext' h

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
simpa [pred_eq_sub_one] using insert_Ioc_left_eq_Ioc_pred_of_not_isMin h ha

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

Goal state before:
pp: case refine_1
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.1 = (-t + -s).toProd.1

Tactic:
exact neg_add_rev _ _

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

Goal state before:
pp: case refine_2
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.2 = (-t + -s).toProd.2

Tactic:
exact neg_add_rev _ _

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff x.order = 0

Tactic:
rw [order_of_ne hx]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff (⋯.min ⋯) = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < x.order

Tactic:
rw [order_of_ne hx]

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hi : i < x.order
⊢ x.coeff i = 0

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)
  · simp
  contrapose! hi
  rw [← mem_support] at hi
  rw [order_of_ne hx]
  exact Set.IsWF.not_lt_min _ _ hi

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

Goal state before:
pp: case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ g ∈ x.support

Tactic:
have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]

Goal state after:
case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g
⊢ g ∈ x.support
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✝ : AddCommMonoid R
x y : R⟦Γ⟧
x✝ : Γ
⊢ (x + y).coeff x✝ = (y + x).coeff x✝

Tactic:
apply add_comm

Goal state after:
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|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ ↑j < (ofLex |y|).orderTop

Tactic:
simpa [← h] using hj

Goal state after:
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|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ ↑j < (ofLex |x|).orderTop

Tactic:
simpa using hj

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : RingCone R
h : (fun C ↦ C.carrier) p = (fun C ↦ C.carrier) q
⊢ p = q

Tactic:
cases p; cases q; congr; exact SetLike.ext' h

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℤ
⊢ f ↑n ≤ 1

Tactic:
obtain ⟨a, rfl | rfl⟩ := Int.eq_nat_or_neg n <;>
  simp [apply_natCast_le_one hna]

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ 0
y z : R
hyz : (fun x_1 ↦ mk x + x_1) (mk y) = (fun x_1 ↦ mk x + x_1) (mk z)
⊢ mk y = mk z

Tactic:
| mk z =>

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

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b → a1 = a ∧ a2 = b

Tactic:
rintro ⟨_, rfl, h1⟩
      exact ⟨add_right_cancel h1, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : RingPreordering R
h : (fun P ↦ (↑P).carrier) p = (fun P ↦ (↑P).carrier) q
⊢ p = q

Tactic:
cases p; cases q; congr; exact SetLike.ext' h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝⁴ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝³ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝² : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝¹ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this✝ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
⊢ False

Tactic:
cases (by aesop : x ∈ P ∨ -x ∈ P) <;> simp_all [mem_support]

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

Goal state before:
pp: case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ IsUnit ⟨x⁻¹, ⋯⟩

Tactic:
refine .of_mul_eq_one (⟨x, hx⟩ : S) ?_

Goal state after:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ⟨x⁻¹, ⋯⟩ * ⟨x, hx⟩ = 1
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 : x ∈ A
⊢ x ∈ B

Tactic:
rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx

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.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x⁻¹ + 1 = 0
⊢ x ∈ B

pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
⊢ x ∈ B

Tactic:
· rw [add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv, inv_neg, inv_one] at h_2
      simpa only [h_2] using B.neg_mem _ B.one_mem

Goal state after:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
⊢ x ∈ B
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
⊢ Subgroup.map f (stabilizer G s) ≤ stabilizer H (⇑f '' s)

Tactic:
by
  rintro a
  simp only [Subgroup.mem_map, mem_stabilizer_iff, forall_exists_index, and_imp]
  rintro a ha rfl
  rw [← image_smul_distrib, ha]

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ ↑a ∈ ⊥

Tactic:
simp only [mem_stabilizer_iff, Subgroup.mem_bot, QuotientGroup.eq_one_iff]

Goal state after:
case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' 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 : K
h : 0 ≤ x
⊢ 0 ≤ stdPart x

Tactic:
obtain hx | hx := eq_or_ne (ArchimedeanClass.mk x) 0

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : 0 ≤ x
hx : mk x = 0
⊢ 0 ≤ stdPart x

case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : 0 ≤ x
hx : mk x ≠ 0
⊢ 0 ≤ stdPart x
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

Tactic:
by_cases h : P = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
h : P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
h : ¬P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
by
      by_cases hp : p = 0; · simp [hp]
      by_cases hq : q = 0; · simp [hq]
      by_cases hpq : p + q = 0
      · simp only [hpq, hp, hq, if_true, if_false]
        exact add_nonneg (pow_pos _).le (pow_pos _).le
      simp only [hpq, hp, hq, if_false]
      exact le_trans (pow_right_mono₀ (by lia) (Polynomial.natDegree_add_le _ _)) (by grind)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ ∑ x ∈ q.support, MvPolynomial.C (MvPolynomial.coeff x q) * (x.prod fun i k ↦ ![X, 1] i ^ k).homogenize n =
    ∑ v ∈ q.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v q)

Tactic:
refine Finset.sum_congr rfl fun m hm ↦ ?_

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
⊢ MvPolynomial.C (MvPolynomial.coeff m q) * (m.prod fun i k ↦ ![X, 1] i ^ k).homogenize n =
    (MvPolynomial.monomial m) (MvPolynomial.coeff m q)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_1.last
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ (Fin.snoc r (q %ₘ g) (Fin.last n)).degree < g.degree

Tactic:
simpa using degree_modByMonic_lt q hg

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
obtain rfl | hxy := eq_or_ne x y

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x : α
xs : List α
h : (∀ (a' : α), a' ∈ x :: xs → r x a') ∧ Pairwise r (x :: xs)
⊢ (if x ≠ x then x :: (x :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: x :: xs).dedup

case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : SignType.sign c ≠ 0
⊢ c = P.eraseLead.leadingCoeff

Tactic:
have h_eL : eraseLead P ≠ 0 := by simp [← coeffList_eq_nil, h_eL]
    obtain ⟨ls, hls⟩ := coeffList_eq_cons_leadingCoeff h_eL
    grind

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
η : R
P : R[X]
hx : η ≠ 0
⊢ (C η * P).signVariations = P.signVariations

Tactic:
by
  wlog! hx2 : 0 < η
  · simpa [lt_of_le_of_ne hx2, hx] using this (η := -η) (P := -P)
  rw [signVariations, signVariations]
  rw [coeffList_C_mul _ (lt_or_lt_iff_ne.mp (.inr hx2)), ← List.comp_map]
  congr 5
  funext
  simp [hx2, sign_mul]

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
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ ((monomial d) c).signVariations + 1 ≤ ((X - C η) * (monomial d) c).signVariations

Tactic:
by
  have h₁ : nextCoeff ((X - C η) * monomial d c) = -(η * c) := by
    convert coeff_mul_monomial (X - C η) d 0 c
    · simp [hc, nextCoeff, natDegree_mul (X_sub_C_ne_zero η)]
    · simp
  have h₂ : eraseLead ((X - C η) * monomial d c) ≠ 0 := by
    apply mt nextCoeff_eq_zero_of_eraseLead_eq_zero
    simp [h₁, hc, hη.ne']
  have h₃ : SignType.sign c ≠ SignType.sign (-(η * c)) := by
    simp [hη, hc, Left.sign_neg, sign_mul]
  simpa [h₁, h₂, h₃, hc, hη.ne', signVariations, List.destutter_cons_cons,
    ← leadingCoeff_cons_eraseLead, coeffList_eraseLead, leadingCoeff_eraseLead_eq_nextCoeff]
  using! List.length_pos_of_ne_nil (List.destutter'_ne_nil _ _)

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

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ range (q - 1), (aeval r) ((⇑derivative)^[x] p) + (aeval r) ((⇑derivative)^[q - 1] p) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) =
    0 + (q - 1)! • eval r p' + q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)

pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))

Tactic:
· congr 2
    · apply sum_eq_zero
      exact fun x hx => aeval_iterate_derivative_of_lt p _ r hp (mem_range.mp hx)
    · rw [← aeval_iterate_derivative_self _ _ _ hp]
    · rw [smul_sum, sum_congr rfl]
      intro k hk
      exact hc k (mem_Ico.mp hk).1 r

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case e_a
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
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re) • 1 + ((z.re * w.im) • ↑u + (z.im * w.re) • ↑u) = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • ↑u

Tactic:
← add_smul

Goal state after:
case e_a
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
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • ↑u = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • ↑u
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ QuadraticAlgebra.C (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
ext <;> rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ ((LinearMap.toMatrix (basis a b) (basis a b)) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)).det = norm z

Tactic:
have : !![z.re, a * z.im; z.im, z.re + b * z.im].det = z.norm := by
    simp [norm]
    ring

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
⊢ ((LinearMap.toMatrix (basis a b) (basis a b)) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)).det = norm z
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ q • x = ↑q * x

Tactic:
ext <;> simp [NNRat.smul_def]

Goal state after: