mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t : NonemptyInterval α
hb : ↑s ≤ ↑t
c : NonemptyInterval α
hc : ↑s ≤ ↑c
⊢ ↑s ≤
    match ↑t, ↑c with
    | none, x => ⊥
    | x, none => ⊥
    | some s, some t =>
      if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ }
      else ⊥

Tactic:
change _ ≤ dite _ _ _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t : NonemptyInterval α
hb : ↑s ≤ ↑t
c : NonemptyInterval α
hc : ↑s ≤ ↑c
⊢ ↑s ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }
    else ⊥
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ pure a⁻¹ = pure b

Tactic:
inv_eq_of_mul_eq_one_right hab

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ pure b = pure b
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
refine (eq_empty_of_subset_empty ?_).symm

Goal state after:
case neg.inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ⋂ s ∈ S, ↑s ⊆ ∅
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop (-y).orderTop ≤ (x + -y).orderTop

Tactic:
exact min_orderTop_le_orderTop_add

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
u : ArchimedeanStrata K M
⊢ iSupIndep u.stratum

Tactic:
intro c
  rw [Submodule.disjoint_def']
  intro a ha b hb hab
  obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ b).mp hb
  obtain hf' := congr(ArchimedeanClass.mk $hf)
  contrapose! hf' with h0
  rw [← hab, DFinsupp.sum]
  by_cases! hnonempty : f.support.Nonempty
  · have hmem (x : FiniteArchimedeanClass M) : (f x).val ∈ u.stratum x :=
      Set.mem_of_mem_of_subset (f x).prop (by simp)
    have hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk (f i).val) f.support := by
      intro x hx y hy hxy
      change ArchimedeanClass.mk (f x).val < ArchimedeanClass.mk (f y).val
      rw [u.archimedeanClassMk_of_mem_stratum (hmem x) (by simpa using hx)]
      rw [u.archimedeanClassMk_of_mem_stratum (hmem y) (by simpa using hy)]
      exact hxy
    rw [ArchimedeanClass.mk_sum hnonempty hmono, u.archimedeanClassMk_of_mem_stratum (hmem _)
      (by simpa using f.support.min'_mem hnonempty), ← val_mk h0, Subtype.coe_ne_coe]
    by_contra!
    obtain h := this ▸ Finset.min'_mem f.support hnonempty
    contrapose! h
    have := u.archimedeanClassMk_of_mem_stratum ha h0
    rw [← val_mk h0, ← Subtype.ext_iff] at this
    simpa [DFinsupp.notMem_support_iff, this] using (f c).prop
  · rw [hnonempty]
    symm
    simpa using h0

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
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
⊢ 0 < f.sum fun x x_1 ↦ ↑x_1

Tactic:
rw [hf]

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
⊢ 0 < ↑x
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
hxy : ¬(of R).symm (x • y) = 0
⊢ ↑(⋯.min ⋯) ≤ ((of R).symm (x • y)).orderTop

Tactic:
rw [HahnSeries.orderTop_of_ne_zero hxy, WithTop.coe_le_coe]
    exact Set.IsWF.min_le_min_of_subset support_smul_subset_vadd_support

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : ArchimedeanClass R
⊢ 0 • x = 0

Tactic:
induction x with | mk x => rw [← mk_pow, pow_zero, mk_one]

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

Goal state before:
pp: case mk.mk.mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x ≤ mk y
z : R
⊢ mk (x * z) ≤ mk (y * z)

Tactic:
exact mk_mul_le_of_le h le_rfl

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
⊢ ∑ x_1 ∈ antidiagonal ⋯ ⋯ x✝, f (x.coeff x_1.1) * f (y.coeff x_1.2) =
    ∑ x_1 ∈ antidiagonal ⋯ ⋯ x✝, f (x.coeff x_1.1) * f (y.coeff x_1.2)

Tactic:
refine Eq.symm (sum_subset (fun gh hgh => ?_) (fun gh hgh hz => ?_))

Goal state after:
case refine_1
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : gh ∈ antidiagonal ⋯ ⋯ x✝
⊢ gh ∈ antidiagonal ⋯ ⋯ x✝

case refine_2
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : gh ∈ antidiagonal ⋯ ⋯ x✝
hz : gh ∉ antidiagonal ⋯ ⋯ x✝
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n * x ^ 1).orderTop

Tactic:
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.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
x y : R
⊢ x ∈ P → y ∈ P → x + y ∈ P

Tactic:
simpa using add

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

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ x ∈ R

Tactic:
by rw [h]; exact R.zero_mem

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

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
⊢ B = ⊤

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hlt.le

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : A = B
⊢ B = ⊤

case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : B = ⊤
⊢ B = ⊤
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ (⇑(Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))) ∘ ⇑↑A.unitGroupMulEquiv) x✝ = 1 ↔
    (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))) (A.unitGroupMulEquiv x✝) = 1

Tactic:
MonoidHom.coe_coe,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ (⇑(Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))) ∘ ⇑A.unitGroupMulEquiv) x✝ = 1 ↔
    (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))) (A.unitGroupMulEquiv x✝) = 1
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:
rw [mul_comm]
      exact one_mul _

Goal state after:
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:
rw [mul_comm]
      exact one_mul _

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

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

Tactic:
injective_iff_map_eq_zero

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
⊢ ∀ (a : R), (ofArchimedean f) a = 0 → a = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
⊢ stdPart x = sInf {r | x < f r}

Tactic:
obtain ⟨a, ha⟩ := exists_int_lt_of_mk_nonneg hx
    obtain ⟨b, hb⟩ := exists_int_gt_of_mk_nonneg hx
    have hn : {r | x < f r}.Nonempty := ⟨b, by simpa using hb⟩
    have hb : BddBelow {r | x < f r} := by
      refine ⟨a, fun r hr ↦ ?_⟩
      by_contra! hra
      exact (f.monotone' hra.le).not_gt (by simpa using ha.trans hr)
    apply stdPart_eq f <;> intro r hr
    · simpa using notMem_of_lt_csInf hr hb
    · obtain ⟨s, hs, hs'⟩ := (csInf_lt_iff hb hn).1 hr
      exact hs.le.trans (f.monotone' hs'.le)

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
p q : A[X]
⊢ (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) (p * q) =
    p • (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) q +
      q • (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) p

Tactic:
dsimp
    induction p using Polynomial.induction_on' with
    | add => simp only [add_mul, map_add, add_smul, smul_add, add_add_add_comm, *]
    | monomial n a =>
      induction q using Polynomial.induction_on' with
      | add => simp only [mul_add, map_add, add_smul, smul_add, add_add_add_comm, *]
      | monomial m b => ext; simp [Polynomial.monomial_mul_monomial, add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
P : R[X]
⊢ (-P).coeffList = List.map (fun x ↦ -x) P.coeffList

Tactic:
by
  by_cases hp : P = 0
  · rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
  · simp [coeffList]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
⊢ d.mapCoeffs X = 0

Tactic:
by
  simp [← monomial_one_one_eq_X, PolynomialModule.single]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : q = 0
⊢ 0 < 0 ↔ p.degree < q.degree

pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : ¬q = 0
⊢ 0 < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree

pp: case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < 0 ↔ p.degree < q.degree

pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree

Tactic:
· simp only [hp, hq, lt_self_iff_false]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : ¬q = 0
⊢ 0 < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree

case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < 0 ↔ p.degree < q.degree

case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree
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.Monic
h_irr : Irreducible (map φ f)
⊢ Irreducible f

Tactic:
refine ⟨h_irr.not_isUnit ∘ IsUnit.map (mapRingHom φ), fun a b h => ?_⟩

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.Monic
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n₁ : ℕ
x✝⁴ : n₁ ∈ Finset.range (p.natDegree + 1)
x✝³ : p.mirror.coeff n₁ ≠ 0
x✝² : ℕ
x✝¹ : x✝² ∈ Finset.range (p.natDegree + 1)
x✝ : p.mirror.coeff x✝² ≠ 0
h : (revAt (p.natDegree + p.natTrailingDegree)) n₁ = (revAt (p.natDegree + p.natTrailingDegree)) x✝²
⊢ n₁ = x✝²

Tactic:
by rw [← @revAt_invol _ n₁, h, revAt_invol]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ Irreducible p

pp: case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ Irreducible p

Tactic:
· rw [Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three hdeg2 hdeg.2]
    apply Multiset.eq_zero_of_forall_notMem
    simp_all

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ Irreducible p
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp :
  #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3 ∧
    ∀ k_1 ∈ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support,
      IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
rw [support_trinomial hkm hmn hx hy hz] at hp

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
| inl hk =>

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ : ((X - C η) * (monomial d) c).nextCoeff = -(η * c)
h₂ : ((X - C η) * (monomial d) c).eraseLead ≠ 0
h₃ : SignType.sign c ≠ SignType.sign (-(η * c))
⊢ ((monomial d) c).signVariations + 1 ≤ ((X - C η) * (monomial d) c).signVariations

Tactic:
simpa [h₁, h₂, h₃, hc, hη.ne', signVariations, List.destutter_cons_cons,
    ← leadingCoeff_cons_eraseLead, coeffList_eraseLead, leadingCoeff_eraseLead_eq_nextCoeff]
  using! List.length_pos_of_ne_nil (List.destutter'_ne_nil _ _)

Goal state after:
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
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨⟨⟩⟩

Goal state after:
R : Type u
inst₂ : AddMonoidWithOne R
toAddMonoid✝ : AddMonoid R
toOne✝ : One R
natCast✝ : ℕ → R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toAddMonoid =
    inst₂.toAddMonoid
h_zero' :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toZero =
    inst₂.toZero
h_one' :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toOne =
    inst₂.toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
      natCast_succ := natCast_succ✝ } =
    inst₂
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ {B.i, B.j, B.k} ⊆ ↑B.liftHom.range

Tactic:
rintro x (rfl | rfl | rfl)
      <;> [use (Basis.self R).i; use (Basis.self R).j; use (Basis.self R).k]

Goal state after:
case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.toRingHom (Basis.self R).i = B.i

case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.toRingHom (Basis.self R).j = B.j

case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.toRingHom (Basis.self R).k = B.k
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ ^ 1 =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹ ^ (↑0 + 1)
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)

Tactic:
Fin.val_zero,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ ^ 1 =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹ ^ (0 + 1)
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ (algebraMap R[X] K) q₁ + ∑ x ∈ s, (algebraMap R[X] K) (r₁ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ (↑0 + 1) =
    (algebraMap R[X] K) q₂ + ∑ x ∈ s, (algebraMap R[X] K) (r₂ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ (↑0 + 1)

Tactic:
Fin.val_zero,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ (algebraMap R[X] K) q₁ + ∑ x ∈ s, (algebraMap R[X] K) (r₁ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ (0 + 1) =
    (algebraMap R[X] K) q₂ + ∑ x ∈ s, (algebraMap R[X] K) (r₂ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ (0 + 1)