mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x.order = y.order
hyne : (single y.order) y.leadingCoeff ≠ 0
⊢ False

Tactic:
rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy, single_eq_zero] at hyne

Goal state after:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x.order = y.order
hyne : 0 ≠ 0
⊢ False
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : R⟦Γ⟧
⊢ (-f).order = f.order

Tactic:
by_cases hf : f = 0
  · simp only [hf, neg_zero]
  simp only [order, support_neg, neg_eq_zero]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
⊢ a + c ≤ b + c

Tactic:
obtain rfl | hlt := hab.eq_or_lt

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a c : Lex R⟦Γ⟧
hab : a ≤ a
⊢ a + c ≤ a + c

case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c ≤ b + c
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
h✝ : toLex (ao, ac) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, ac))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))

Tactic:
induction ac using FiniteArchimedeanClass.ind with | mk a ha

Goal state after:
case inl.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
a : R
ha : a ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, FiniteArchimedeanClass.mk a ha)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

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

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case mpr
Γ : 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
hr : ¬r = 0
a1 : Γ
a2 : Γ'
hx : ¬((of R).symm x).coeff a2 = 0
⊢ a1 = a1 ∧ a2 ∈ ((of R).symm x).support ∧ a1 +ᵥ a2 = a1 +ᵥ a2
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case succ
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝³ : AddMonoid α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : α
n : ℕ
a✝ : f (n • a) ≤ f a
⊢ f ((n + 1) • a) ≤ f a

Tactic:
rw [add_nsmul]
    apply le_trans <| hna (n • a) (1 • a)
    simpa

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✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f y < f x
⊢ f (x + y) = f x

Tactic:
by_contra! h
  have h1 : f (x + y) ≤ f x := (hna x y).trans_eq (max_eq_left_of_lt h_lt)
  apply lt_irrefl (f x)
  calc
    f x = f (x + y + -y) := by simp
    _   ≤ max (f (x + y)) (f (-y)) := hna (x + y) (-y)
    _   < max (f x) (f x) := by
      rw [max_self, map_neg_eq_map]
      apply max_lt (lt_of_le_of_ne h1 h) h_lt
    _   = f x := max_self (f x)

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 y : ArchimedeanClass R
h : x ≤ y
z : ArchimedeanClass R
⊢ x + z ≤ y + z

Tactic:
induction x with | mk x
    induction y with | mk y
    induction z with | mk z
    rw [← mk_mul, ← mk_mul]
    exact mk_mul_le_of_le h le_rfl

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

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

Tactic:
simpa [← mk_mul, mk_eq_mk, mul_left_comm _ (|x|), abs_pos.2 hx] using hyz

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 : x ≠ 0
⊢ IsAddRegular (mk x)

Tactic:
by
  rw [← isAddLeftRegular_iff_isAddRegular]
  rintro y z hyz
  induction y with | mk y =>
  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.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 = a ∧ a2 = b → a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
hr : ¬r = 0
a1 a2 : Γ
hx : ¬x.coeff a1 = 0
⊢ a1 ∈ x.support ∧ a2 = a2 ∧ a1 + a2 = a1 + a2
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
⊢ 0 < (x - 1).orderTop → x.orderTop = 0 ∧ x.leadingCoeff = 1

pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
⊢ x.orderTop = 0 ∧ x.leadingCoeff = 1 → 0 < (x - 1).orderTop

Tactic:
· intro hx
    constructor
    · rw [← sub_add_cancel x 1, add_comm, ← orderTop_one (R := R)]
      exact orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)
    · rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]
      exact leadingCoeff_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

Goal state after:
case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
⊢ x.orderTop = 0 ∧ x.leadingCoeff = 1 → 0 < (x - 1).orderTop
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
⊢ (ofLex (↑seed.baseEmbedding ⟨f'.sum fun d x ↦ ↑x, ⋯⟩)).coeff d =
    ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d

Tactic:
rw [seed.coeff_baseEmbedding rfl]

Goal state after:
case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
⊢ (seed.coeff d) (f' d) = ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case e'_2.e'_5
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
⊢ f.evalCoeff 0 = coeff 0

Tactic:
ext c

Goal state after:
case e'_2.e'_5
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
c : FiniteArchimedeanClass M
⊢ f.evalCoeff 0 c = coeff 0 c
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg
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
k : K
x : M
hk : ¬k = 0
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ } = k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ }

Tactic:
ext c

Goal state after:
case neg
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ }.coeff c =
    (k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ }).coeff c
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy : (i : ι) → A i
this : closure (Set.range fun s ↦ star s * s) = pi Set.univ fun i ↦ closure (Set.range fun s ↦ star s * s)
⊢ (∃ p, (∀ (i : ι), p i ∈ closure (Set.range fun s ↦ star s * s)) ∧ xy = xa + p) →
    ∀ (i : ι), ∃ p ∈ closure (Set.range fun s ↦ star s * s), xy i = xa i + p

Tactic:
simp only [forall_exists_index, and_imp]
      intro x h rfl i
      exact ⟨x i, by simp [h]⟩

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
this : ↑y - x ≠ 0
⊢ f.eval x ≠ ↑↑f y

Tactic:
sub_ne_zero,

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
this : ↑y ≠ x
⊢ f.eval x ≠ ↑↑f y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ ¬mk ↑x ≤ 0 ↔ ¬mk ↑x = 0

Tactic:
x.2.ge_iff_eq'

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ ¬mk ↑x = 0 ↔ ¬mk ↑x = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ ArchimedeanClass.mk ↑x ≤ 0 ↔ ArchimedeanClass.mk ↑x = 0

Tactic:
x.2.ge_iff_eq'

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ ArchimedeanClass.mk ↑x = 0 ↔ ArchimedeanClass.mk ↑x = 0
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_2
inst✝ : AddMonoidWithOne α
⊢ untop₀ 1 = 1

Tactic:
convert WithTop.untop₀_natCast 1
  all_goals exact Nat.cast_one.symm

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
refine ⟨?_, hp.monic.mul hq.monic⟩

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).natDegree = m + n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
a b : R
⊢ (-(C a * X - C b)).natDegree < 2

Tactic:
by
    rw [natDegree_neg]
    calc
    _ ≤ max (C a * X).natDegree (C b).natDegree := natDegree_sub_le ..
    _ = (C a * X).natDegree := by simp
    _ < 2 := natDegree_C_mul_le .. |>.trans natDegree_X_le |>.trans_lt one_lt_two

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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
⊢ ∃ f, (↑f).domain = ⊤

Tactic:
obtain ⟨f, hf⟩ := exists_isMax seed
  refine ⟨f, Submodule.eq_top_iff'.mpr ?_⟩
  rw [isMax_iff_forall_not_lt] at hf
  contrapose! hf with hx
  obtain ⟨x, hx⟩ := hx
  exact ⟨f.extend hx, f.lt_extend hx⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : (ofFn n) v = 0
⊢ ⊥ < ↑n

Tactic:
exact Batteries.compareOfLessAndEq_eq_lt.mp rfl

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

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

Tactic:
rw [eval_eq_sum, smeval_eq_sum]

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
p : R[X]
⊢ (p.sum fun e a ↦ a * r ^ e) = p.sum (smul_pow r)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ eval₂ RingHom.smulOneHom x p = p.sum (smul_pow x)

Tactic:
eval₂_eq_sum

Goal state after:
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ (p.sum fun e a ↦ RingHom.smulOneHom a * x ^ e) = p.sum (smul_pow x)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) r ∣ z ↔ r ∣ z.re ∧ r ∣ z.im

Tactic:
constructor
  · rintro ⟨x, rfl⟩
    simp
  · rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
    use ⟨r, i⟩
    simp [QuadraticAlgebra.ext_iff, hr, hi, ← C_eq_algebraMap]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case incl
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x : EnvelGroup R
x✝ : R
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦incl x✝⟧ =
    F ⟦incl x✝⟧

Tactic:
| incl =>

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid := by
    ext : 1 <;> assumption

Goal state after:
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case symm
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x y : R
a✝ : Relation.EqvGen (Rel r) x y
hxy : ∀ {c d : R}, Relation.EqvGen (Rel r) c d → Relation.EqvGen (Rel r) (x * c) (y * d)
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (y * c) (x * d)

Tactic:
| symm x y _ hxy =>

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
⊢ single a (f.coeff a) + (erase a) f = f

Tactic:
ext; simp [ coeff_add, Finsupp.single_add_erase]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case symm
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x y : R
a✝ : Relation.EqvGen (Rel r) x y
hxy : ∀ {c d : R}, Relation.EqvGen (Rel r) c d → Relation.EqvGen (Rel r) (x + c) (y + d)
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (y + c) (x + d)

Tactic:
| symm x y _ hxy =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ X * (monomial n) r = (monomial (n + 1)) (φ r)

Tactic:
simp [X_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : SkewPolynomial R
n : ℕ
⊢ (p - q).coeff n = p.coeff n - q.coeff n

Tactic:
by
  simp_rw [sub_eq_add_neg, ← coeff_neg, SkewPolynomial.coeff_add]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p f

Tactic:
rw [← sum_single f, sum_def']
  exact Finset.sum_induction _ _ add zero (by simp_all)

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case mpr
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : WithConv ((m → R) →ₗ[R] n → R)
⊢ IsSelfAdjoint f ↔ ∀ (i : n) (j : m), IsSelfAdjoint (toMatrix' f.ofConv i j)

Tactic:
simp [IsSelfAdjoint, ← toMatrix'.injective.eq_iff, toMatrix'_intrinsicStar, ← Matrix.ext_iff,
    WithConv.ext_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pullback

Goal state before:
pp: C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
D : Type u₃
inst✝⁷ : Category.{v₃, u₃} D
G : C ⥤ D
A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁵ : G.IsContinuous J K
inst✝⁴ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasLeftKanExtension F
inst✝³ : RepresentablyFlat G
inst✝² : HasSheafify K A
inst✝¹ : HasSheafify J A
inst✝ : PreservesFiniteLimits G.op.lan
⊢ PreservesFiniteLimits (sheafPullback G A J K)

Tactic:
have : PreservesFiniteLimits (G.op.lan ⋙ presheafToSheaf K A) :=
    comp_preservesFiniteLimits _ _
  apply comp_preservesFiniteLimits

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ Y.presheaf.stalk ((ConcreteCategory.hom α.base) x) = Y.presheaf.stalk ((ConcreteCategory.hom β.base) x')

Tactic:
rw [h₁, h₂]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c

Tactic:
· apply ((TopCat.Sheaf.pushforward _ β.hom.base).obj X.sheaf).hom_ext _
      PrimeSpectrum.isBasis_basic_opens
    intro r
    apply (StructureSheaf.to_basicOpen_epi R r).1
    simpa using! h r

Goal state after: