mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg.refine_3
ι : 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)
⊢ (fun x ↦ x.2.1.piecewise x.2.2 x.1) ({j | r j i ∧ j ∈ p}, x₁, x₂.piecewise x {j | r j i}) = x

Tactic:
simp only [piecewise_apply, Set.mem_ofPred_eq]

Goal state after:
case neg.refine_3
ι : 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)
⊢ x₁.piecewise (x₂.piecewise x {j | r j i}) {j | r j i ∧ j ∈ p} = x
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg.refine_3
ι : 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 : ι
⊢ (x₁.piecewise (x₂.piecewise x {j | r j i}) {j | r j i ∧ j ∈ p}) j = x j

Tactic:
simp only [piecewise_apply, Set.mem_ofPred_eq]

Goal state after:
case neg.refine_3
ι : 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 : ι
⊢ (if r j i ∧ j ∈ p then x₁ j else if r j i then x₂ j else x j) = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
⊢ Fibration (InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd) (DFinsupp.Lex r s) fun x ↦
    x.2.1.piecewise x.2.2 x.1

Tactic:
by
  rintro ⟨p, x₁, x₂⟩ x ⟨i, hr, hs⟩
  simp_rw [piecewise_apply] at hs hr
  split_ifs at hs with hp
  · refine ⟨⟨{ j | r j i → j ∈ p }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;> simp only [piecewise_apply, Set.mem_ofPred_eq]
    · simp only [if_pos hj]
    · split_ifs with hi
      · rwa [hr i hi, if_pos hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_ofPred_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₂, if_pos (h₁ h₂)]
      · rw [Classical.not_imp] at h₁
        rw [hr j h₁.1, if_neg h₁.2]
  · refine ⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;> simp only [piecewise_apply, Set.mem_ofPred_eq]
    · exact if_pos hj
    · split_ifs with hi
      · rwa [hr i hi, if_neg hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_ofPred_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₁.1, if_pos h₁.2]
      · rw [hr j h₂, if_neg]
        simpa [h₂] using h₁

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
⊢ ∀ ⦃i : ι⦄ ⦃a : β i⦄, ¬a < 0

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
⊢ WellFounded (Function.swap (Function.swap WellOrderingRel))

Tactic:
· rintro i ⟨a⟩
        apply hbot

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
⊢ WellFounded (Function.swap (Function.swap WellOrderingRel))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ ∀ b ∈ f.support, (b.sum fun x e ↦ e) ≤ Finsupp.degree (degLex.degree f)

Tactic:
intro b hb

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
b : σ →₀ ℕ
hb : b ∈ f.support
⊢ (b.sum fun x e ↦ e) ≤ Finsupp.degree (degLex.degree f)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0
⊢ ¬((optionEquivLeft R { b // ¬b = j }) ((renameEquiv R (optionSubtypeNe j).symm) (C c))).leadingCoeff *
        ((optionEquivLeft R { b // ¬b = j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).leadingCoeff =
      0

Tactic:
renameEquiv_apply,

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0
⊢ ¬((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) (C c))).leadingCoeff *
        ((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff =
      0
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
⊢ f ∈ piFinset s ↔ f (last n) ∈ s (last n) ∧ init f ∈ piFinset (init s)

Tactic:
simp only [Fintype.mem_piFinset, forall_fin_succ', init, and_comm]

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 g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.degree f) ∨ m.toSyn c ≤ m.toSyn (m.degree g)

Tactic:
intro b hb

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
suffices m.degree g ≺[m] d by
        rw [coeff_eq_zero_of_lt this, mul_zero]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
⊢ m.toSyn (m.degree g) < m.toSyn d
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree n ∧ k = 1 → Squarefree (n ^ k)

Tactic:
by rintro ⟨hn, rfl⟩; simpa

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

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
⊢ n'.sqrt - k ≤ n.sqrt - k

Tactic:
by gcongr

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

Goal state before:
pp: case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : k.succ ∣ n'
ml : k < m
me : k.succ = m
⊢ False

Tactic:
e

Goal state after:
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : (2 * i + 3).succ ∣ n'
ml : k < m
me : k.succ = m
⊢ False
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : k ≤ 2
⊢ False

Tactic:
e

Goal state after:
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mp.some
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
d : ℕ
e : n.minSqFac = some d
⊢ some d = none

Tactic:
e

Goal state after:
case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : n.MinSqFacProp (some d)
e : n.minSqFac = some d
⊢ some d = none
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ x ∈ n.primeFactors, (f x + g x) = (f * g) n

Tactic:
rw [prod_add, mul_apply, sum_divisorsAntidiagonal (f · * g ·),
    ← divisors_filter_squarefree_of_squarefree hn, sum_divisors_filter_squarefree hn.ne_zero,
    factors_eq]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i =
    ∑ i ∈ (↑n.primeFactorsList).toFinset.powerset, f i.val.prod * g (n / i.val.prod)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length

Tactic:
← Multiset.coe_card,

Goal state after:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (↑(m * n).primeFactorsList).card = m.primeFactorsList.length + n.primeFactorsList.length
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ n = a 1 * a 2 * a 0

Tactic:
rw [← finMulAntidiag_three a ha]

Goal state after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case refine_3
ι : 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
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s

Tactic:
· convert! h.comp_right σ.symm
    · rw [comp_assoc, self_comp_symm, comp_id]
    · rw [σ.symm.eq_preimage_iff_image_eq]
      exact Set.image_perm hσinv

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 : Antivary f g
⊢ ∑ i, f i • g (σ i) = ∑ i, f i • g i ↔ Antivary f (g ∘ ⇑σ)

Tactic:
by
  simp [(hfg.antivaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

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

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉₊ ≤ ↑⌈(b - 1)⁻¹⌉₊

Tactic:
by gcongr

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

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * a

Tactic:
by gcongr

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

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
rw [← sub_pos] at hb
    calc
      ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

Goal state after:
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))
⊢ False

Tactic:
obtain ⟨m, n, mn, h2'⟩ := h2 fun n ↦ h.natEmbedding _ _

Goal state after:
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) (fun x ↦ x ∈ s.mulAntidiagonal t a)
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (?m.120 m))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (?m.120 n))
⊢ False
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } ≤ some s

Tactic:
exact WithBot.coe_le_coe.2 ⟨le_sup_left, inf_le_left⟩

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

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun x ↦ (ofLex x).1) '' Function.support fun g ↦ (x.coeff g.1).coeff g.2) ⊆ Function.support x.coeff

Tactic:
Set.image_subset_iff,

Goal state after:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ (Function.support fun g ↦ (x.coeff g.1).coeff g.2) ⊆ (fun x ↦ (ofLex x).1) ⁻¹' Function.support x.coeff
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ f (x.orderTop.untop ⋯) ≤ f z

Tactic:
rw [OrderEmbedding.le_iff_le, WithTop.untop_le_iff]

Goal state after:
case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ x.orderTop ≤ ↑z
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
⊢ a ≤ b ∨ b ≤ a

Tactic:
· have hab := Function.ne_iff.mp <| HahnSeries.ext_iff.ne.mp hab
      let u := {i : Γ | (ofLex a).coeff i ≠ 0} ∪ {i : Γ | (ofLex b).coeff i ≠ 0}
      let v := {i : Γ | (ofLex a).coeff i ≠ (ofLex b).coeff i}
      have hvu : v ⊆ u := by
        intro i h
        rw [Set.mem_union, Set.mem_ofPred_eq, Set.mem_ofPred_eq]
        contrapose! h
        rw [Set.notMem_ofPred_iff, not_not, h.1, h.2]
      have hv : v.IsWF :=
        ((ofLex a).isPWO_support'.isWF.union (ofLex b).isPWO_support'.isWF).subset hvu
      let i := hv.min hab
      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'
      have hne : (ofLex a).coeff i ≠ (ofLex b).coeff i := hv.min_mem hab
      obtain hi | hi := lt_or_gt_of_ne hne
      · exact Or.inl (le_of_lt ⟨i, hji, hi⟩)
      · exact Or.inr (le_of_lt ⟨i, fun j hj ↦ (hji j hj).symm, hi⟩)

Goal state after:
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✝ : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ∀ x_1 ∈ VAddAntidiagonal a ⋯ \ VAddAntidiagonal a ⋯, x.coeff x_1.1 • ((of R).symm y).coeff x_1.2 = 0

Tactic:
intro b hb

Goal state after:
Γ : 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✝ : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
b : Γ × Γ'
hb : b ∈ VAddAntidiagonal a ⋯ \ VAddAntidiagonal a ⋯
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0
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
⊢ ∀ x_1 ∈ VAddAntidiagonal a ⋯ \ VAddAntidiagonal a ⋯, x.coeff x_1.1 • ((of R).symm y).coeff x_1.2 = 0

Tactic:
intro b hb

Goal state after:
Γ : 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
b : Γ × Γ'
hb : b ∈ VAddAntidiagonal a ⋯ \ VAddAntidiagonal a ⋯
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0
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✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal k ⋯, x.coeff x_1.1 • (((of R).symm y).coeff x_1.2 + ((of R).symm z).coeff x_1.2) =
    ((of R).symm (x • y)).coeff k + ((of R).symm (x • z)).coeff k

Tactic:
coeff_smul_right hwf Set.subset_union_right,

Goal state after:
Γ : 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✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal k ⋯, x.coeff x_1.1 • (((of R).symm y).coeff x_1.2 + ((of R).symm z).coeff x_1.2) =
    ((of R).symm (x • y)).coeff k + ∑ ij ∈ VAddAntidiagonal k ⋯, x.coeff ij.1 • ((of R).symm z).coeff ij.2
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ x_1 ∈ antidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 =
    ∑ ij ∈ {(a, b)}, x.coeff ij.1 * ((single b) r).coeff ij.2

Tactic:
apply sum_congr _ fun _ _ => rfl
    ext ⟨a1, a2⟩
    simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_antidiagonal, mem_singleton]
    constructor
    · rintro ⟨_, rfl, h1⟩
      exact ⟨add_right_cancel h1, rfl⟩
    · rintro ⟨rfl, rfl⟩
      simp [hx]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
← order_eq_orderTop_of_ne_zero hx,

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ (x * y).orderTop = ↑x.order + y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop

Tactic:
by gcongr

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop

Tactic:
rw [one_nsmul]

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

Goal state before:
pp: case mp.right
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ x.leadingCoeff = 1

Tactic:
rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]

Goal state after:
case mp.right
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ (1 + (x - 1)).leadingCoeff = leadingCoeff 1