mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, p = n

Tactic:
← toFinset_factors,

Goal state after:
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactorsList.toFinset, p = n
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : ¬m.sPolynomial f g = 0
⊢ m.degree (m.sPolynomial f g) ≠ m.degree f ⊔ m.degree g

Tactic:
contrapose hs

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g
⊢ m.sPolynomial f g = 0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
by
  rw [isPrimePow_nat_iff]
  constructor
  · rintro ⟨p, k, hp, hk, rfl⟩
    refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩
    rintro q ⟨hq, hq'⟩
    exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')
  rintro ⟨p, ⟨hp, hn⟩, hq⟩
  rcases eq_or_ne n 0 with (rfl | hn₀)
  · cases (hq 2 ⟨Nat.prime_two, dvd_zero 2⟩).trans (hq 3 ⟨Nat.prime_three, dvd_zero 3⟩).symm
  refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, ?_⟩
  simp only [and_imp] at hq
  apply Nat.dvd_antisymm (Nat.ordProj_dvd _ _)
  -- We need to show n ∣ p ^ n.factorization p
  apply Nat.dvd_of_primeFactorsList_subperm hn₀
  rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
  intro q hq'
  rw [Nat.mem_primeFactorsList hn₀] at hq'
  cases hq _ hq'.1 hq'.2
  simp

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p a m n : ℕ
hp : Prime p
hn : n ≠ 0
k : ℕ
h : (p ^ k) ^ n = a ^ n
m_eq : m = n * k
⊢ ∃ k, a = p ^ k

Tactic:
use k

Goal state after:
case h
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
k : ℕ
h : (p ^ k) ^ n = a ^ n
m_eq : m = n * k
⊢ a = p ^ k
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ #n.divisors = ∏ x ∈ n.primeFactors, (n.factorization x + 1)

Tactic:
rw [← sigma_zero_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]
  exact prod_congr n.support_factorization fun _ h =>
    sigma_zero_apply_prime_pow <| prime_of_mem_primeFactors h

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactors = 1

Tactic:
← toFinset_factors,

Goal state after:
n : ℕ
⊢ n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactorsList.toFinset = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1

Tactic:
· rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
⊢ s.Infinite → ∀ (b : R), ∃ a, b ≤ ∑ k ∈ Finset.range a, s.indicator (fun x ↦ r) k

Tactic:
intro hs n

Goal state after:
case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
⊢ ∃ a, n ≤ ∑ k ∈ Finset.range a, s.indicator (fun x ↦ r) k
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

Tactic:
wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0

Goal state after:
case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
        (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
            (c₁ * c₂) *
          m.sPolynomial p₁ p₂
H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : f (x.lcm y) ≠ 0
⊢ f (x.gcd y) = f (x.lcm y) * f (x.gcd y) / f (x.lcm y)

Tactic:
mul_div_cancel_left₀ _ hf_lcm

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : f (x.lcm y) ≠ 0
⊢ f (x.gcd y) = f (x.gcd y)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
u : MulArchimedeanClass M
hu : u ∈ ↑s
⊢ mk 1 ∈ ↑s

Tactic:
simpa using s.upper (by simp) hu

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
⊢ (b + a - 1) / a = 0

Tactic:
by simp_rw [ha.antisymm <| zero_le _, Nat.div_zero]

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

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
a b : G
nab : b / a ∈ C
nba : a / b ∈ C
⊢ (b / a)⁻¹ ∈ C

Tactic:
by simpa using nba

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ b ∈ ↑(pure a) ↔ b = a

Tactic:
coe_pure,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ b ∈ {a} ↔ b = a
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case coe
α : Type u_1
inst✝ : PartialOrder α
s₀ : NonemptyInterval α
⊢ ↑(dual ↑s₀) = ⇑ofDual ⁻¹' ↑↑s₀

Tactic:
exact NonemptyInterval.coe_dual s₀

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⟦Γ⟧
⊢ x.leadingCoeff = x.coeff x.order

Tactic:
by_cases h : x = 0
  · rw [h, leadingCoeff_zero, coeff_zero]
  · simp [leadingCoeff_of_ne_zero, orderTop_of_ne_zero, order_of_ne, h]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x✝ : Γ'
⊢ (embDomain f 0).coeff x✝ = coeff 0 x✝

Tactic:
simp [embDomain_notin_image_support]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : ¬r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
· rw [hrx, orderTop_zero]
    exact not_top_lt

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : ¬r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop
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
u : ArchimedeanStrata K M
⊢ ⨆ i, u.baseDomain ⊓ u.stratum i = u.baseDomain

Tactic:
apply iSup_congr

Goal state after:
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
⊢ ∀ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.stratum i
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : 0 < y
⊢ mk (f y) < mk x

Tactic:
rwa [mk_map_of_archimedean' f hy.ne']

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

Goal state before:
pp: case pos
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
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
rw [ArchimedeanClass.mk_sum hsupport' (hmono.mono (by simp))]

Goal state after:
case pos
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
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk ↑(f ((f.support.erase (f.support.min' hsupport)).min' hsupport'))
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
⊢ f.evalCoeff x c = (ofLex (↑↑f y)).coeff c

Tactic:
have hnonempty : ∃ y : f.val.domain, y.val - x ∈ ball K c := ⟨y, hy⟩
  simpa [evalCoeff, dif_pos hnonempty] using coeff_eq_of_mem f x hnonempty.choose_spec hy le_rfl

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

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
⊢ ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (x - ↑y)

Tactic:
have : x - y.val = x - z.val + (z.val - y.val) := by abel

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
⊢ ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (x - ↑y)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
x✝ : ArchimedeanClass.mk (x - ↑y) ≠ ⊤
⊢ ⟨ArchimedeanClass.mk (x - ↑y), x✝⟩ ∈ UpperSet.Ici xy

Tactic:
by simp; rfl

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

Goal state before:
pp: α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsLowerSet (s / t)

Tactic:
by
  rw [div_eq_mul_inv]
  exact ht.inv.mul_left

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
f : ℝ →+*o K
x : K
⊢ stdPart x = sInf {r | x < f r}

Tactic:
obtain hx | hx := le_or_gt 0 (mk x)

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
⊢ stdPart x = sInf {r | x < f r}

case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
⊢ stdPart x = sInf {r | x < f r}
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
f : R[X]
⊢ f.IsMonicOfDegree 2 ↔ ∃ a b, f = X ^ 2 - C a * X + C b

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_sub_add_two a b⟩
  simp only [sub_eq_add_neg, ← neg_mul, ← map_neg]
  obtain ⟨a, b, h⟩ := isMonicOfDegree_two_iff.mp H
  exact ⟨-a, b, (neg_neg a).symm ▸ h⟩

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree n

Tactic:
rw [← mul_one n]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree (n * 1)
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
h_dvd_k_rev : h ∣ k.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
have hk := h2 k key

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
hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n

Tactic:
apply homogenize_eq_of_isHomogeneous
  · apply_rules [MvPolynomial.IsHomogeneous.mul, isHomogeneous_homogenize]
  · simp [*]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
p : R[X]
⊢ eval r p = p.smeval r

Tactic:
rw [eval_eq_sum, smeval_eq_sum]
  rfl

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

Goal state before:
pp: case monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ↑a * ↑n ^ n✝ = ↑(a * n ^ n✝)

Tactic:
Nat.cast_mul,

Goal state after:
case monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ↑a * ↑n ^ n✝ = ↑a * ↑(n ^ n✝)
Module: Mathlib.Algebra.Polynomial.Smeval

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

Tactic:
by
    induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, mul_add]
  | monomial n a =>
    rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ sumIDeriv (C a) = C a

Tactic:
by
  rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]

Goal state after:
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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ↑(q + k)! * (aeval r) p' = ↑q ! * ((aeval r) ↑((q + k).descFactorial k) * (aeval r) p')

Tactic:
map_natCast,

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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ ↑(q + k)! * (aeval r) p' = ↑q ! * (↑((q + k).descFactorial k) * (aeval r) p')
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
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ P.coeff d < 0

Tactic:
grind [nextCoeff_of_natDegree_pos]

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
m' n' : ℕ
hmn' : m' < n'
x y z : ℤˣ
hn : n = n'
hkm' : k < m'
hq : q = trinomial k m' n' ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
subst hn

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
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
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✝ : AddCommGroupWithOne R
n : ℕ
⊢ QuadraticAlgebra.C (-↑(↑n + 1)) = -↑(n + 1)

Tactic:
C_neg

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ -QuadraticAlgebra.C ↑(↑n + 1) = -↑(n + 1)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : norm x * r = 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
rw [← C_inj (R := R) (a := a) (b := b), C_mul, C_eq_algebraMap, algebraMap_norm_eq_mul_star,
      mul_assoc, map_one] at hr

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : x * (star x * (algebraMap R (QuadraticAlgebra R a b)) r) = 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q₁ q₂ : Basis A c₁ c₂ c₃
hi : q₁.i = q₂.i
hj : q₁.j = q₂.j
⊢ q₁ = q₂

Tactic:
cases q₁; cases q₂; grind

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

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toAdd.add x y) h

Goal state after:
case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
x y : R
⊢ x * y = x * y