mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: 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 - 1) * a = b * a

Tactic:
sub_one_mul,

Goal state after:
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 - a) = b * a
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
n : ℕ
⊢ s.sup g ≤ n → f (s.sup g) = f n

Tactic:
hn

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
n : ℕ
hn : s.sup g ≤ n
⊢ f (s.sup g) = f n
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

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

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico_of_not_isMin ha b

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✝² : R
x✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ ((x✝³ + x✝²) • x✝¹).coeff x✝ = (x✝³ • x✝¹ + x✝² • x✝¹).coeff x✝

Tactic:
simp [add_smul]

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c ≤ b + c

Tactic:
· apply le_of_lt
      rw [lt_iff] at hlt ⊢
      obtain ⟨i, hj, hi⟩ := hlt
      refine ⟨i, fun j hji ↦ ?_, add_left_strictMono hi⟩
      simp [hj j hji]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a * d * c = a * c * d

Tactic:
by simp_rw [mul_assoc, mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr.inr
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
have : ¬0 < a + b := by simpa using add_nonpos ha hb
      simp [ha, hb, card_Ico_zero_add, Ico_eq_empty, this]

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 ⋯
this : (ofLex |x|).coeff j = 0
⊢ 0 = (ofLex ((n + 1) • |x|)).coeff j

Tactic:
by simp [this]

Goal state after:
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
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
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ (ofLex 0).coeff j = (seed.coeff j) (f j)

Tactic:
DFinsupp.notMem_support_iff.mp ?_

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
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
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ (ofLex 0).coeff j = (seed.coeff j) 0

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
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ j ∉ f.support
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s✝ : Finset β
l : β → α
i : β
s : Finset β
h✝ : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun i ↦ f (l i)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun a ↦ f (l a)

Tactic:
rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂

Goal state after:
case cons.inl
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s✝ : Finset β
l : β → α
i : β
s : Finset β
h✝ : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun i ↦ f (l i)
h₁ : f (l i + ∑ i ∈ s, l i) ≤ f (l i)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun a ↦ f (l a)

case cons.inr
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s✝ : Finset β
l : β → α
i : β
s : Finset β
h✝ : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun i ↦ f (l i)
h₂ : f (l i + ∑ i ∈ s, l i) ≤ f (∑ i ∈ s, l i)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun a ↦ f (l a)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
⊢ f (∑ i ∈ s, l i) = f (l k)

Tactic:
by_cases hcard : s.card = 1
  · grind [Finset.card_eq_one.mp hcard]
  · classical
    rw [← Finset.add_sum_erase _ _ hk]
    have hNonempty : (s.erase k).Nonempty :=
      Finset.Nontrivial.erase_nonempty (Finset.one_lt_card_iff_nontrivial.mp (by grind))
    have hrest_le := IsNonarchimedean.apply_sum_le_sup fna hNonempty (l := l)
    simp only [Finset.le_sup'_iff, Finset.mem_erase, ne_eq] at hrest_le
    rw [add_eq_max_of_ne' f fna f_neg (by grind), max_eq_left (le_of_lt (by grind))]

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

Goal state before:
pp: case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

Tactic:
refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩

Goal state after:
case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ (↑n + 1) * (f q * |y|) ≤ (↑n + 1) * |x|
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Tactic:
· rw [h, coeff_mul_single_add]
    simp

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P

Tactic:
refine ⟨fun _ a b _ => ?_, fun h => ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
⊢ a ∈ P ∨ b ∈ P

case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ P.IsOrdering
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 y : ↥(↑f).domain
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
by
  obtain hsubsingleton | hnontrivial := subsingleton_or_nontrivial M
  · have : y = x := Subtype.ext <| hsubsingleton.allEq _ _
    simp [this]
  have hnonempty : Nonempty (FiniteArchimedeanClass M) := inferInstance
  obtain c := hnonempty.some
  have : Nontrivial R := (seed.strictMono_coeff c).injective.nontrivial
  rw [← archimedeanClassMk_eq_iff]
  simp_rw [← HahnSeries.archimedeanClassOrderIsoWithTop_apply]
  rw [(HahnSeries.archimedeanClassOrderIsoWithTop (FiniteArchimedeanClass M) R).injective.eq_iff]

Goal state after:
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
x y : FiniteElement K
hy : ⟦y⟧ ∈ {⟦x⟧}
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ⟦z⟧ ∈ {⟦x⟧}

Tactic:
Set.mem_singleton_iff,

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
x y : FiniteElement K
hy : ⟦y⟧ = ⟦x⟧
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ⟦z⟧ = ⟦x⟧
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : (p - X ^ n).natDegree ≤ n - 1
hq : (q - X ^ n).natDegree ≤ n - 1
⊢ (p - X ^ n - (q - X ^ n)).natDegree ≤ n - 1

Tactic:
exact (natDegree_sub_le_iff_left hq).mpr hp

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 : ℕ
⊢ n ∈ Finset.range (p.natDegree + 1) →
    p.mirror.coeff n ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

Tactic:
hn

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
⊢ p.mirror.coeff n ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n ∈ Finset.range (p.natDegree + 1) →
    p.coeff n ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = n

Tactic:
hn

Goal state after:
case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
⊢ p.coeff n ≠ 0 →
    ∃ a,
      ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
        (revAt (p.natDegree + p.natTrailingDegree)) a = n
Module: Mathlib.Algebra.Polynomial.Module.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : R[X] ⊗[R] M →ₗ[R[X]] PolynomialModule R M := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M := ↑R (eval X) ∘ₗ map R[X] ((TensorProduct.mk R R[X] M) 1)
⊢ inv ∘ₗ ↑R e = LinearMap.id

Tactic:
ext n x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : R[X] ⊗[R] M →ₗ[R[X]] PolynomialModule R M := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M := ↑R (eval X) ∘ₗ map R[X] ((TensorProduct.mk R R[X] M) 1)
n : ℕ
x : M
⊢ ((AlgebraTensorModule.curry (inv ∘ₗ ↑R e) ∘ₗ monomial n) 1) x =
    ((AlgebraTensorModule.curry LinearMap.id ∘ₗ monomial n) 1) x
Module: Mathlib.Algebra.Polynomial.Module.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : R[X] ⊗[R] M →ₗ[R[X]] PolynomialModule R M := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M := ↑R (eval X) ∘ₗ map R[X] ((TensorProduct.mk R R[X] M) 1)
left : inv ∘ₗ ↑R e = LinearMap.id
⊢ ↑R e ∘ₗ inv = LinearMap.id

Tactic:
ext n x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : R[X] ⊗[R] M →ₗ[R[X]] PolynomialModule R M := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M := ↑R (eval X) ∘ₗ map R[X] ((TensorProduct.mk R R[X] M) 1)
left : inv ∘ₗ ↑R e = LinearMap.id
n : ℕ
x : M
a✝ : ℕ
⊢ (((↑R e ∘ₗ inv) ∘ₗ lsingle R n) x).coeff a✝ = ((LinearMap.id ∘ₗ lsingle R n) x).coeff a✝
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)

Tactic:
by_cases h : n = 0
  · subst h
    simp [ofFn]
  · rw [as_sum_range' (ofFn n v) n <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr h) v]
    simp [Finset.sum_range]

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

Goal state before:
pp: case succ.refine_2
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
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i =
    q /ₘ g * g ^ (n + 1) +
      (∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc + Fin.snoc r (q %ₘ g) (Fin.last n) * g ^ ↑(Fin.last n))

Tactic:
← add_rotate',

Goal state after:
case succ.refine_2
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
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i =
    Fin.snoc r (q %ₘ g) (Fin.last n) * g ^ ↑(Fin.last n) +
      (q /ₘ g * g ^ (n + 1) + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)
      simp [destutter', if_pos hac, if_pos (not_not.1 hbc), if_neg hab]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] (derivative p) =
    derivative (∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p)

Tactic:
derivative_sum

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] (derivative p) =
    ∑ b ∈ range (p.natDegree + 1), derivative ((⇑derivative)^[b] p)
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]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
      (∑ x ∈ range q.succ, (q.choose x * q.descFactorial (q - x)) • (X - C r) ^ (q - (q - x)) * (⇑derivative)^[x] p') =
    q ! • eval r p'

Tactic:
rw [sum_range_succ', Nat.choose_zero_right, one_mul, tsub_zero, Nat.descFactorial_self, tsub_self,
    pow_zero, smul_mul_assoc, one_mul, Function.iterate_zero_apply, eval_add, eval_smul]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
        (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
            (⇑derivative)^[k + 1] p') +
      q ! • eval r p' =
    q ! • eval r p'
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2.e_a
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 ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = ∑ x ∈ Ico q (p.natDegree + 1), q ! • (aeval r) (c x)

Tactic:
sum_congr rfl

Goal state after:
case inr.refine_2.e_a
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)
⊢ (Ico q (p.natDegree + 1)).sum ?m.743 = ∑ x ∈ Ico q (p.natDegree + 1), q ! • (aeval r) (c x)

case inr.refine_2.e_a
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 ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = ?m.743 x

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] := ⋯
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)
⊢ ℕ → A
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ AddMonoid (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addMonoid _ rfl ?_ ?_

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r✝ : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).re = (r • x + s • x).re

Tactic:
simp [add_smul]

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r✝ : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).im = (r • x + s • x).im

Tactic:
simp [add_smul]

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

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0) →
    ∀ (x : R), x * r = 0 → x = 0

Tactic:
intro H x hxr

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ x = 0