mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ mk (x ^ (n + 1)) = n • mk x + mk x

Tactic:
pow_succ,

Goal state after:
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
⊢ mk (x ^ n * x) = n • mk x + mk x
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
β : Type u_4
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Finset β
b : β → α
m : ℕ
⊢ ∃ u, f (∑ t ∈ powersetCard (#s - m) s, ∏ i ∈ t, -b i) ≤ f (∏ i ∈ ↑u, -b i)

Tactic:
by
  set g := fun t : Finset β ↦ t.prod fun i : β ↦ - b i
  obtain ⟨b, hb_in, hb⟩ := hf_na.finset_image_add (by grind) (apply_nonneg f)
    g (powersetCard (s.card - m) s)
  exact ⟨⟨b, hb_in (powersetCard_nonempty.mpr (Nat.sub_le s.card m))⟩, hb⟩

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
n : ℕ
x : R
⊢ mk (x ^ (n + 1))⁻¹ = -(↑n.succ • mk x)

Tactic:
pow_succ,

Goal state after:
case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ n * x)⁻¹ = -(↑n.succ • mk x)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk x ≤ mk y ↔ ∃ q, 0 < q ∧ ↑q * |y| ≤ |x|

Tactic:
simpa using mk_le_mk_iff_denselyOrdered (Rat.castHom _) Rat.cast_strictMono (x := x)

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

Tactic:
obtain h | h := total_of (· ≤ ·) x y

Goal state after:
case h.h.inl
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
h : x ≤ y
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

case h.h.inr
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
h : y ≤ x
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
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 + 1) = (single ((n + 1) • a)) (r ^ (n + 1))

Tactic:
pow_succ,

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 a) r ^ n * (single a) r = (single ((n + 1) • a)) (r ^ (n + 1))
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 + 1))

Tactic:
pow_succ,

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 a) r ^ n * (single a) r = (single ((n + 1) • a)) (r ^ n * r)
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inr.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
⊢ x ≤ z ∨ x ≈ z

Tactic:
· exact .inr (_root_.trans h₁ h₂)

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

Goal state before:
pp: case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
snd✝ : Γ'
i : Γ
left✝ : i ∈ x.support
h1 : (f i, snd✝) ∈ antidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (f i, snd✝).1 * (embDomain f y).coeff (f i, snd✝).2 ≠ 0
⊢ (f i, snd✝) ∈ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g)

Tactic:
obtain ⟨j, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).2

Goal state after:
case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g i : Γ
left✝¹ : i ∈ x.support
j : Γ
left✝ : j ∈ y.support
h1 : (f i, f j) ∈ antidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (f i, f j).1 * (embDomain f y).coeff (f i, f j).2 ≠ 0
⊢ (f i, f j) ∈ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case inr
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
hnontrivial : Nontrivial M
hnonempty : Nonempty (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
have : Nontrivial R := (seed.strictMono_coeff c).injective.nontrivial

Goal state after:
case inr
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
hnontrivial : Nontrivial M
hnonempty : Nonempty (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
this : Nontrivial R
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y
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⟦Γ⟧
⊢ (C.comp (algebraMap R A)) r * x = x * (C.comp (algebraMap R A)) r

Tactic:
ext
    simp only [coeff_smul, single_zero_mul_eq_smul, RingHom.coe_comp, C_apply,
      Function.comp_apply, algebraMap_smul, coeff_mul_single_zero]
    rw [← Algebra.commutes, Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ support (conjneg f) = -support f

Tactic:
by
  ext; simp [starRingEnd_apply]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
⊢ R.valuation ↑((A.inclusion R hR) x) < 1

Tactic:
by
      by_contra! c; replace c := monotone_mapOfLE R S h c
      rw [(mapOfLE _ _ _).map_one, mapOfLE_valuation_apply] at c
      apply not_le_of_gt ((valuation_lt_one_iff S _).1 hx) c

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a - f b ≤ f (a - b)

Tactic:
by
  rw [tsub_le_iff_right, ← f.map_add]
  exact hf le_tsub_add

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ B.nonunits ≤ A.nonunits ↔ A ≤ B

Tactic:
by
  constructor
  · intro h x hx
    by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
    rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1] at hx ⊢
    by_contra h_2; exact hx (h h_2)
  · intro h x hx
    by_contra h_1; exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ ((Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).comp ↑A.unitGroupMulEquiv) x✝ = 1 ↔
    (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))) (A.unitGroupMulEquiv x✝) = 1

Tactic:
MonoidHom.coe_comp,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ (⇑(Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))) ∘ ⇑↑A.unitGroupMulEquiv) x✝ = 1 ↔
    (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))) (A.unitGroupMulEquiv x✝) = 1
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝¹ : k + 1 < ((monomial n) x).coeffList.length
h₁✝ : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < (List.replicate n 0).length + 1
⊢ ((monomial n) x).coeffList.get ⟨k + 1, h₁✝¹⟩ = (x :: List.replicate n 0).get ⟨k + 1, h₁✝⟩

Tactic:
List.length_replicate

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝¹ : k + 1 < ((monomial n) x).coeffList.length
h₁✝ : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < n + 1
⊢ ((monomial n) x).coeffList.get ⟨k + 1, h₁✝¹⟩ = (x :: List.replicate n 0).get ⟨k + 1, h₁✝⟩
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
x✝ : p.natDegree ≤ n ∧ p.coeff n = 1
H₁ : p.natDegree ≤ n
H₂ : p.coeff n = 1
⊢ p.Monic

Tactic:
· exact monic_of_natDegree_le_of_coeff_eq_one n H₁ H₂

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ (n + 1)).IsMonicOfDegree (m * (n + 1))

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * (n + 1))
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ (n + 1)).IsMonicOfDegree (m * (n + 1))

Tactic:
rw [pow_succ, mul_add, mul_one]

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * n + m)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p)) = spanCoeffs(q) ^ (deg(r) + 1) * spanCoeffs(p)

Tactic:
pow_succ,

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p)) = spanCoeffs(q) ^ deg(r) * spanCoeffs(q) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p)) = spanCoeffs(q) ^ (deg(r) + 1) * spanCoeffs(p)

Tactic:
rw [pow_succ, mul_assoc]

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

Goal state before:
pp: case isUnit_or_isUnit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ IsUnit g ∨ IsUnit h

Tactic:
have h_dvd_k_rev : h ∣ k.mirror := by
      rw [mirror_mul_of_domain, mirror_mirror]
      exact dvd_mul_left h g.mirror

Goal state after:
case isUnit_or_isUnit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : (ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n

Tactic:
simp only [h, degree_zero]
    exact Batteries.compareOfLessAndEq_eq_lt.mp rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f
⊢ h ∣ f.mirror

Tactic:
by rwa [← hk]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f.mirror
⊢ g ∣ f.mirror

Tactic:
by rwa [← hk]

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

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
⊢ n - m + k < n

Tactic:
rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]

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 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hePn0 : P.eraseLead ≠ 0
⊢ ((X - C η) * P.eraseLead).natDegree = P.natDegree

Tactic:
natDegree_mul (X_sub_C_ne_zero η) hePn0,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hePn0 : P.eraseLead ≠ 0
⊢ (X - C η).natDegree + P.eraseLead.natDegree = P.natDegree
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
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re • 1 + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
    (z.re * w.re) • 1 + (z.re * w.im) • ↑u + (z.im * w.re) • ↑u + (z.im * w.im) • (↑u * ↑u)

Tactic:
simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : SignType.sign P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1 := by simp [h_lC]

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : SignType.sign P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : z.re * r = 0 ∧ z.im * r = 0
⊢ z = 0

Tactic:
simp [QuadraticAlgebra.ext_iff, re_zero, im_zero, h _ hz.left, h _ hz.right]

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

Goal state before:
pp: case mpr
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
⊢ z = 0 → norm z = 0

Tactic:
· intro hz
    simp [hz]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
⊢ Multiset.countP (fun x ↦ 0 < x) P.roots ≤ P.signVariations

Tactic:
by
  generalize h : P.roots.countP (0 < ·) = num_pos_roots
  induction num_pos_roots generalizing P -- Induct on number of roots.
  · exact zero_le
  rename_i ih
  have hp : P ≠ 0 := by grind [roots_zero, Multiset.countP_zero]
  -- we can take a positive root, η, because the number of roots is positive
  obtain ⟨η, η_root, η_pos⟩ : ∃ x, x ∈ P.roots ∧ 0 < x := by grind [Multiset.countP_pos]
  -- (X - η) divides P(X), so write P(X) = (X - η) * Q(X)
  obtain ⟨Q, rfl⟩ := dvd_iff_isRoot.mpr (isRoot_of_mem_roots η_root)
  -- P has at least num_roots sign variations
  grw [ih Q, succ_signVariations_le_X_sub_C_mul η_pos]
  · exact right_ne_zero_of_mul hp
  · simp [← h, roots_mul (ne_zero_of_mem_roots η_root), η_pos, ← Nat.succ.injEq]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (q.i * q.i) = c₁ • 1 + c₂ • F q.i

Tactic:
q.i_mul_i,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₁ • 1 + c₂ • q.i) = c₁ • 1 + c₂ • F q.i
Module: Mathlib.Algebra.Ring.Pointwise.Set

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
x✝¹ x✝ : Set α
⊢ x✝¹ * -x✝ = -(x✝¹ * x✝)

Tactic:
by simp_rw [← image_neg_eq_neg]; exact image_image2_right_comm mul_neg

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : ↑(1 + n) = 0
⊢ n + 1 = 0

Tactic:
push_cast at hn

Goal state after:
case succ
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : 1 + ↑n = 0
⊢ n + 1 = 0
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ T (S (a * b)) = S (T (a * b))

Tactic:
rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]

Goal state after:
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)

Tactic:
simpa [e2] using (map_mul_left T · ·)

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
⊢ ∀ (c : SkewMonoidAlgebra k G) {x : V}, x ∈ ↑W → c • x ∈ ↑W

Tactic:
intro f v hv

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ f • v ∈ ↑W
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ 1 * { toQuot := Quot.mk (Rel r) a✝ } = { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp only [mul_quot, ← one_quot, one_mul]

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: ⊢ (√2)⁻¹ * (√2)⁻¹ = 2⁻¹

Tactic:
rw [← mul_inv]

Goal state after:
⊢ (√2 * √2)⁻¹ = 2⁻¹