mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ‖↑t - x‖ = 0
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)

pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖↑t - x‖ = 0
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)

Tactic:
· simpa [show t = x by simpa [sub_eq_zero] using ht₂, two_mul] using t.2

Goal state after:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖↑t - x‖ = 0
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) =
    multinomial {a, b} (Function.update f a (f a).succ) + multinomial {a, b} (Function.update f b (f b).succ)

Tactic:
simp only [binomial_eq_choose, Function.update_apply,
    h, Ne, ite_true, ite_false, not_false_eq_true]

Goal state after:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ ((f a).succ + (f b).succ).choose (f a).succ =
    ((f a).succ + if b = a then (f a).succ else f b).choose (f a).succ + (f a + (f b).succ).choose (f a)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
⊢ IsCancelAdd (MvPolynomial σ R)

Tactic:
suffices IsLeftCancelAdd (MvPolynomial σ R) from
    AddCommMagma.IsLeftCancelAdd.toIsCancelAdd _

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
⊢ IsLeftCancelAdd (MvPolynomial σ R)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : IsReduced R
⊢ P.totalDegree = 0 ↔ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

Tactic:
rw [totalDegree_eq_zero_iff]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : IsReduced R
⊢ (∀ m ∈ P.support, ∀ (x : σ), m x = 0) ↔ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
rw [sum_empty]
    rintro (_ | n)
    · rw [_root_.pow_zero, Fintype.sum_subsingleton]
      swap
      · exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
      convert! (@one_mul R _ _).symm
      convert! @Nat.cast_one R _
      simp
    · rw [_root_.pow_succ, mul_zero]
      have : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
      apply (Fintype.sum_empty _).symm

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((expand p).comp (bind₁ f)) φ = (bind₁ fun i ↦ (expand p) (f i)) φ

Tactic:
expand_comp_bind₁

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (bind₁ fun i ↦ (expand p) (f i)) φ = (bind₁ fun i ↦ (expand p) (f i)) φ
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
x : σ → R
hx : x ∈ Set.univ.pi s
⊢ (eval x) q - (eval x) q = 0

Tactic:
sub_self

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

Goal state before:
pp: case pos
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : m i = 0
j : σ
hj : j = i
⊢ m j ≤ 0

Tactic:
← hm,

Goal state after:
case pos
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : m i = 0
j : σ
hj : j = i
⊢ m j ≤ m 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
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ f.totalDegree = 0

Tactic:
rw [totalDegree_eq_zero_iff]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ ∀ m ∈ f.support, ∀ (x : σ), m x = 0
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
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + g) = m.degree f

Tactic:
apply m.toSyn.injective
  apply le_antisymm
  · apply le_trans degree_add_le
    simp only [sup_le_iff, le_refl, true_and, le_of_lt h]
  · apply le_degree
    rw [mem_support_iff, coeff_add, m.coeff_eq_zero_of_lt h, add_zero,
      ← leadingCoeff, leadingCoeff_ne_zero_iff]
    intro hf
    rw [← not_le, hf] at h
    apply h
    simp only [degree_zero, map_zero]
    apply bot_le

Goal state after:
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
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

Tactic:
suffices m.degree g ≺[m] e by
      rw [m.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
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ m.toSyn (m.degree g) < m.toSyn e
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 : ↥(s.finsuppAntidiag n)
hsum : s.sum ⇑↑f = n
hs : (↑f).support ⊆ s
⊢ ↑((fun f ↦ ⟨(↑f).extendDomain, ⋯⟩) ((fun f ↦ ⟨subtypeDomain (fun x ↦ x ∈ s) ↑f, ⋯⟩) f)) = ↑f

Tactic:
exact extendDomain_subtypeDomain _ hs

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.leadingCoeff (P i) ∈ R⁰
x✝ : Subsingleton R ∨ Nontrivial R
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
cases subsingleton_or_nontrivial R with

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
x✝ : Subsingleton R ∨ Nontrivial R
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
cases subsingleton_or_nontrivial R with

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
x✝ : Subsingleton R ∨ Nontrivial R
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
cases subsingleton_or_nontrivial R with

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ m.Monic (∏ i ∈ s, P i)

Tactic:
by
  rw [Monic, leadingCoeff_prod_of_regular]
  · exact Finset.prod_eq_one H
  · intro i hi
    rw [(H i hi).leadingCoeff_eq_one]
    exact isRegular_one

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

Goal state before:
pp: case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p < 1 ↔ ¬p ∣ m
⊢ n.factorization p = m.factorization p

Tactic:
lt_one_iff,

Goal state after:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ ¬p ∣ m
⊢ n.factorization p = m.factorization p
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
⊢ n.MinSqFacProp (n.minSqFacAux k)

Tactic:
minSqFacAux

Goal state after:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_2
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 * a + 1 ∧ (b * x) ^ 2 ∣ b ^ 2 * a ∧ ∃ x_1, (b * x) ^ 2 = x_1 ^ 2

Tactic:
refine ⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩ <;> use y

Goal state after:
case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
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 * a = (b * x) ^ 2 * y

case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
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 * a = (b * x) ^ 2 * y
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
hn0 : n ≠ 0
⊢ 0 < (σ k) n

Tactic:
sigma_pos_iff,

Goal state after:
k n : ℕ
hn0 : n ≠ 0
⊢ 0 < n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.snd
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ g ∣ b.2

Tactic:
apply Nat.gcd_dvd_right

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hb : b ∈ cutMap β (a * a)
⊢ b ≤ inducedMap α β a * inducedMap α β a

Tactic:
obtain ⟨q, hb, rfl⟩ := hb
  obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')
  trans (q' : β) ^ 2
  · exact mod_cast hqq'.le
  · rw [pow_two] at hqa ⊢
    exact mul_self_le_mul_self (mod_cast hq'.le)
      (le_csSup (cutMap_bddAbove β a) <|
        coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self₀ ha.le hqa)

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
⊢ f ((a1, a2), b1, b2).1.1 * g ((a1, a2), b1, b2).1.2 * (f ((a1, a2), b1, b2).2.1 * g ((a1, a2), b1, b2).2.2) =
    f (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1) * g (((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2)

Tactic:
rw [hf.map_mul_of_coprime cop.coprime_mul_right.coprime_mul_right_right,
      hg.map_mul_of_coprime cop.coprime_mul_left.coprime_mul_left_right]

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
⊢ f ((a1, a2), b1, b2).1.1 * g ((a1, a2), b1, b2).1.2 * (f ((a1, a2), b1, b2).2.1 * g ((a1, a2), b1, b2).2.2) =
    f ((a1, a2), b1, b2).1.1 * f ((a1, a2), b1, b2).2.1 * (g ((a1, a2), b1, b2).1.2 * g ((a1, a2), b1, b2).2.2)
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
⊢ i ≤ i + 1

Tactic:
rw [← Order.succ_eq_add_one]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
⊢ i ≤ succ i
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_1.inr
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
hamax :
  (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).1 = (g a, f a).1 ∧
    (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).2 ≤ (g a, f a).2
⊢ f ((Equiv.symm σ) a) ≤ f a

Tactic:
· exact hamax.2

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

Goal state before:
pp: case e'_6
ι : 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
⊢ f = f ∘ ⇑σ ∘ ⇑(Equiv.symm σ)

Tactic:
self_comp_symm,

Goal state after:
case e'_6
ι : 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
⊢ f = f ∘ id
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) * a = b * a

Tactic:
by rw [sub_one_mul, add_sub_cancel]

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
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
by
  simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc_of_not_isMax hb a

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

Goal state before:
pp: case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : f a ∈ ⇑f '' x.support
b : Γ
hb1 : b ∈ x.support
hb2 : f b = f a
⊢ a ∈ x.support

Tactic:
rwa [f.injective hb2] at hb1

Goal state after:
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⟦Γ⟧ᵃᵒᵖ
⊢ (fun x ↦ AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ })
      ((fun x ↦ { coeff := fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }) x) =
    x

Tactic:
apply AddOpposite.unop_injective
    simp

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hlt : x < 0
hlt' : (ofLex x).leadingCoeff < 0
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|

Tactic:
rw [abs_eq_neg_self.mpr hlt.le, abs_eq_neg_self.mpr hlt'.le, ofLex_neg, leadingCoeff_neg]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
⊢ (↑(addMonoidHom G)).toFun a ≤ (↑(addMonoidHom G)).toFun b

Tactic:
by
    obtain ⟨b, rfl⟩ := add_left_surjective a b
    replace hab : 0 ≤ b := by simpa using hab
    suffices 0 ≤ addMonoidHom G b by simpa
    simp [addMonoidHom, hab]

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

Goal state before:
pp: case inr.mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
⊢ (∃ n, |y| ≤ n • |x|) → ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|

pp: case inr.mpr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
⊢ (∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) → ∃ n, |y| ≤ n • |x|

Tactic:
· -- `mk x ≤ mk y → mk x.leadingCoeff ≤ mk y.leadingCoeff`
    intro ⟨n, hn⟩
    refine ⟨n + 1, ?_⟩
    have hn' : |y| < (n + 1) • |x| :=
      lt_of_le_of_lt hn <| nsmul_lt_nsmul_left (by simpa using hx) (by simp)
    obtain ⟨j, hj, hi⟩ := (lt_iff _ _).mp hn'
    simp_rw [ofLex_smul, coeff_smul] at hj hi
    simp_rw [← leadingCoeff_abs]
    rw [leadingCoeff_of_ne_zero (by simpa using hy), leadingCoeff_of_ne_zero (by simpa using hx)]
    simp_rw [← h']
    obtain hjlt | hjeq | hjgt := lt_trichotomy (WithTop.some j) (ofLex |x|).orderTop
    · -- impossible case: `x` and `y` differ before their leading coefficients
      have hjlt' : j < (ofLex |y|).orderTop := h'.symm ▸ hjlt
      simp [coeff_eq_zero_of_lt_orderTop hjlt, coeff_eq_zero_of_lt_orderTop hjlt'] at hi
    · convert! hi.le <;> exact (WithTop.untop_eq_iff _).mpr hjeq.symm
    · exact (hj _ ((WithTop.untop_lt_iff _).mpr hjgt)).le

Goal state after:
case inr.mpr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
⊢ (∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) → ∃ n, |y| ≤ n • |x|
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos
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
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
⊢ f.support.min' hnonempty ≠ FiniteArchimedeanClass.mk a h0

Tactic:
by_contra!

Goal state after:
case pos
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
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
this : f.support.min' hnonempty = FiniteArchimedeanClass.mk a h0
⊢ False
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ (ofLex 0).coeff j = (ofLex (↑seed.baseEmbedding x)).coeff j

Tactic:
rw [seed.coeff_baseEmbedding hf.symm]

Goal state after:
case refine_1
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ (ofLex 0).coeff j = (seed.coeff j) (f j)