mathlib-initiative/mathlib-tactics huggingface dataset:
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 y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
⊢ ((ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧ ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) →
    ∃ n, |y| ≤ n • |x|

Tactic:
by simp [hgt.not_gt, hgt.ne']

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

Goal state before:
pp: α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ f (-b) < f (a + b + -b)

Tactic:
simpa [Neg b] using hab

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

Goal state before:
pp: case cons
R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : s ≠ 0 → ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
⊢ ∃ b ∈ a ::ₘ s, f (Multiset.map g (a ::ₘ s)).sum ≤ f (g b)

Tactic:
simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]

Goal state after:
case cons
R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : s ≠ 0 → ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
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
⊢ ↑c < ↑d

Tactic:
exact h

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
⊢ ∃ n, x < ↑n

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg hx

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
n : ℕ
hn : x < ↑n
⊢ ∃ n, x < ↑n
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : y + x = z + x
⊢ y = z

Tactic:
← add_comm x

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : x + y = x + z
⊢ y = z
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
⊢ x.order + y.order ≤ (x * y).order

Tactic:
order_of_ne <| leadingCoeff_ne_zero.mp hx,

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 ⋯ + y.order ≤ (x * y).order
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case zero
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
⊢ 0 • x.orderTop ≤ (x ^ 0).orderTop

Tactic:
simp only [zero_smul, pow_zero]

Goal state after:
case zero
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
⊢ 0 ≤ orderTop 1
Module: Mathlib.Order.Quotient

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

Tactic:
exact .inl <| .single <| .inl h

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
n : ℕ
r : R
⊢ (single a) r ^ n = (single (n • a)) (r ^ n)

Tactic:
induction n with
  | zero => ext; simp only [pow_zero, coeff_one, zero_smul, coeff_single]
  | succ n IH => rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]

Goal state after:
Module: Mathlib.Order.Quotient

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

Tactic:
cases h₂ with

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

Goal state before:
pp: case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g i : Γ
left✝¹ : i ∈ x.support
j : Γ
left✝ : j ∈ y.support
h1 : (f i, f j) ∈ antidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (f i, f j).1 * (embDomain f y).coeff (f i, f j).2 ≠ 0
⊢ ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (f i, f j)

Tactic:
simp only [mem_antidiagonal, embDomain_coeff, mem_support, ← hf,
        OrderEmbedding.eq_iff_eq] at h1

Goal state after:
case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g i : Γ
left✝¹ : i ∈ x.support
j : Γ
left✝ : j ∈ y.support
h2 : (embDomain f x).coeff (f i, f j).1 * (embDomain f y).coeff (f i, f j).2 ≠ 0
h1 : x.coeff i ≠ 0 ∧ y.coeff j ≠ 0 ∧ i + j = g
⊢ ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (f i, f j)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case inr
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 y : ↥(↑f).domain
hnontrivial : Nontrivial M
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
have hnonempty : Nonempty (FiniteArchimedeanClass M) := inferInstance

Goal state after:
case inr
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 y : ↥(↑f).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty (FiniteArchimedeanClass M)
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
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 : ↥(↑f).domain
hx0 : x = 0
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x

Tactic:
simp [hx0]

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

Goal state before:
pp: case hfg
Γ : 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
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ j ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ antidiagonal ⋯ ⋯ (a + x.order),
    j ≠ (a, x.order) → y.coeff j.1 * x.coeff j.2 = z.coeff j.1 * x.coeff j.2

Tactic:
simp +contextual only [mem_union, mem_antidiagonal, mul_eq_mul_right_iff, Prod.mk.injEq,
        ne_eq, ← or_and_right, or_false, and_imp, Prod.forall, mem_support, not_and]
      rintro b c - hxb hbc hbc'
      contrapose! hbc'
      rwa [eq_comm, eq_comm (a := c), ← add_eq_add_iff_eq_and_eq
        (Set.IsWF.min_le this hyz ((Set.mem_ofPred (p := fun a => y.coeff a ≠ z.coeff a)).mpr hbc'))
        (order_le_of_coeff_ne_zero hxb), eq_comm]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1

Tactic:
· refine ⟨⟨1, ⟨⟨_, hh⟩, ?_⟩⟩, mul_inv_cancel₀ h⟩
      exact mem_nonZeroDivisors_iff_ne_zero.2 fun c => h (inv_eq_zero.mp (congr_arg Subtype.val c))

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f a - f b = f (a - b)

Tactic:
by
  conv => lhs; rw [← tsub_add_cancel_of_le h]
  rw [map_add, add_tsub_cancel_right]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ (OrderDual.ofDual b).asIdeal ≤ (OrderDual.ofDual a).asIdeal

Tactic:
exact h

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ A.valuation.valuationSubring = A

Tactic:
by
  ext; rw [← A.valuation_le_one_iff]; rfl

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

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

Tactic:
← Set.iUnion_smul_set

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet (⋃ a ∈ s, a • t)
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : UpperSet α
⊢ Set.Ici 1 • ↑s ⊆ ↑s

Tactic:
← Set.iUnion_smul_set

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : UpperSet α
⊢ ⋃ a ∈ Set.Ici 1, a • ↑s ⊆ ↑s
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : LowerSet α
⊢ Set.Iic 1 • ↑s ⊆ ↑s

Tactic:
← Set.iUnion_smul_set

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : LowerSet α
⊢ ⋃ a ∈ Set.Iic 1, a • ↑s ⊆ ↑s
Module: Mathlib.Algebra.Order.UpperLower

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

Tactic:
LowerSet.coe_mul,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(lowerClosure (s * t)) = ↑(lowerClosure s) * ↑(lowerClosure t)
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a • s = s ↔ a • s ⊆ s

Tactic:
Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).ge

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a • s = s ↔ a • s = s
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
n : ℕ
a : R[X]
⊢ eval x ((aeval (C y)) ((aeval Y) a)) * x ^ n = (aeval y) a * x ^ n

Tactic:
induction a using Polynomial.induction_on' <;> aesop (add norm add_mul)

Goal state after:
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.mirror.natDegree = p.natDegree

Tactic:
rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
    tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
by_cases hp : p = 0
  · rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
  rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : (ofFn n) v ≠ 0
⊢ n ≠ 0

Tactic:
contrapose h
  subst h
  simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
⊢ Irreducible f

Tactic:
by
  constructor
  · exact h1
  · intro g h fgh
    let k := g * h.mirror
    have key : f * f.mirror = k * k.mirror := by
      rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h,
        mul_comm g.mirror, mul_assoc, ← mul_assoc]
    have g_dvd_f : g ∣ f := by
      rw [fgh]
      exact dvd_mul_right g h
    have h_dvd_f : h ∣ f := by
      rw [fgh]
      exact dvd_mul_left h g
    have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
    have h_dvd_k_rev : h ∣ k.mirror := by
      rw [mirror_mul_of_domain, mirror_mirror]
      exact dvd_mul_left h g.mirror
    have hk := h2 k key
    rcases hk with (hk | hk | hk | hk)
    · exact Or.inr (h3 h_dvd_f (by rwa [← hk]))
    · exact Or.inr (h3 h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))
    · exact Or.inl (h3 g_dvd_f (by rwa [← hk]))
    · exact Or.inl (h3 g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
have : x ∉ xs := fun hx ↦ hxy (antisymm h.1.1 (h.2.1 x hx))

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X - C (-q.coeff 0) ∣ p

Tactic:
apply h

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑n

pp: case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n

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

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

Goal state after:
case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n

case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).natTrailingDegree = k

Tactic:
refine
    natTrailingDegree_eq_of_trailingDegree_eq_some
      ((Finset.le_inf fun i h => ?_).antisymm <|
          trailingDegree_le_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ (trinomial k m n u v w).support
⊢ ↑k ≤ ↑i
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)

Tactic:
refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩

Goal state after:
case cons.refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ i ∉ s

case cons.refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ (↑(Finset.cons i s ?cons.refine_1)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
hn : n = n'
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
subst hk

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' n' : ℕ
hmn' : m' < n'
x y z : ℤˣ
hn : n = n'
hkm' : k < m'
hq : q = trinomial k m' n' ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t) • z = s • t • z

Tactic:
by ext <;> exact smul_assoc _ _ _

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
⊢ w = 0

Tactic:
have : norm z • w = 0 := by
      rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_mul]

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : norm z • w = 0
⊢ w = 0
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
⊢ 0 ∈ r • t ↔ 0 ∈ t

Tactic:
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff hr, mem_coe]

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_toAddCommMonoid
R : Type u
toAddCommMonoid✝¹ : AddCommMonoid R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommMonoid✝ : AddCommMonoid R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommMonoid✝¹ = toAddCommMonoid✝

Tactic:
ext : 1

Goal state after:
case e_toAddCommMonoid
R : Type u
toAddCommMonoid✝¹ : AddCommMonoid R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommMonoid✝ : AddCommMonoid R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HAdd.hAdd = HAdd.hAdd
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁.toAddMonoid = inst₂.toAddMonoid

Tactic:
ext : 1

Goal state after:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ HAdd.hAdd = HAdd.hAdd