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

Goal state before:
pp: n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
⊢ n.MinSqFacProp o

Tactic:
have : ∀ p, Prime p → p * p ∣ n → k * (p * p) ∣ n := fun p pp dp =>
    have :=
      (coprime_primes pk pp).2 fun e => by
        subst e
        contradiction
    (coprime_mul_iff_right.2 ⟨this, this⟩).mul_dvd_of_dvd_of_dvd dk dp
  rcases o with - | d
  · rw [MinSqFacProp, squarefree_iff_prime_squarefree] at H ⊢
    exact fun p pp dp => H p pp ((dvd_div_iff_mul_dvd dk).2 (this _ pp dp))
  · obtain ⟨H1, H2, H3⟩ := H
    simp only [dvd_div_iff_mul_dvd dk] at H2 H3
    exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, fun p pp dp => H3 _ pp (this _ pp dp)⟩

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
⊢ Squarefree n ↔ n.minSqFac = none

Tactic:
by
  have := minSqFac_has_prop n
  constructor <;> intro H
  · rcases e : n.minSqFac with - | d
    · rfl
    rw [e] at this
    cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1
  · rwa [H] at this

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

Goal state before:
pp: ⊢ Ω 1 = 0

Tactic:
simp [cardFactors_apply]

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

Goal state before:
pp: n : ℕ
⊢ Ω n = 1 ↔ Nat.Prime n

Tactic:
by
  refine ⟨fun h => ?_, fun h => List.length_eq_one_iff.2 ⟨n, primeFactorsList_prime h⟩⟩
  cases n with | zero => simp at h | succ n =>
  rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩
  rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
  apply prime_of_mem_primeFactorsList
  rw [hx, List.mem_singleton]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i, f i = m → f ∈ d.finMulAntidiag m

Tactic:
· rw [mem_finMulAntidiag]
    exact fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : ∏ i, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i

Tactic:
mem_primeFactorsList hf.2,

Goal state after:
d n p : ℕ
hn : Squarefree n
hp : Prime p ∧ p ∣ n
f : Fin d → ℕ
hf : ∏ i, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (sigma 0) n = ∑ n ∈ Ioc 0 N, N / n

Tactic:
by
  rw [← zeta_mul_pow_eq_sigma, pow_zero_eq_zeta]
  convert! sum_Ioc_mul_zeta_eq_sum zeta N using 1
  simpa using sum_congr rfl (by grind)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
b : β
x✝ : ∃ q, b < ↑q ∧ ↑q < a
q : ℚ
hbq : b < ↑q
hqa : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
by rwa [coe_lt_inducedMap_iff]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i + C r) = single i 1

Tactic:
rw [degree_add_of_lt, degree_X]

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
a✝ : Nontrivial R
⊢ m.Monic (X i + C r)

Tactic:
apply monic_X.add_of_lt

Goal state after:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
a✝ : Nontrivial R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑(#s) * ∑ i ∈ s, f i * g i

Tactic:
by
  rw [← nsmul_eq_mul]
  exact hfg.sum_smul_sum_le_card_smul_sum

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
⊢ ∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s

Tactic:
by
  simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, lt_iff_le_and_ne,
    hfg.sum_comp_perm_smul_le_sum_smul hσ]

Goal state after:
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
x : M
hx : x ∈ s
⊢ ∃ i, x ∈ f i

Tactic:
apply subset_closure (s := (s : Set M)) at hx

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
x : M
hx : x ∈ ↑(closure ↑s)
⊢ ∃ i, x ∈ f i
Module: Mathlib.Algebra.Order.Module.PositiveLinearMap

Goal state before:
pp: R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid E₁
inst✝⁷ : PartialOrder E₁
inst✝⁶ : AddCommMonoid E₂
inst✝⁵ : PartialOrder E₂
inst✝⁴ : AddCommMonoid E₃
inst✝³ : PartialOrder E₃
inst✝² : Module R E₁
inst✝¹ : Module R E₂
inst✝ : Module R E₃
f g : E₁ →ₚ[R] E₂
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid E₁
inst✝⁷ : PartialOrder E₁
inst✝⁶ : AddCommMonoid E₂
inst✝⁵ : PartialOrder E₂
inst✝⁴ : AddCommMonoid E₃
inst✝³ : PartialOrder E₃
inst✝² : Module R E₁
inst✝¹ : Module R E₂
inst✝ : Module R E₃
g : E₁ →ₚ[R] E₂
toLinearMap✝ : E₁ →ₗ[R] E₂
monotone'✝ : Monotone toLinearMap✝.toFun
h : (fun f ↦ f.toFun) { toLinearMap := toLinearMap✝, monotone' := monotone'✝ } = (fun f ↦ f.toFun) g
⊢ { toLinearMap := toLinearMap✝, monotone' := monotone'✝ } = g
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order

Tactic:
have hne' : ofLex x ≠ 0 := hne

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: 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
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
wlog hab : a ≤ b generalizing a b

Goal state after:
case 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
this :
  ∀ (a b : G),
    a ≤ b →
      ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) =
        ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
hab : ¬a ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

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
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inr.inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
hx' : mk x ≠ ⊤
⊢ mk x + mk x⁻¹ = mk y + mk y⁻¹

Tactic:
simp [← mk_mul, hx, hy]

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

Goal state before:
pp: case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S

Tactic:
rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]

Goal state after:
case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 1 ≤ S.valuation ((algebraMap (↥R) K) r)

case a.ha
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < S.valuation ((algebraMap (↥R) K) r)

case a.hb
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R

Tactic:
exact R.zero_mem

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| f a - f b

Tactic:
rw [← tsub_add_cancel_of_le h]

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| f (a - b + b) - f b
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ mk x = 0 ↔ 0 < ArchimedeanClass.mk ↑x

Tactic:
by
  apply mk_eq_mk.trans
  simp

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
q : ℚ
⊢ mk (FiniteElement.mk ↑q ⋯) = ↑q

Tactic:
cases q with | div n d hd
   =>  _ 

Goal state after:
case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk ↑(↑n / ↑d) ⋯) = ↑(↑n / ↑d)
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
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ stdPart x = f (FiniteResidueField.mk (FiniteElement.mk x h))

Tactic:
stdPart,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0) =
    f (FiniteResidueField.mk (FiniteElement.mk x h))
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 : mk x = 0
⊢ FiniteResidueField.mk (FiniteElement.mk x ⋯) ≠ 0

Tactic:
FiniteResidueField.mk_ne_zero

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : mk x = 0
⊢ mk ↑(FiniteElement.mk x ⋯) = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ stdPart x = 0

Tactic:
stdPart,

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0) = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ stdPart 0 = 0

Tactic:
stdPart,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (if h : 0 ≤ mk 0 then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 0 h) else 0) = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ stdPart 1 = 1

Tactic:
stdPart,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (if h : 0 ≤ mk 1 then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 1 h) else 0) = 1
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
⊢ stdPart (-x) = -stdPart x

Tactic:
stdPart,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
⊢ (if h : 0 ≤ mk (-x) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (-x) h) else 0) =
    -if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0
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
r : ℝ
⊢ stdPart (f r) = r

Tactic:
stdPart,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
r : ℝ
⊢ (if h : 0 ≤ mk (f r) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (f r) h) else 0) = r
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
f : ℝ →+*o K
hx : 0 ≤ mk x
⊢ (FiniteResidueField.ofArchimedean f) (stdPart x) = FiniteResidueField.mk (FiniteElement.mk x hx)

Tactic:
stdPart,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : 0 ≤ mk x
⊢ (FiniteResidueField.ofArchimedean f)
      (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0) =
    FiniteResidueField.mk (FiniteElement.mk x hx)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: 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

Tactic:
stdPart,

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 ≤ if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0
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
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : r < stdPart x
⊢ f r - f (stdPart x) < x - f (stdPart x)

Tactic:
← map_sub

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : r < stdPart x
⊢ f (r - stdPart x) < x - f (stdPart x)
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)
  · obtain ⟨a, ha⟩ := exists_int_lt_of_mk_nonneg hx
    obtain ⟨b, hb⟩ := exists_int_gt_of_mk_nonneg hx
    have hn : {r | x < f r}.Nonempty := ⟨b, by simpa using hb⟩
    have hb : BddBelow {r | x < f r} := by
      refine ⟨a, fun r hr ↦ ?_⟩
      by_contra! hra
      exact (f.monotone' hra.le).not_gt (by simpa using ha.trans hr)
    apply stdPart_eq f <;> intro r hr
    · simpa using notMem_of_lt_csInf hr hb
    · obtain ⟨s, hs, hs'⟩ := (csInf_lt_iff hb hn).1 hr
      exact hs.le.trans (f.monotone' hs'.le)
  · rw [stdPart_of_mk_ne_zero hx.ne]
    have hr {r} := hx.trans_le (mk_map_nonneg_of_archimedean f r)
    obtain h | h := le_or_gt 0 x
    · convert! Real.sInf_empty.symm
      rw [Set.eq_empty_iff_forall_notMem]
      exact fun r ↦ (lt_of_mk_lt_mk_of_nonneg hr h).not_gt
    · convert! Real.sInf_univ.symm
      rw [Set.eq_univ_iff_forall]
      exact fun r ↦ lt_of_mk_lt_mk_of_nonpos hr h.le

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

Goal state before:
pp: case pos.inl
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
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : d < c
⊢ ((truncLTLinearMap K c) (ofLex (↑↑f y))).coeff d = ((truncLTLinearMap K c) (ofLex (f.eval x))).coeff d

pp: case pos.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 : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ ((truncLTLinearMap K c) (ofLex (↑↑f y))).coeff d = ((truncLTLinearMap K c) (ofLex (f.eval x))).coeff d

Tactic:
· simp_rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc]
      refine (f.evalCoeff_eq (Set.mem_of_mem_of_subset hy ?_)).symm
      simpa using (ball_strictAnti K hdc).le

Goal state after:
case pos.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 : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ ((truncLTLinearMap K c) (ofLex (↑↑f y))).coeff d = ((truncLTLinearMap K c) (ofLex (f.eval x))).coeff d
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
⊢ P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList

Tactic:
by
  have h₂ := ne_zero_of_natDegree_gt (natDegree_pos_of_nextCoeff_ne_zero h)
  have h₃ := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h
  simpa [natDegree_eraseLead_add_one h, coeffList, withBotSucc_degree_eq_natDegree_add_one h₂,
    withBotSucc_degree_eq_natDegree_add_one h₃, List.range_succ] using
    (Polynomial.eraseLead_coeff_of_ne · ·.ne)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ swap (C f) = map C f

Tactic:
by
  simpa [← algebraMap_eq] using aeval_X_left_eq_map f

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
rcases subsingleton_or_nontrivial R with H | H

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Subsingleton R
⊢ (p * q).IsMonicOfDegree (m + n)

case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).IsMonicOfDegree (m + n)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
⊢ q.IsMonicOfDegree n

Tactic:
rcases subsingleton_or_nontrivial R with H | H

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
⊢ q.IsMonicOfDegree n

case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
⊢ q.IsMonicOfDegree n
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
⊢ (evalEval h) ((mk p) g) = Polynomial.evalEval x y g

Tactic:
by
  rw [evalEval, lift_mk, eval₂_evalRingHom]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
⊢ p.IsMonicOfDegree m

Tactic:
rcases subsingleton_or_nontrivial R with H | H

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
⊢ p.IsMonicOfDegree m

case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
⊢ p.IsMonicOfDegree m
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p + q).IsMonicOfDegree n

Tactic:
rcases subsingleton_or_nontrivial R with H | H

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Subsingleton R
⊢ (p + q).IsMonicOfDegree n

case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Nontrivial R
⊢ (p + q).IsMonicOfDegree n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

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

Tactic:
rcases subsingleton_or_nontrivial R with H | H

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Subsingleton R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree n

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