mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case pos
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree a < degree b
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b

pp: case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b

Tactic:
· exact Or.inl ha

Goal state after:
case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b
Module: Mathlib.Data.Sym.Card

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

pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ℕ

pp: α : 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)}) = ?m.32

Tactic:
mul_comm

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

α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ℕ

α : 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)}) = ?m.32
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: ⊢ WellFounded DvdNotUnit

Tactic:
refine RelHomClass.wellFounded
      (⟨fun x : ℕ => if x = 0 then (⊤ : ℕ∞) else x, ?_⟩ : DvdNotUnit →r (· < ·)) wellFounded_lt
    intro a b h
    rcases a with - | a
    · exfalso
      revert h
      simp [DvdNotUnit]
    cases b
    · simp
    obtain ⟨h1, h2⟩ := dvd_and_not_dvd_iff.2 h
    simp only [succ_ne_zero, cast_lt, if_false]
    refine lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h1) fun con => h2 ?_
    rw [con]

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
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
this : m.toSyn (m.degree g) < m.toSyn d
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
by
        rw [coeff_eq_zero_of_lt this, mul_zero]

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

Goal state before:
pp: case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ m.leadingCoeff f ^ n * coeff (m.degree f) f = m.leadingCoeff f ^ n * m.leadingCoeff f

Tactic:
leadingCoeff

Goal state after:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ coeff (m.degree f) f ^ n * coeff (m.degree f) f = coeff (m.degree f) f ^ n * coeff (m.degree f) f
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 f) < m.toSyn (m.degree g)
⊢ m.degree g ∉ f.support

Tactic:
by
  simp [coeff_eq_zero_of_lt h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f.ppow 0 = ↑ζ

Tactic:
ppow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ (if h0 : 0 = 0 then ↑ζ else { toFun := fun x ↦ f x ^ 0, map_zero' := ⋯ }) = ↑ζ
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ (f.ppow k) x = f x ^ k

Tactic:
ppow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ (if h0 : k = 0 then ↑ζ else { toFun := fun x ↦ f x ^ k, map_zero' := ⋯ }) x = f x ^ k
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a

Tactic:
refine symm <| Nat.div_eq_of_eq_mul_left (Finset.prod_pos
    fun p hp => (prime_of_mem_primeFactorsList (List.mem_toFinset.mp (ht hp))).pos) ?_
  rw [Finset.prod_sdiff ht, prod_primeFactors_of_squarefree hn]

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ¬(p ∈ a.factorization.support ∧ p ∈ b.factorization.support)

Tactic:
←
      Finset.mem_inter

Goal state after:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ∉ a.factorization.support ∩ b.factorization.support
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k ↦ (σ 1) (p ^ k)) = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k

Tactic:
exact prod_congr n.support_factorization fun _ h =>
    sigma_one_apply_prime_pow <| prime_of_mem_primeFactors h

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁹ : Field α✝
inst✝⁸ : LinearOrder α✝
inst✝⁷ : Field β✝
inst✝⁶ : LinearOrder β✝
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h : f x < g x
q : ℚ
hf : f x < f ↑q
hg : ↑q < g x
⊢ False

Tactic:
rw [← map_ratCast g] at hg

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝⁹ : Field α✝
inst✝⁸ : LinearOrder α✝
inst✝⁷ : Field β✝
inst✝⁶ : LinearOrder β✝
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h : f x < g x
q : ℚ
hf : f x < f ↑q
hg : g ↑q < g x
⊢ False
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap β γ (inducedMap α β a) ↔ ↑q < inducedMap α γ a

Tactic:
coe_lt_inducedMap_iff,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap α β a ↔ ↑q < inducedMap α γ a
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap α β a ↔ ↑q < inducedMap α γ a

Tactic:
coe_lt_inducedMap_iff,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < a ↔ ↑q < inducedMap α γ a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case h
M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b c : MulArchimedeanOrder M
m : ℕ
hm : |val b|ₘ ≤ |val a|ₘ ^ m
n : ℕ
hn : |val c|ₘ ≤ |val b|ₘ ^ n
⊢ |val c|ₘ ≤ (|val a|ₘ ^ m) ^ n

Tactic:
exact hn.trans (pow_le_pow_left' hm n)

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|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)

Tactic:
rw [max_eq_left h, min_eq_left, mk_mabs]
    exact mk_le_mk_of_mabs h

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ ∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
      f (x_1 ^ (x.lcm y).factorization x_1) * f (x_1 ^ (x.gcd y).factorization x_1) =
    (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors, f (x_1 ^ x.factorization x_1)) *
      ∏ x ∈ x.primeFactors ∪ y.primeFactors, f (x ^ y.factorization x)

Tactic:
← prod_mul_distrib

Goal state after:
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ ∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
      f (x_1 ^ (x.lcm y).factorization x_1) * f (x_1 ^ (x.gcd y).factorization x_1) =
    ∏ x_1 ∈ x.primeFactors ∪ y.primeFactors, f (x_1 ^ x.factorization x_1) * f (x_1 ^ y.factorization x_1)
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
s : NonemptyInterval α
x : α × α
a : α
inst✝ : Nonempty α
⊢ Nonempty α

Tactic:
infer_instance

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

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

Tactic:
· intro s ha
      split_ifs with h
      · exact bot_le
      obtain ⟨b, hs, hb⟩ := not_subset.1 h
      lift s to NonemptyInterval α using ne_bot_of_le_ne_bot hb (ha hs)
      exact
        Interval.coe_le_coe.2
          ⟨le_iInf₂ fun c hc => (WithBot.coe_le_coe.1 <| ha hc).1,
            iSup₂_le fun c hc => (WithBot.coe_le_coe.1 <| ha hc).2⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
H : ∀ j < i, x.coeff j = 0
⊢ i ≤ x.order

Tactic:
contrapose! h
    have := H _ h
    rwa [coeff_order_eq_zero] at this

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

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ x.coeff (x.orderTop.untop ⋯) + y.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)

Tactic:
rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]

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

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 < (ofLex x).leadingCoeff →
    ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i

Tactic:
intro hpos
    have hne : (ofLex x) ≠ 0 := leadingCoeff_ne_zero.mp hpos.ne.symm
    have htop : (ofLex x).orderTop ≠ ⊤ := orderTop_ne_top.2 hne
    refine ⟨(ofLex x).orderTop.untop htop, ?_, by simpa [coeff_untop_eq_leadingCoeff] using hpos⟩
    intro j hj
    simpa using (coeff_eq_zero_of_lt_orderTop ((WithTop.lt_untop_iff htop).mp hj)).symm

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a * (d * c) = a * (c * d)

Tactic:
mul_comm

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

Goal state before:
pp: case inl.inr
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 : G
ha : 0 ≤ a
hab : a ≤ 0
hb : 0 ≤ 0
⊢ ↑(#(Ico 0 (a + 0))) - ↑(#(Ico 0 (-(a + 0)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 0)) - ↑(#(Ico 0 (-0))))

Tactic:
obtain rfl := ha.antisymm hab

Goal state after:
case inl.inr
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
hb ha : 0 ≤ 0
hab : 0 ≤ 0
⊢ ↑(#(Ico 0 (0 + 0))) - ↑(#(Ico 0 (-(0 + 0)))) = ↑(#(Ico 0 0)) - ↑(#(Ico 0 (-0))) + (↑(#(Ico 0 0)) - ↑(#(Ico 0 (-0))))
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this✝ : 0 ≤ ↑b
x : G
h₁ : 0 ≤ x
h₂ : x < ↑b
hx' : ¬x = 0
this : 0 ≤ ↑b ∧ ↑b ≤ a
⊢ x ∈ Icc 0 a

Tactic:
simpa [h₁] using! h₂.le.trans this.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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Nonempty (ArchimedeanStrata K M)

Tactic:
have hstratum (c : FiniteArchimedeanClass M) :
      ∃ G : Submodule K M, Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c :=
    IsModularLattice.exists_disjoint_and_sup_eq (ball_lt_closedBall _).le
  choose g h1 h2 using hstratum
  exact ⟨g, h1, h2⟩

Goal state after:
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 α
m✝ n₁✝ n₂✝ : α
⊢ n₁✝ ≤ n₂✝ → m✝ * n₁✝ ≤ m✝ * n₂✝

Tactic:
intro

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ m✝ * n₁✝ ≤ m✝ * n₂✝
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 α
m✝ n₁✝ n₂✝ : α
⊢ n₁✝ ≤ n₂✝ → swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝ ≤ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝

Tactic:
intro

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝ ≤ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⊥ * x = ⊥

Tactic:
by
  rw [← sSup_empty, sSup_mul_distrib]
  simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]

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

Goal state before:
pp: case mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ 0
z : ArchimedeanClass R
y : R
hyz : (fun x_1 ↦ mk x + x_1) (mk y) = (fun x_1 ↦ mk x + x_1) z
⊢ mk y = z

Tactic:
induction z with | mk z =>
  simpa [← mk_mul, mk_eq_mk, mul_left_comm _ (|x|), abs_pos.2 hx] using hyz

Goal state after:
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:
mul_comm

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.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inr
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
hn : q ≠ 0
⊢ 0 ≤ mk ↑q

Tactic:
mk_ratCast hn

Goal state after:
case inr
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
hn : q ≠ 0
⊢ 0 ≤ 0
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✝ : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x✝ : Γ
⊢ ∑ ij ∈ antidiagonal ⋯ ⋯ x✝, x.coeff ij.1 * y.coeff ij.2 = ∑ ij ∈ antidiagonal ⋯ ⋯ x✝, y.coeff ij.1 * x.coeff ij.2

Tactic:
mul_comm

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✝ : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x✝ : Γ
⊢ ∑ ij ∈ antidiagonal ⋯ ⋯ x✝, x.coeff ij.1 * y.coeff ij.2 = ∑ x_1 ∈ antidiagonal ⋯ ⋯ x✝, x.coeff x_1.2 * y.coeff x_1.1
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 : ℕ
⊢ n • x.orderTop ≤ (x ^ n).orderTop

Tactic:
by
  induction n with
  | zero =>
    simp only [zero_smul, pow_zero]
    by_cases h : NeZero (1 : R)
    · simp
    · have : Subsingleton R := not_nontrivial_iff_subsingleton.mp fun _ ↦ h NeZero.one
      simp
  | succ n ih =>
    rw [add_nsmul, pow_add]
    calc
      n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop := by gcongr
      (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
      (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
      (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.single.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ : α
h : x ≈ b✝
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧

Tactic:
exact (H _ _ h).le

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.tail.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ c✝ : α
a✝ : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x b✝
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧
h : b✝ ≈ c✝
⊢ Quotient.lift f H ⟦b✝⟧ ≤ Quotient.lift f H ⟦c✝⟧

Tactic:
exact (H _ _ h).le

Goal state after:
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✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
⊢ {a | y.coeff a ≠ z.coeff a} ⊆ y.support ∪ z.support

Tactic:
intro

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
a✝ : Γ
⊢ a✝ ∈ {a | y.coeff a ≠ z.coeff a} → a✝ ∈ y.support ∪ z.support
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
have : x ≠ 0 := fun h => hr (by rw [h]; exact R.zero_mem)

Goal state after:
case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
this : x ≠ 0
⊢ x ∈ R.ofPrime (R.idealOfLE S h)
Module: Mathlib.Algebra.Order.UpperLower

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

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : UpperSet α
⊢ s * 1 = s

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : UpperSet α
⊢ 1 * s = s
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : LowerSet α
⊢ s * 1 = s

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : LowerSet α
⊢ 1 * s = s
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
⊢ 0 < mk (x - f r) ↔ stdPart x = r

Tactic:
refine (FiniteResidueField.mk_eq_zero
    (x := .mk x hx - .mk _ (mk_map_nonneg_of_archimedean f r))).symm.trans ?_

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
⊢ FiniteResidueField.mk (FiniteElement.mk x hx - FiniteElement.mk (f r) ⋯) = 0 ↔ stdPart x = r
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
⊢ eval y (map (evalRingHom x) p) = evalEval x y p

Tactic:
eval_map,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
⊢ eval₂ (evalRingHom x) y p = evalEval x y p
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)

Tactic:
eval_map,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
⊢ eval₂ (mapRingHom f) (map f q) p = map f (eval q p)