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

Goal state before:
pp: case h₀
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
⊢ ∀ b ∈ a.support.piAntidiag n,
    b ≠ ⇑s →
      (if s = indicator a.support fun i x ↦ b i then ↑(Nat.multinomial a.support b) * ∏ x ∈ a.support, a x ^ b x
        else 0) =
        0

Tactic:
simp only [Finset.mem_piAntidiag, ne_eq, Finsupp.mem_support_iff, ite_eq_right_iff, and_imp]
    intro _ _ _ _ hed
    simp [Finsupp.ext_iff] at hed
    grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (f a + ∑ x ∈ s, f x)! / ((f a)! * ∏ x ∈ s, (f x)!) = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Tactic:
h₁,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (1 + ∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
n : σ →₀ ℕ
⊢ n ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support → n i = 0

Tactic:
contrapose

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
n : σ →₀ ℕ
⊢ ¬n i = 0 → n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
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
inst✝¹ : Finite σ
this : Fintype σ
α β : Type u_1
inst✝ : Fintype β
e : α ≃ β
h₁ : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial β R
⊢ IsNilpotent ((rename ⇑e.symm) P) ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
h₁,

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P✝ : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α β : Type u_1
inst✝ : Fintype β
e : α ≃ β
h₁ : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial β R
⊢ (∀ (i : α →₀ ℕ), IsNilpotent (coeff i ((rename ⇑e.symm) P))) ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m u✝ : σ →₀ ℕ
a✝ : R
⊢ coeff (p • m) ((expand p) ((monomial u✝) a✝)) = coeff m ((monomial u✝) a✝)

Tactic:
simp [*, nsmul_right_inj hp]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (p • m) ((expand p) p✝) = coeff m p✝
a✝ : coeff (p • m) ((expand p) q✝) = coeff m q✝
⊢ coeff (p • m) ((expand p) (p✝ + q✝)) = coeff m (p✝ + q✝)

Tactic:
simp [*, nsmul_right_inj hp]

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

Goal state before:
pp: m m' : Multiset ℕ
⊢ (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial

Tactic:
by
  induction m using Multiset.induction_on with
  | empty => simp
  | cons x m hind =>
    simp only [cons_add, sum_cons, sum_add, multinomial_cons, hind, ← mul_assoc]
    congr 2
    rw [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left, eq_comm,
      Nat.choose_mul (Nat.le_add_right _ _), ← Nat.choose_symm (Nat.le_add_right x _)]
    simp [add_tsub_cancel_left]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : r j i ∧ j ∈ p
⊢ x₁ j = x j

pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ x₂ j = x j

Tactic:
· rw [hr j h₁.1, if_pos h₁.2]

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ x₂ j = x j
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)
hbc : degree (ofDegLex b) < degree (ofDegLex c)
⊢ degree (ofDegLex a) < degree (ofDegLex c) ∨
    degree (ofDegLex a) = degree (ofDegLex c) ∧ toLex (ofDegLex a) < toLex (ofDegLex c)

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)
hbc : degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) < toLex (ofDegLex c)
⊢ degree (ofDegLex a) < degree (ofDegLex c) ∨
    degree (ofDegLex a) = degree (ofDegLex c) ∧ toLex (ofDegLex a) < toLex (ofDegLex c)

Tactic:
· left; exact lt_of_eq_of_lt hab.1 hbc

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

Goal state before:
pp: case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ f ∣ C a → ∃ b, b ∣ a ∧ f = C b

pp: case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ (∃ b, b ∣ a ∧ f = C b) → f ∣ C a

Tactic:
· intro hf
    use coeff 0 f
    suffices f.totalDegree = 0 by
      rw [totalDegree_eq_zero_iff_eq_C] at this
      refine ⟨?_, this⟩
      rw [this, C_dvd_iff_dvd_coeff] at hf
      simpa using hf 0
    apply Nat.eq_zero_of_le_zero
    simpa using totalDegree_le_of_dvd_of_isDomain hf (by simp [ha])

Goal state after:
case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ (∃ b, b ∣ a ∧ f = C b) → f ∣ C a
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (init r)}) = #(S (last n)) * #({r ∈ piFinset (init S) | P r})

Tactic:
by
  rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]

Goal state after:
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) = c

Tactic:
simp only [leadingCoeff, degree_monomial]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ coeff (if c = 0 then 0 else d) ((monomial d) c) = c
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : { P // (P.sum fun x ↦ id) = n }
⊢ (↑f).extendDomain.support ⊆ s

Tactic:
by simp [map_eq_image, image_subset_iff]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Tactic:
rw [leadingCoeff, degree_pow_of_pow_leadingCoeff_ne_zero hf, coeff_pow_nsmul_degree]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
⊢ f ∈ (MvPolynomial σ R)⁰

Tactic:
← nonZeroDivisorsLeft_eq_nonZeroDivisors,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
⊢ f ∈ nonZeroDivisorsLeft (MvPolynomial σ R)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ (f * g) x✝ = (g * f) x✝

Tactic:
rw [mul_apply, ← map_swap_divisorsAntidiagonal, sum_map]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ∑ x ∈ x✝.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 * g ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    (g * f) x✝
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n

Tactic:
simp [squarefree_mul_iff, Nat.coprime_iff_isRelPrime.mp hmn]

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

Goal state before:
pp: p i : ℕ
hp : Nat.Prime p
⊢ (σ 1) (p ^ i) = ∑ k ∈ range (i + 1), p ^ k

Tactic:
by
  simp [sigma_apply_prime_pow hp]

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

Goal state before:
pp: p i : ℕ
hp : Nat.Prime p
⊢ (σ 0) (p ^ i) = i + 1

Tactic:
by
  simp [sigma_apply_prime_pow hp]

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

Goal state before:
pp: d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1) = t i

Tactic:
rw [prod_attach (f := fun p => if p ∣ t i then p else 1), ← Finset.prod_filter]

Goal state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ n.primeFactors with a ∣ t i, a = t i
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
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁)) (c₂ * m.leadingCoeff p₂ * c₁) * p₁ -
      (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂)) (c₁ * m.leadingCoeff p₁ * c₂) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂

Tactic:
mul_right_comm,

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
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁)) (c₂ * c₁ * m.leadingCoeff p₂) * p₁ -
      (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂)) (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂
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
hab : mk a ≤ mk b
⊢ mk a ≤ mk (a * b)

Tactic:
by
  simpa [hab] using min_le_mk_mul (a := a) (b := b)

Goal state after:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 - x

Tactic:
rwa [tsub_pos_iff_lt]

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m n : ℕ
hn : Squarefree n
hmn : m ∣ n
h_zero : f m = 0
⊢ f n = 0

Tactic:
by
  rcases hmn with ⟨k, rfl⟩
  simp only [zero_mul, hf.map_mul_of_coprime (coprime_of_squarefree_mul hn), h_zero]

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 α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i, f i • g (σ i) < ∑ i, f i • g i ↔ ¬Monovary f (g ∘ ⇑σ)

Tactic:
by
  simp [(hfg.monovaryOn _).sum_smul_comp_perm_lt_sum_smul_iff fun _ _ ↦ mem_univ _]

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

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌈r⌉ₑ = 0 ↔ r = 0

Tactic:
simpa using ceil_le (n := 0)

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

Goal state before:
pp: case refine_1.refine_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ s.toProd = (s.toProd.1, s.toProd.1)

Tactic:
this.1

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ s.toProd = (s.toProd.1, s.toProd.2)
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
inst✝ : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }) =
    Function.support fun g g' ↦ x.coeff (g, g')
⊢ (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }).IsPWO

Tactic:
h₁,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }) =
    Function.support fun g g' ↦ x.coeff (g, g')
⊢ (Function.support fun g g' ↦ x.coeff (g, g')).IsPWO
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
refine (not_nonempty_iff_eq_empty.1 ?_).symm

Goal state after:
case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ¬(⋂ s ∈ S, ↑s).Nonempty
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
x✝ : Γ
⊢ x✝ ∈ Function.support f → n ≤ x✝

Tactic:
contrapose

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
x✝ : Γ
⊢ ¬n ≤ x✝ → x✝ ∉ Function.support f
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
· simp [hx]

Goal state after:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.order y.order ≤ (x + y).order

pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
· simp [hx]

Goal state after:
case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.order y.order ≤ (x + y).order
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
a : Γ
⊢ (embDomain f (x + y)).coeff (f a) = (embDomain f x + embDomain f y).coeff (f a)
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
a : Γ
⊢ (embDomain f (r • x)).coeff (f a) = (r • embDomain f x).coeff (f a)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inl
Γ : 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
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex a).coeff i < (ofLex b).coeff i
⊢ a ≤ b ∨ b ≤ a

pp: case inr.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
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex b).coeff i < (ofLex a).coeff i
⊢ a ≤ b ∨ b ≤ a

Tactic:
· exact Or.inl (le_of_lt ⟨i, hji, hi⟩)

Goal state after:
case inr.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
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex b).coeff i < (ofLex a).coeff i
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
heq : 0 = (ofLex x).leadingCoeff
⊢ 0 ≤ x

pp: case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x

Tactic:
· exact le_of_eq (leadingCoeff_eq_zero.mp heq.symm).symm

Goal state after:
case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
⊢ ((of R).symm (x • y)).coeff a = ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2

Tactic:
rw [coeff_smul]
  apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_left _ hxs _ _) _ fun _ _ => rfl
  intro b hb
  simp only [not_and', mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb
  rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]

Goal state after: