mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
⊢ ∑ J ∈ π.boxes with π.tag J ∉ s, ε' * B J ≤ ∑ J ∈ π.boxes, ε' * B J

Tactic:
by
      gcongr
      · exact fun _ _ _ ↦ mul_nonneg ε'0.le (hB0 _)
      · apply filter_subset

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
x : DegLex (α →₀ ℕ)
h : degree (ofDegLex x) = 0
⊢ 0 ≤ toLex (ofDegLex x)

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: n : ℕ
⊢ Multiset.Rel (fun x1 x2 ↦ x1 = x2) (normalizedFactors (n + 1)) ↑(n + 1).primeFactorsList

Tactic:
← associated_eq_eq

Goal state after:
n : ℕ
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) (normalizedFactors (n + 1)) ↑(n + 1).primeFactorsList
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ Multiset.Rel (fun x1 x2 ↦ x1 = x2) (normalizedFactors s.prod) s

Tactic:
← associated_eq_eq

Goal state after:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) (normalizedFactors s.prod) s
Module: Mathlib.Data.Nat.Squarefree

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

Tactic:
refine ⟨fun h => ?_, by rintro ⟨hn, rfl⟩; simpa⟩

Goal state after:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

Tactic:
simp_rw [h]

Goal state after:
case neg.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0
⊢ m.withBotDegree 0 = m.withBotDegree g ↔ m.degree 0 = m.degree g ∧ (True ↔ g = 0)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

Tactic:
simp_rw [h]

Goal state after:
case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : g = 0
⊢ m.withBotDegree f = m.withBotDegree 0 ↔ m.degree f = m.degree 0 ∧ (f = 0 ↔ True)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ x1 = x2) x.val y.val

Tactic:
← associated_eq_eq

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑(insert a✝ s✝)).Pairwise (Coprime on g)
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)

Tactic:
coe_insert,

Goal state after:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (insert a✝ ↑s✝).Pairwise (Coprime on g)
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2 =
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2

Tactic:
simp_rw [sum_filter]
    rw [sum_comm]
    exact sum_congr rfl fun _ _ ↦ (by simp_all)

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

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ n = a 0 * a 1 * b 2

Tactic:
hfab1,

Goal state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ n = b 0 * b 1 * b 2
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

Tactic:
wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  simp [H, degree_mul, sPolynomial_monomial_mul, degree_monomial]

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 : M
ha : a ∈ Set.Ici 1
b : M
hb : b ∈ Set.Ici 1
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
h : |b|ₘ ^ 1 < a
⊢ b < a

Tactic:
mabs_eq_self.mpr hb

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Ici 1
b : M
hb : b ∈ Set.Ici 1
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
h : b ^ 1 < a
⊢ b < a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ mk z ≤ mk y

Tactic:
exact mk_le_mk_of_mabs h

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ mk y ≤ mk z

Tactic:
exact mk_le_mk_of_mabs h

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 α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s

Tactic:
refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not at h
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]

Goal state after:
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✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some s

Tactic:
exact bot_le

Goal state after:
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✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some t

Tactic:
exact bot_le

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

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

Tactic:
exact bot_le

Goal state after:
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✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : x✝ ⊆ {⊥}
⊢ ⊥ ≤ s

Tactic:
exact bot_le

Goal state after:
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 α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ¬(⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ≤ s

Tactic:
exact bot_le

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

Goal state before:
pp: case right.bot
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
ha : ⊥ ∈ lowerBounds s₁
⊢ ⊥ ≤
    if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥

Tactic:
exact bot_le

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b✝ : Γ
r : R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ ⇑f '' x.support
⊢ ¬(if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) ≠ 0

Tactic:
dif_neg hb,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b✝ : Γ
r : R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ ⇑f '' x.support
⊢ ¬0 ≠ 0
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ Covariant α α (swap fun x1 x2 ↦ x1 * x2) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro _ _ _; simp only; intro
    rwa [← left_eq_sup, ← sup_mul_distrib, sup_of_le_left]

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✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ VAddAntidiagonal (b +ᵥ a) ⋯ = ∅

Tactic:
ext ⟨a1, a2⟩

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✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ (a1, a2) ∈ VAddAntidiagonal (b +ᵥ a) ⋯ ↔ (a1, a2) ∈ ∅
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✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ VAddAntidiagonal (b +ᵥ a) ⋯ = {(b, a)}

Tactic:
ext ⟨a1, a2⟩

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✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ (a1, a2) ∈ VAddAntidiagonal (b +ᵥ a) ⋯ ↔ (a1, a2) ∈ {(b, a)}
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
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
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
c : FiniteArchimedeanClass M
hc : c ∈ ↑f.support
d : FiniteArchimedeanClass M
hd : d ∈ ↑f.support
h : c < d
⊢ ArchimedeanClass.mk ↑(f c) < ArchimedeanClass.mk ↑(f d)

Tactic:
seed.archimedeanClassMk_of_mem_stratum (f c).prop (by simpa using! hc)

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
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
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
c : FiniteArchimedeanClass M
hc : c ∈ ↑f.support
d : FiniteArchimedeanClass M
hd : d ∈ ↑f.support
h : c < d
⊢ ↑c < ArchimedeanClass.mk ↑(f d)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case cons.inr
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s✝ : Finset β
l : β → α
i : β
s : Finset β
h✝ : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun i ↦ f (l i)
h₂ : f (l i + ∑ i ∈ s, l i) ≤ f (∑ i ∈ s, l i)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun a ↦ f (l a)

Tactic:
· exact .inr <| le_trans h₂ hind

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Multiset α
m : ℕ
⊢ ∃ t, t.card = s.card - m ∧ (∀ x ∈ t, x ∈ s) ∧ f (map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod

Tactic:
set g := fun t : Multiset α ↦ t.prod

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Multiset α
m : ℕ
g : Multiset α → α := fun t ↦ t.prod
⊢ ∃ t, t.card = s.card - m ∧ (∀ x ∈ t, x ∈ s) ∧ f (map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
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
⊢ antidiagonal ⋯ ⋯ (a + b) = ∅

Tactic:
ext ⟨a1, a2⟩

Goal state after:
Γ : 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
a1 a2 : Γ
⊢ (a1, a2) ∈ antidiagonal ⋯ ⋯ (a + b) ↔ (a1, a2) ∈ ∅
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

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

Tactic:
rw [mul_comm] at hM

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : m < n + 1
hM : f ((a + b) ^ n) ≤ f (↑(n.choose m) * (a ^ m * b ^ (n - m)))
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))
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
⊢ antidiagonal ⋯ ⋯ (a + b) = {(a, b)}

Tactic:
ext ⟨a1, a2⟩

Goal state after:
Γ : 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
a1 a2 : Γ
⊢ (a1, a2) ∈ antidiagonal ⋯ ⋯ (a + b) ↔ (a1, a2) ∈ {(a, b)}
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
⊢ (∃ q, 0 < f q ∧ f q * |y| ≤ |x|) → mk x ≤ mk y

Tactic:
rintro ⟨q, hq₀, hq⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
q : R
hq₀ : 0 < f q
hq : f q * |y| ≤ |x|
⊢ mk x ≤ mk y
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy : (i : ι) → A i
this : closure (Set.range fun s ↦ star s * s) = pi Set.univ fun i ↦ closure (Set.range fun s ↦ star s * s)
h : ∀ (i : ι), ∃ p ∈ closure (Set.range fun s ↦ star s * s), xy i = xa i + p
⊢ ∃ p, (∀ (i : ι), p i ∈ closure (Set.range fun s ↦ star s * s)) ∧ xy = xa + p

Tactic:
simp only [funext_iff, add_apply]
      exact ⟨fun i => h i |>.choose, fun i => h i |>.choose_spec.1, fun i => h i |>.choose_spec.2⟩

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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
hd : d < c
x✝ : ArchimedeanClass.mk (↑y - x) ≠ ⊤
⊢ ⟨ArchimedeanClass.mk (↑y - x), x✝⟩ ∈ UpperSet.Ioi d

Tactic:
by simpa [hy]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))

Tactic:
by
  simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul,
    LowerSet.coe_iSup₂]
  rfl

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
⊢ Function.Injective ⇑(ofArchimedean f)

Tactic:
by
  rw [injective_iff_map_eq_zero]
  intro r hr
  contrapose! hr
  rw [ofArchimedean_apply, mk_ne_zero]
  exact mk_map_of_archimedean' f hr

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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -0 • x < a
hc : c = 0
⊢ 0 < ⟨a, ha⟩

Tactic:
by simpa using! hac

Goal state after: