mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: ⊢ ∀ {a b : ℕ}, DvdNotUnit a b → (if a = 0 then ⊤ else ↑a) < if b = 0 then ⊤ else ↑b

Tactic:
intro a b h

Goal state after:
a b : ℕ
h : DvdNotUnit a b
⊢ (if a = 0 then ⊤ else ↑a) < if b = 0 then ⊤ else ↑b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f * g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply ne_zero_and_ne_zero_of_mul at hf
  exact m.degree_mul hf.1 hf.2

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

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

Tactic:
cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1

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
hf : m.leadingCoeff g ∈ R⁰
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
rw [mul_comm, add_comm, withBotDegree_mul_of_left_mem_nonZeroDivisors (hf := hf)]

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
h : f = 0 ∨ g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

Tactic:
rcases h with 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.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h✝ : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g f : MvPolynomial σ R
⊢ ∀ (g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f

Tactic:
g

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g✝ f g : MvPolynomial σ R
⊢ m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
hs : s < n + 1 ∧ s ∣ n ∧ ∃ x, s = x ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs

Goal state after:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
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) ?_

Goal state after:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = (∏ a ∈ n.primeFactors \ t, a) * ∏ a ∈ t, a
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n d : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
i : Fin d
⊢ f i ∣ n

Tactic:
by
  rw [mem_finMulAntidiag] at hf
  rw [← hf.1]
  exact dvd_prod_of_mem f (mem_univ i)

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

Goal state before:
pp: 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
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1

Tactic:
rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]

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

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n}) = 3 ^ ω n

Tactic:
← card_finMulAntidiag_of_squarefree hn,

Goal state after:
n : ℕ
hn : Squarefree n
⊢ #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n}) = #(finMulAntidiag 3 n)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
    apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
    exact mod_cast hq

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

Goal state before:
pp: F : Type u_1
α : 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 : α
b : β
q : ℚ
⊢ ∀ {a b : β}, (inducedOrderRingHom β γ).toRingHom a ≤ (inducedOrderRingHom β γ).toRingHom b ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩

Goal state after:
F : Type u_1
α : 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 : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ ≤ b✝
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.withBotDegree (-f) = m.withBotDegree f

Tactic:
classical
  simp [m.withBotDegree_eq]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i + -C r) = single i 1

Tactic:
← map_neg,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i + C (-r)) = single i 1
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_1
ι : 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
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : 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
⊢ f ((Equiv.symm σ) a) ≤ f a

Tactic:
specialize hamax (σ.symm a) h1s

Goal state after:
case insert.inr.refine_1
ι : 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 ι
hamax : toLex (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)) ≤ toLex (g a, f a)
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
⊢ f ((Equiv.symm σ) a) ≤ f a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |b * a|ₘ ≤ |a * b|ₘ ^ 2

Tactic:
mul_comm b a,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |a * b|ₘ ≤ |a * b|ₘ ^ 2
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |b * a|ₘ ≤ |a * b|ₘ ^ 2

Tactic:
rw [mul_comm b a, pow_two, mul_le_mul_iff_right]

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ ≤ |a * b|ₘ
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
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk b ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s

Tactic:
exact s.upper h hb

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

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

Tactic:
by
  obtain rfl | hba := hba.eq_or_lt
  · rw [mul_div_cancel₀, cast_le, ceil_le]
    · exact _root_.div_le_self (by positivity) hb.le
    · positivity
  · exact (ceil_lt_mul hb hba).le

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s))

Tactic:
rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
⊢ g1 = g2

Tactic:
have h2 : Nontrivial ↥(Subgroup.zpowers g1) := by rw [h]; exact h'

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
h2 : Nontrivial ↥(Subgroup.zpowers g1)
⊢ g1 = g2
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 : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
h : x = 0
⊢ False

Tactic:
by simp_all [orderTop_zero, WithTop.top_ne_coe]

Goal state after:
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
h : y = 0
⊢ False

Tactic:
by simp_all [orderTop_zero, WithTop.top_ne_coe]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : LocallyFiniteOrder Gˣ
this : StrictMono ⇑(orderMonoidHom Gˣ)
⊢ StrictMono ⇑(orderMonoidWithZeroHom G)

Tactic:
intro a b h

Goal state after:
G : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : LocallyFiniteOrder Gˣ
this : StrictMono ⇑(orderMonoidHom Gˣ)
a b : G
h : a < b
⊢ (orderMonoidWithZeroHom G) a < (orderMonoidWithZeroHom G) b
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case a
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
h0 : a ≠ 0
⊢ ↑c ≤ ArchimedeanClass.mk a

Tactic:
· apply (mem_closedBall_iff K).mp _ h0
    rw [← u.ball_sup_stratum_eq c]
    exact Submodule.mem_sup_right ha

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝ : { a // a ≠ 0 }
x : Lex R⟦Γ⟧
hx : x ≠ 0
⊢ (ofLex x).orderTop ≠ ⊤

Tactic:
simp [orderTop_of_ne_zero (show ofLex x ≠ 0 by exact hx)]

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

Goal state before:
pp: case h₁.h
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Γ × FiniteArchimedeanClass R
⊢ ((finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R)) (toLex x) =
    OrderHom.id (toLex x)

Tactic:
| h x
     => 

Goal state after:
case h₁.h
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Γ × FiniteArchimedeanClass R
⊢ ((finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R)) (toLex x) =
    OrderHom.id (toLex x)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mp
Γ : 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 = b ∧ a2 ∈ ((of R).symm x).support ∧ a1 +ᵥ a2 = b +ᵥ a → a1 = b ∧ a2 = a

Tactic:
rintro ⟨rfl, _, h1⟩
      exact ⟨rfl, IsCancelVAdd.left_cancel a1 a2 a h1⟩

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h
α : Type u_1
s : Setoid α
inst✝ : LE α
x : α
⊢ ⟦x⟧ ≤ ⟦x⟧

Tactic:
| h x
     => 

Goal state after:
case h
α : Type u_1
s : Setoid α
inst✝ : LE α
x : α
⊢ ⟦x⟧ ≤ ⟦x⟧
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h
α : Type u_1
s : Setoid α
inst✝ : LE α
y z : Quotient s
h₂ : y ≤ z
x : α
h₁ : ⟦x⟧ ≤ y
⊢ ⟦x⟧ ≤ z

Tactic:
| h x
     => 

Goal state after:
case h
α : Type u_1
s : Setoid α
inst✝ : LE α
y z : Quotient s
h₂ : y ≤ z
x : α
h₁ : ⟦x⟧ ≤ y
⊢ ⟦x⟧ ≤ z
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : Quotient s
x : α
⊢ ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧

Tactic:
| h x
     => 

Goal state after:
case h
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : Quotient s
x : α
⊢ ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
y : Quotient s
x : α
h₁ : ⟦x⟧ ≤ y
h₂ : y ≤ ⟦x⟧
⊢ ⟦x⟧ = y

Tactic:
| h x
     => 

Goal state after:
case h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
y : Quotient s
x : α
h₁ : ⟦x⟧ ≤ y
h₂ : y ≤ ⟦x⟧
⊢ ⟦x⟧ = y
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✝⁴ : CommSemiring R
A : Type u_6
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Nontrivial Γ
inst✝ : Nontrivial R
⊢ ⊥ ≠ ⊤

Tactic:
rw [Ne, SetLike.ext_iff, not_forall]

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✝⁴ : CommSemiring R
A : Type u_6
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Nontrivial Γ
inst✝ : Nontrivial R
⊢ ∃ x, ¬(x ∈ ⊥ ↔ x ∈ ⊤)
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
a : α
hs : s.OrdConnected
⊢ (a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s)).OrdConnected

Tactic:
exact (upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b * a ∈ s

Tactic:
rwa [← smul_eq_mul, mem_stabilizer_set.1 hb]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ Classical.ofNonempty (FiniteResidueField.mk (FiniteElement.mk x ⋯)) = 0

Tactic:
FiniteResidueField.mk_eq_zero.2 h,

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ Classical.ofNonempty 0 = 0
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
f : ℕ → R → R[X][Y]
⊢ evalEval x y (p.sum f) = p.sum fun n a ↦ evalEval x y (f n a)

Tactic:
simp only [evalEval, eval, eval₂_sum]

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
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c✝
hf' : ↑f' = f
x' : ↥f.domain
hx' : ↑f x' = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
⊢ ↑f.domain ⊆ ↑(sSupFun hc).domain

Tactic:
exact hf'.symm ▸ (le_sSupFun hc hmem').1

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = f.leadingCoeff
⊢ IsUnit a ∨ IsUnit b

Tactic:
h_mon

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff ≠ 0

Tactic:
reverse_leadingCoeff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.trailingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ eval 1 p.mirror = eval 1 p

Tactic:
by
  simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]
  refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_
  · exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n
  · intro n hn hp
    rw [Finset.mem_range_succ_iff] at *
    rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
    rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
    exact natTrailingDegree_le_of_ne_zero hp
  · exact fun n₁ _ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]
  · intro n hn hp
    use revAt (p.natDegree + p.natTrailingDegree) n
    refine ⟨?_, ?_, revAt_invol⟩
    · rw [Finset.mem_range_succ_iff] at *
      rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
      rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]
      exact natTrailingDegree_le_of_ne_zero hp
    · change p.mirror.coeff _ ≠ 0
      rwa [coeff_mirror, revAt_invol]
  · exact fun n _ _ => p.coeff_mirror n

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_1.cast
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
i : Fin n
⊢ (Fin.snoc r (q %ₘ g) i.castSucc).degree < g.degree

Tactic:
| cast i =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_2
inst✝ : Field R
p : R[X]
x : R
⊢ eval x p =
    (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 0) / (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 1)

Tactic:
simp [toTupleMvPolynomial, eval_homogenize]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ((monomial n✝) a).smeval ↑n = ↑(((monomial n✝) a).smeval n)

Tactic:
rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i

Tactic:
exact WithTop.coe_le_coe.mpr (hkm.trans hmn).le

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ∑ n_1 ∈ (trinomial k m n ↑u ↑v ↑w).support, (trinomial k m n ↑u ↑v ↑w).coeff n_1 ^ 2 = 3

Tactic:
trinomial_support hkm hmn u.ne_zero v.ne_zero w.ne_zero,

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ∑ n_1 ∈ {k, m, n}, (trinomial k m n ↑u ↑v ↑w).coeff n_1 ^ 2 = 3