mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: case mpr
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ hs.min hns ∈ s ∧ ht.min hnt ∈ t ∧ hs.min hns • ht.min hnt = hs.min hns • ht.min hnt

Tactic:
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
g : G
hg : g ∈ f.coeff.support
hgn : g ∉ Prod.fst '' s
⊢ f.coeff g • x (g⁻¹ • p) = 0

Tactic:
obtain (h | h) : f.coeff g = 0 ∨ ∀ q, ¬ x q = 0 → ¬g • q = p := by aesop

Goal state after:
case inl
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
g : G
hg : g ∈ f.coeff.support
hgn : g ∉ Prod.fst '' s
h : f.coeff g = 0
⊢ f.coeff g • x (g⁻¹ • p) = 0

case inr
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
g : G
hg : g ∈ f.coeff.support
hgn : g ∉ Prod.fst '' s
h : ∀ (q : P), ¬x q = 0 → ¬g • q = p
⊢ f.coeff g • x (g⁻¹ • p) = 0
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length ≤ l₁.length + k
⊢ l₂.getD k 0 = 0 + (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) (l₁.length + k)

Tactic:
zero_add

Goal state after:
case inr
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length ≤ l₁.length + k
⊢ l₂.getD k 0 = (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) (l₁.length + k)
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case nil
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ [inst : DecidablePred fun x ↦ [].getD x 0 ≠ 0], [].toFinsupp = (mapIdx (fun n r ↦ Finsupp.single n r) []).sum

Tactic:
exact toFinsupp_nil

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case inr
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}ᶜ
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)

Tactic:
by_cases ht₁ : ‖t‖ = 0

Goal state after:
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
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)

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
⊢ 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
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Tactic:
by
  rw [multinomial, Nat.div_eq_iff_eq_mul_left _ (prod_factorial_dvd_factorial_sum _ _), prod_cons,
    multinomial, mul_assoc, mul_left_comm _ (f a)!,
    Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
    Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]
  positivity

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

Goal state before:
pp: α : Type u_1
a : α
f : α → ℕ
⊢ multinomial {a} f = 1

Tactic:
rw [← cons_empty, multinomial_cons]; simp

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

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

Tactic:
refine { add_left_cancel := fun f g h H ↦ ?_ }

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
f g h : MvPolynomial σ R
H : (fun x ↦ f + x) g = (fun x ↦ f + x) h
⊢ g = h
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
refine Acc.intro _ fun s => ?_

Goal state after:
case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
s : Sym2 α
⊢ Sym2.GameAdd rα s s(a, b) → Acc (Sym2.GameAdd rα) s
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✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
classical
    convert! ←
      @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩
        (InvImage.accessible snd <| hs.prod_gameAdd hu)
    convert! piecewise_single_erase x i

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 < degree (ofDegLex x) ∨ 0 = degree (ofDegLex x) ∧ 0 ≤ toLex (ofDegLex x)

Tactic:
simp only [h, lt_self_iff_false, true_and, false_or]
      exact bot_le

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case refine_2
ι : 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
⊢ dist (∑ x ∈ π.boxes with π.tag x ∉ s, (vol x) (f (π.tag x))) (∑ x ∈ π.boxes with π.tag x ∉ s, g x) ≤ ε / 2

Tactic:
calc
    dist (∑ J ∈ π.boxes with tag π J ∉ s, vol J (f (tag π J)))
      (∑ J ∈ π.boxes with tag π J ∉ s, g J)
      ≤ ∑ J ∈ π.boxes with tag π J ∉ s, ε' * B J := dist_sum_sum_le_of_le _ fun J hJ ↦ by
      rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
      refine Hδ₂ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ ε'0 _ (π.le_of_mem' _ hJ) ?_ (fun hH => hπδ.2 hH J hJ)
        fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)
      convert! hπδ.1 J hJ using 3; exact (if_neg hJs).symm
    _ ≤ ∑ J ∈ π.boxes, ε' * B J := by
      gcongr
      · exact fun _ _ _ ↦ mul_nonneg ε'0.le (hB0 _)
      · apply filter_subset
    _ = B I * ε' := by rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]
    _ ≤ ε / 2 := hεI.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 : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = coeff d (C (coeff 0 f))

Tactic:
· rw [coeff_C, if_neg (Ne.symm hd)]
    apply coeff_eq_zero_of_lt (m := m)
    rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]
    exact ⟨bot_le, hd⟩

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ 2 * #(image (uncurry Sym2.mk) s.offDiag) = #s.offDiag

Tactic:
rw [card_eq_sum_card_image (Sym2.mk.uncurry : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: s : Finset ℕ
m n✝ p n k : ℕ
h : ¬n < k * k
⊢ n.sqrt - k < n.sqrt + 2 - k

Tactic:
by
        exact Nat.minFac_lemma n k h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ ↑ζ i.1 • f i.2 = f i.2

Tactic:
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ ↑ζ i.1 • f i.2 = f i.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
⊢ (f * g) • h = f • g • h

Tactic:
by
  ext n
  simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum, sum_sigma']
  apply sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;> aesop (add simp mul_assoc)

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

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k

Tactic:
hp.pow_minFac hk.ne',

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ (p ^ k).factorization p = p ^ k
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction M
⊢ 0 • r = 0

Tactic:
by
    ext
    simp only [smul_apply, sum_const_zero, zero_smul, zero_apply]

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

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

Tactic:
Multiset.coe_card,

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q₁ ∈ cutMap β a

Tactic:
coe_mem_cutMap_iff

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q₁ < a
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) ∈ cutMap β b

Tactic:
coe_mem_cutMap_iff

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) < b
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
s : Finset ι
hf : ∀ i ∈ s, (f i).IsMultiplicative
⊢ (∏ i ∈ s, f i).IsMultiplicative

Tactic:
by
  induction s using Finset.cons_induction
  case empty => simp
  case cons a s ha ih =>
    rw [Finset.prod_cons]
    exact (hf a (by grind)).mul (by grind)

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

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
a b : M
hle : mk a ≤ mk b
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ (mk b)

Tactic:
| mk b
     => 

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
a b : M
hle : mk a ≤ mk b
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ (mk b)
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulLeftStrictMono α
a b c : α
hc : c < a * b
⊢ ∃ b', b' < b ∧ c < a * b'

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul'.2 hc)

Goal state after:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulLeftStrictMono α
a b c : α
hc : c < a * b
a' : α
hc' : c / a < a'
ha' : a' < b
⊢ ∃ b', b' < b ∧ c < a * b'
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: case inr
M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
y : M
hy : 1 < y
z : M
hz : 1 < z
hx : 1 < y * z
hyx : y < y * z
hxy : y * z ≤ y ^ 2
⊢ ∃ y_1, 1 < y_1 ∧ y_1 ^ 2 ≤ y * z

Tactic:
exact ⟨z, hz, by simpa [pow_succ] using hxy⟩

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

Goal state before:
pp: case mp
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt → a = hs.min hns ∧ b = ht.min hnt

pp: case mpr
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt

Tactic:
· rintro ⟨has, hat, hst⟩
    obtain rfl :=
      (hs.min_le hns has).eq_of_not_lt fun hlt =>
        (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
    exact ⟨rfl, mul_left_cancel hst⟩

Goal state after:
case mpr
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: case mpr
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ hs.min hns ∈ s ∧ ht.min hnt ∈ t ∧ hs.min hns * ht.min hnt = hs.min hns * ht.min hnt

Tactic:
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
⊢ ((single a) r).map f = (single a) (f r)

Tactic:
ext g
  by_cases h : g = a <;> simp [h]

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

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

Tactic:
WithTop.coe_eq_coe

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

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

Tactic:
WithTop.coe_eq_coe

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
⊢ (x - y).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Addition

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

Tactic:
WithTop.coe_eq_coe

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
hy : y ≠ 0
hyg : ⋯.min ⋯ = g
⊢ (x - y).coeff g = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
⊢ 0 < ↑(f (f.support.min' hsupport))

Tactic:
apply ArchimedeanClass.pos_of_pos_of_mk_lt hfpos

Goal state after:
case refine_2
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
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk (↑(f (f.support.min' hsupport)) - f.sum fun x x_1 ↦ ↑x_1)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
y : S
hy : y ≠ 0
⊢ mk x ≤ 0 + mk x

Tactic:
zero_add

Goal state after:
case inr
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
y : S
hy : y ≠ 0
⊢ mk x ≤ mk x
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).order = ↑(x.order + y.order)

Tactic:
WithTop.coe_eq_coe

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).order = x.order + y.order
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
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
← Set.IsWF.min_add

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
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : 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.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
← Set.IsWF.min_add

Goal state after:
Γ : 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.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
⊢ (single 0) (x * y) = (single (0 + 0)) (x * y)

Tactic:
zero_add

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
⊢ (single 0) (x * y) = (single 0) (x * y)