mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
⊢ ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d + 1 →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
intro n

Goal state after:
case inr.succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
⊢ Finsupp.degree n = d + 1 →
    ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
⊢ ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
p

Goal state after:
case inr.succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H : IsUnit P
⊢ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

Tactic:
intro n

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H : IsUnit P
n : σ →₀ ℕ
⊢ n ≠ 0 → IsNilpotent (coeff n P)
Module: Mathlib.Algebra.Order.Ring.Finset

Goal state before:
pp: case insert
R : Type u_1
ι : Type u_2
inst✝³ : LinearOrder R
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : OrderBot R
f : ι → R
a : R
a✝¹ : ι
s✝ : Finset ι
a✝ : a✝¹ ∉ s✝
IH : s✝.sup f * a = s✝.sup fun x ↦ f x * a
⊢ (insert a✝¹ s✝).sup f * a = (insert a✝¹ s✝).sup fun x ↦ f x * a

Tactic:
simp only [sup_insert, max_mul, ← IH]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on x)) (n : ℕ),
    s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
hc : (↑(insert a s)).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), (insert a s).sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
intro n

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on x)) (n : ℕ),
    s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
hc : (↑(insert a s)).Pairwise (Commute on x)
n : ℕ
⊢ (insert a s).sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ (↑(fill x m s)).countPerms = n.choose ↑m * (↑s).countPerms

Tactic:
rw [Multiset.countPerms_filter_ne x]
  rw [← mem_coe] at hx
  refine congrArg₂ _ ?_ ?_
  · rw [card_coe, count_coe_fill_self_of_notMem hx]
  · refine congrArg _ ?_
    rw [coe_fill, coe_replicate, Multiset.filter_add]
    rw [Multiset.filter_eq_self.mpr]
    · rw [add_eq_left]
      rw [Multiset.filter_eq_nil]
      exact fun j hj ↦ by simp [Multiset.mem_replicate.mp hj]
    · exact fun j hj h ↦ hx <| by simpa [h] using hj

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ toDegLex (single a 1) < toDegLex (single b 1) ↔ b < a

Tactic:
DegLex.single_lt_iff

Goal state after:
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ b < a ↔ b < a
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d) c) = 1 ↔ c = 1

Tactic:
m.leadingCoeff_monomial

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ c = 1 ↔ c = 1
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#(S 0) * #({r ∈ piFinset (tail S) | (eval r) pₖ = 0})) / ∏ i, ↑(#(S i)) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))

Tactic:
prod_univ_succ,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#(S 0) * #({r ∈ piFinset (tail S) | (eval r) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ))) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:

Tactic:
#{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0} / ∏ i, (#(S i) : ℚ≥0)
            ≤ ↑(p.degreeOf 0 * ∏ i, #(S (.succ i))) / ∏ i, (#(S i) : ℚ≥0) := ?_
          _ = p.degreeOf 0 * (∏ i, #(S (.succ i))) / (#(S 0) * ∏ i, #(S (.succ i))) := by
            norm_cast; rw [prod_univ_succ]
          _ ≤ (p.degreeOf 0 / #(S 0) : ℚ≥0) := mul_div_mul_right_le (by positivity)

Goal state after:
case h₂
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    ↑(degreeOf 0 p * ∏ i, #(S i.succ)) / ∏ i, ↑(#(S i))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

Tactic:
classical
  by_cases h : f = 0 <;> simp [withBotDegree_eq, h]

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
      a ∈ Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val

Tactic:
intro a
    simp only [Multiset.mem_filter, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def,
      mem_divisors]
    constructor
    · rintro ⟨⟨an, h0⟩, hsq⟩
      use (UniqueFactorizationMonoid.normalizedFactors a).toFinset
      simp only [Finset.mem_powerset]
      rcases an with ⟨b, rfl⟩
      rw [mul_ne_zero_iff] at h0
      rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq
      rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
        normalizedFactors_mul h0.1 h0.2]
      exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), prod_normalizedFactors h0.1⟩
    · rintro ⟨s, hs, rfl⟩
      rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs
      have hs0 : s.val.prod ≠ 0 := by
        rw [Ne, Multiset.prod_eq_zero_iff]
        intro con
        apply
          not_irreducible_zero
            (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
      rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]
      refine ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩
      have h :=
        UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
          (fun x hx =>
            irreducible_of_normalized_factor x
              (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
          (prod_normalizedFactors hs0)
      rw [associated_eq_eq, Multiset.rel_eq] at h
      rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
      apply s.nodup

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

Goal state before:
pp: case e'_4
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 = b ^ 2 * x ^ 2

Tactic:
mul_pow

Goal state after:
case e'_4
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * x ^ 2 = b ^ 2 * x ^ 2
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Tactic:
obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)

Goal state after:
case succ
n a b : ℕ
h₁ : b ^ 2 * a = n.succ
h₂ : Squarefree a
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
this : a.factorization p = 0 ∨ b.factorization p = 0
⊢ k ≤ a.factorization p + b.factorization p → k ≤ a.factorization p ∨ k ≤ b.factorization p

Tactic:
rcases this with h | h <;> simp [h, imp_or]

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

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

Tactic:
m_eq,

Goal state after:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
k : ℕ
h : p ^ (n * k) = a ^ n
m_eq : m = n * k
⊢ ∃ k, a = p ^ k
Module: Mathlib.Algebra.Order.Antidiag.Tendsto

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
⊢ Tendsto (fun a ↦ (antidiagonal a).sup' ⋯ f) cofinite F

Tactic:
by
  intro U hU
  refine ((((hf hU).image Prod.fst)).add ((hf hU).image Prod.snd)).subset ?_
  simp only [Set.subset_def, Set.mem_compl_iff, Set.mem_preimage]
  intro x hx
  obtain ⟨i, hi, e⟩ := Finset.exists_mem_eq_sup' (nonempty_antidiagonal x) f
  obtain rfl : i.1 + i.2 = x := by simpa using hi
  exact Set.add_mem_add (by simpa using ⟨i.2, e ▸ hx⟩) (by simpa using ⟨i.1, e ▸ hx⟩)

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

Goal state before:
pp: σ✝ : 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
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial
            (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)

Tactic:
rcases H with ⟨hc1, hc2, hp1, hp2⟩

Goal state after:
σ✝ : 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
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial
            (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (- -(x * x))

Tactic:
neg_neg

Goal state after:
case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (x * x)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = - -((inducedAddHom α β) x * (inducedAddHom α β) x)

Tactic:
neg_neg

Goal state after:
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:
exact hfg.sum_smul_sum_le_card_smul_sum

Goal state after:
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
⊢ mk b ≤ mk (b * a) ↔ mk b ≤ mk a

Tactic:
mk_left_le_mk_mul_iff

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
⊢ mk b ≤ mk a ↔ mk b ≤ mk a
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
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |a * b|ₘ ≤ |a * b|ₘ ^ 2

Tactic:
pow_two,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |a * b|ₘ ≤ |a * b|ₘ * |a * b|ₘ
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
ha : 1 < a
hab : mk a < mk (b / a)
this : a⁻¹ < b / a
⊢ 1 < b

Tactic:
by
    simpa using this

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✝ : CeilDiv α β
f✝ : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ ((fun x ↦ mapRange (fun x ↦ x ⌈/⌉ _a) ⋯ x) f) i ≤ _g i ↔ f i ≤ ((fun x ↦ _a • x) _g) i

Tactic:
simpa only [coe_smul, Pi.smul_apply, mapRange_apply] using gc_smul_ceilDiv ha (f i) _

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
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
⊢ ∀ (m : ℕ), s.sup g ≤ m → f (s.sup g) = f m

Tactic:
intro n

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : ¬x✝ ⊆ {⊥}
b : Interval α
hs : b ∈ x✝
hb : b ∉ {⊥}
⊢ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ } ≤ s

Tactic:
lift s to NonemptyInterval α using ne_bot_of_le_ne_bot hb (ha hs)

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
h : ¬x✝ ⊆ {⊥}
b : Interval α
hs : b ∈ x✝
hb : b ∉ {⊥}
s : NonemptyInterval α
ha : ↑s ∈ upperBounds x✝
⊢ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ } ≤ ↑s
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff g ≠ 0

Tactic:
← hg

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff (⋯.min ⋯) ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx✝ : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (x.orderTop.untop hx✝) = x.leadingCoeff

Tactic:
leadingCoeff_of_ne_zero hx,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx✝ : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (x.orderTop.untop hx✝) = x.coeff (x.orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (Function.support fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)).IsPWO

Tactic:
convert! x.unop.isPWO_support; ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ x.orderTop < i ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0

Tactic:
rw [← not_le, le_orderTop_iff_forall]
  simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ≤ (ofSuppBddBelow f ⋯).order

Tactic:
le_order_iff_forall

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ∀ j < n, (ofSuppBddBelow f ⋯).coeff j = 0

Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ofSuppBddBelow f ⋯ ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).coeff ((x + y).orderTop.untop ⋯) = x.leadingCoeff

Tactic:
leadingCoeff_of_ne_zero hx,

Goal state after:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).coeff ((x + y).orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
h : x = 0
⊢ False

Tactic:
simp_all [orderTop_zero, WithTop.top_ne_coe]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
h : y = 0
⊢ False

Tactic:
simp_all [orderTop_zero, WithTop.top_ne_coe]

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
u : ArchimedeanStrata K M
⊢ Submodule.map u.baseDomain.subtype (iSup u.stratum') = Submodule.map u.baseDomain.subtype ⊤

Tactic:
suffices ⨆ i, u.baseDomain ⊓ u.stratum i = u.baseDomain by simpa using! this

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, u.baseDomain ⊓ u.stratum i = u.baseDomain