mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DegLex (α →₀ ℕ)
h : a ≤ b
c : DegLex (α →₀ ℕ)
⊢ a + c ≤ b + c

Tactic:
rw [le_iff] at h ⊢

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DegLex (α →₀ ℕ)
h :
  degree (ofDegLex a) < degree (ofDegLex b) ∨
    degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) ≤ toLex (ofDegLex b)
c : DegLex (α →₀ ℕ)
⊢ degree (ofDegLex (a + c)) < degree (ofDegLex (b + c)) ∨
    degree (ofDegLex (a + c)) = degree (ofDegLex (b + c)) ∧ toLex (ofDegLex (a + c)) ≤ toLex (ofDegLex (b + c))
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
rw [le_iff] at h ⊢

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h :
  degree (ofDegLex (a + b)) < degree (ofDegLex (a + c)) ∨
    degree (ofDegLex (a + b)) = degree (ofDegLex (a + c)) ∧ toLex (ofDegLex (a + b)) ≤ toLex (ofDegLex (a + c))
⊢ degree (ofDegLex b) < degree (ofDegLex c) ∨
    degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) ≤ toLex (ofDegLex c)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
⊢ degreeOf j (C c * p) = degreeOf j p

Tactic:
by_cases hp : p = 0
  · simp [hp]
  classical
  simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul']
  · simp
  · have hp' : (optionEquivLeft R _ ((rename (optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0 := by
      intro h
      exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))
    simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C,
      Polynomial.leadingCoeff_C]
    contrapose hp'
    ext m
    apply hc.1
    simpa using congr_arg (coeff m) hp'

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

Goal state before:
pp: case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (∑ i ∈ insert a s, m.degree (P i)) (∏ i ∈ insert a s, P i) = ∏ i ∈ insert a s, m.leadingCoeff (P i)

Tactic:
simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f → IsUnit (f 1)

Tactic:
rintro ⟨f, rfl⟩
    refine ⟨⟨f.val 1, f⁻¹.val 1, ?_, ?_⟩, rfl⟩
    · rw [← ArithmeticFunction.mul_apply_one, Units.mul_inv, one_one]
    · rw [← ArithmeticFunction.mul_apply_one, Units.inv_mul, one_one]

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

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ (m.gcd n).Coprime p

Tactic:
coprime_comm,

Goal state after:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ p.Coprime (m.gcd n)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k k' n : ℕ
hk : k ≤ k'
⊢ (σ k) n ≤ (σ k') n

Tactic:
simp_rw [sigma_apply]
  gcongr with d hd
  exact pos_of_mem_divisors hd

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

Goal state before:
pp: ⊢ Ω 1 = 0

Tactic:
by simp [cardFactors_apply]

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

Goal state before:
pp: d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ f ∈ {f ∈ Fintype.piFinset fun x ↦ n.divisors | ∏ i, f i = m}

Tactic:
simp only [ne_eq,
    Fintype.mem_piFinset, mem_divisors, mem_filter]

Goal state after:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i, f i = m
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → 1 (m * n) = 1 m * 1 n

Tactic:
by
    intro m n hm hn hmn
    by_cases h : m = 1 <;> aesop

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

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

Tactic:
exact zero_floorDiv _

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

Goal state before:
pp: M : Type u_2
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
x : M
inst✝¹ : CommGroup M
inst✝ : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
⊢ ∃ y, y < 1 ∧ x < y ^ n

Tactic:
use y⁻¹, inv_lt_one_of_one_lt hy

Goal state after:
case right
M : Type u_2
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
x : M
inst✝¹ : CommGroup M
inst✝ : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
⊢ x < y⁻¹ ^ n
Module: Mathlib.Algebra.Order.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
⊢ |a • b| = |a| • |b|

Tactic:
obtain ha | ha := le_total a 0 <;> obtain hb | hb := le_total b 0

Goal state after:
case inl.inl
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
hb : b ≤ 0
⊢ |a • b| = |a| • |b|

case inl.inr
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
hb : 0 ≤ b
⊢ |a • b| = |a| • |b|

case inr.inl
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
hb : b ≤ 0
⊢ |a • b| = |a| • |b|

case inr.inr
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
hb : 0 ≤ b
⊢ |a • b| = |a| • |b|
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
a✝ : NonemptyInterval α
⊢ dual (map f ↑a✝) = map (OrderHom.dual f) (dual ↑a✝)

Tactic:
· exact WithBot.map_comm rfl _

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b

Tactic:
by
  simpa [succ_eq_add_one] using Iio_succ_eq_Iic_of_not_isMax hb

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : PartialOrder Γ
inst✝² : Zero R
a b : Γ
r : R
inst✝¹ : Nonempty Γ
inst✝ : Nontrivial R
⊢ ∃ x y, x ≠ y

Tactic:
obtain ⟨r, s, rs⟩ := exists_pair_ne R

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : PartialOrder Γ
inst✝² : Zero R
a b : Γ
r✝ : R
inst✝¹ : Nonempty Γ
inst✝ : Nontrivial R
r s : R
rs : r ≠ s
⊢ ∃ x y, x ≠ y
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
⊢ a ≤ b ∨ b ≤ a

Tactic:
have hji (j) : j < i → (ofLex a).coeff j = (ofLex b).coeff j :=
        not_imp_not.mp <| fun h' ↦ hv.not_lt_min hab h'

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : LocallyFiniteOrder Gˣ
⊢ StrictMono ⇑(orderMonoidWithZeroHom G)

Tactic:
have := orderMonoidHom_strictMono (G := Gˣ)
  intro a b h
  aesop (add simp orderMonoidWithZeroHom)

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

Goal state before:
pp: case refine_1
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : gh ∈ antidiagonal ⋯ ⋯ x✝
⊢ gh ∈ antidiagonal ⋯ ⋯ x✝

Tactic:
simp_all only [mem_antidiagonal, mem_support, map_coeff, ne_eq, and_true]

Goal state after:
case refine_1
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : ¬f (x.coeff gh.1) = 0 ∧ ¬f (y.coeff gh.2) = 0 ∧ gh.1 + gh.2 = x✝
⊢ ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0
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 : y < 0
⊢ mk (f y) < mk x

Tactic:
mk_map_of_archimedean' f hy.ne

Goal state after:
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 : y < 0
⊢ 0 < mk x
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : (Finset.range (n + 1)).Nonempty → m ∈ Finset.range (n + 1)
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
simp only [Finset.nonempty_range_iff, ne_eq, Nat.succ_ne_zero, not_false_iff, Finset.mem_range,
    forall_true_left] at hm_lt

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
hm_lt : m < n + 1
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))
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
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
⊢ y⁻¹ ∈ {x | 0 < (↑x - 1).orderTop}

Tactic:
by
    suffices 0 < (y.inv - 1).orderTop by exact this
    obtain (_ | _) := subsingleton_or_nontrivial R
    · simp
    · have : 0 < (y.val - 1).orderTop := h
      rw [orderTop_self_sub_one_pos_iff] at this
      have nz : y.val.leadingCoeff * y.inv.leadingCoeff ≠ 0 := by
        rw [this.2, one_mul]
        exact leadingCoeff_ne_zero.mpr (by simp)
      refine y.inv.orderTop_self_sub_one_pos_iff.mpr ⟨?_, ?_⟩
      · simpa [this.1, y.val_inv] using (orderTop_mul_of_ne_zero nz).symm
      · simpa [this.2, y.val_inv] using (leadingCoeff_mul_of_ne_zero nz).symm

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
x a : R
a✝¹ : a ∈ P
a✝ : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
z : R := (1 - x) * half
⊢ x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
rw [show x = y ^ 2 - z ^ 2 by
    linear_combination (-x - x * half * 2) * h2]

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
x a : R
a✝¹ : a ∈ P
a✝ : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
z : R := (1 - x) * half
⊢ (y ^ 2 - z ^ 2) * a ∈ P ∧ -((y ^ 2 - z ^ 2) * a) ∈ P
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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
⊢ False

Tactic:
have hnonempty : ∃ y : f.val.domain, y.val - x ∈ ball K (seq 0) := by
    specialize hmem 0
    contrapose hmem with hempty
    simp [evalCoeff, dif_neg hempty]

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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
hnonempty : ∃ y, ↑y - x ∈ ball K (seq 0)
⊢ False
Module: Mathlib.Algebra.Order.Star.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : NonUnitalSemiring α
inst✝⁶ : NonUnitalSemiring β
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : StarRing α
inst✝² : StarRing β
inst✝¹ : StarOrderedRing α
inst✝ : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ closure (Set.range fun s ↦ ((star s).1 * s.1, (star s).2 * s.2)) =
    closure (Set.range fun p ↦ (star p.1 * p.1, star p.2 * p.2))

Tactic:
Prod.star_def

Goal state after:
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 : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
hd : c ≤ d
⊢ f.evalCoeff x d = 0

Tactic:
apply evalCoeff_eq_zero

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 : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
hd : c ≤ d
⊢ ¬∃ y, ↑y - x ∈ ball K d
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
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑(f.extendFun hx) ⟨a + b, ⋯⟩

Tactic:
simp_rw [← hc, extendFun]

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
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑((↑f).supSpanSingleton x (f.eval x) hx) ⟨a + c • x, ⋯⟩
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
⊢ ∀ (a : M),
    ArchimedeanClass.mk a = (withTopOrderIso M) (ofLex ((f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) a)).orderTop

Tactic:
· simp_rw [LinearPMap.mk_apply] at harch
    simp [harch]

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

Goal state before:
pp: case hab
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(q) ≤ Mq

Tactic:
exact sup_le (by simpa) (by simpa [Submodule.span_le, Set.range_subset_iff])

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

Goal state before:
pp: case h₂
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(p) ≤ Mp

Tactic:
exact sup_le (by simpa) (by simpa [Submodule.span_le, Set.range_subset_iff])

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

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ (p.divModByMonicAux H).2.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).2
    gcongr <;> exact sup_le (by simpa) (by simpa [Submodule.span_le, Set.range_subset_iff])

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ MvPolynomial.eval₂ f g (p.homogenize n) = eval₂ f (g 0) p

Tactic:
by
  apply Polynomial.induction_with_natDegree_le
    (fun p ↦ MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0)) (N := n)
  · simp
  · simp +contextual [hg]
  · simp +contextual
  · assumption

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
n : ℕ
⊢ (↑n).smeval x = n • x ^ 0

Tactic:
by
  induction n with
  | zero => simp only [smeval_zero, Nat.cast_zero, zero_smul]
  | succ n ih => rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]

Goal state after:
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
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            ((monomial (k + k)) (↑u * ↑w) + (monomial (k + (n - m + k))) (↑u * ↑v) + (monomial (k + n)) (↑u * ↑u) +
                    ((monomial (m + k)) (↑v * ↑w) + (monomial (m + (n - m + k))) (↑v * ↑v) +
                      (monomial (m + n)) (↑v * ↑u)) +
                  ((monomial (n + k)) (↑w * ↑w) + (monomial (n + (n - m + k))) (↑w * ↑v) +
                    (monomial (n + n)) (↑w * ↑u))).toFinsupp.coeff) }

Tactic:
toFinsupp_add,

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (((monomial (k + k)) (↑u * ↑w)).toFinsupp + ((monomial (k + (n - m + k))) (↑u * ↑v)).toFinsupp +
                    ((monomial (k + n)) (↑u * ↑u)).toFinsupp +
                  (((monomial (m + k)) (↑v * ↑w)).toFinsupp + ((monomial (m + (n - m + k))) (↑v * ↑v)).toFinsupp +
                    ((monomial (m + n)) (↑v * ↑u)).toFinsupp) +
                (((monomial (n + k)) (↑w * ↑w)).toFinsupp + ((monomial (n + (n - m + k))) (↑w * ↑v)).toFinsupp +
                  ((monomial (n + n)) (↑w * ↑u)).toFinsupp)).coeff) }