mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inl
S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
h✝ : Subsingleton S
⊢ mk ↑n = 0

Tactic:
exact Subsingleton.allEq ..

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : CommRing R
toSubsemiring✝¹ : Subsemiring R
mem_of_isSquare'✝¹ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝¹.carrier
neg_one_notMem'✝¹ : -1 ∉ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹,
        neg_one_notMem' := neg_one_notMem'✝¹ } =
    (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹, neg_one_notMem' := neg_one_notMem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
inst✝ : CommRing R
toSubsemiring✝¹ : Subsemiring R
mem_of_isSquare'✝¹ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝¹.carrier
neg_one_notMem'✝¹ : -1 ∉ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹,
        neg_one_notMem' := neg_one_notMem'✝¹ } =
    (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
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
x : ↥seed.baseEmbedding.domain
⊢ ∀ ⦃b : ↥seed.baseEmbedding.domain⦄, x < b → ↑seed.baseEmbedding x < ↑seed.baseEmbedding b

Tactic:
y

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
inst✝ : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
⊢ x < y → ↑seed.baseEmbedding x < ↑seed.baseEmbedding 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
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧ˣ
⊢ ∀ {b : R⟦Γ⟧ˣ}, x ∈ {x | 0 < (↑x - 1).orderTop} → b ∈ {x | 0 < (↑x - 1).orderTop} → x * b ∈ {x | 0 < (↑x - 1).orderTop}

Tactic:
y

Goal state after:
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
⊢ x ∈ {x | 0 < (↑x - 1).orderTop} → y ∈ {x | 0 < (↑x - 1).orderTop} → x * y ∈ {x | 0 < (↑x - 1).orderTop}
Module: Mathlib.Order.Quotient

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

Tactic:
y

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y : Quotient s
⊢ x ≤ y → Quotient.lift f H x ≤ Quotient.lift f H y
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ P.IsOrdering

Tactic:
· have : HasMemOrNegMem P := ⟨by simp [h]⟩
    refine IsOrdering.mk' P (fun {x y} _ => ?_)
    by_contra
    have := h (-x) y
    have := h (-x) (-y)
    have := h x y
    have := h x (-y)
    cases (by aesop : x ∈ P ∨ -x ∈ P) <;> simp_all [mem_support]

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
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
simp_rw [mk_eq_mk]
    aesop

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 Γ
Γ' : 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⟦Γ⟧
⊢ embDomain f (x * y) = embDomain f x * embDomain f y

Tactic:
by
  ext g
  by_cases hg : g ∈ Set.range f
  · obtain ⟨g, rfl⟩ := hg
    simp only [coeff_mul, embDomain_coeff]
    trans
      ∑ ij ∈
        (antidiagonal x.isPWO_support y.isPWO_support g).map
          (f.toEmbedding.prodMap f.toEmbedding),
        (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2
    · simp
    apply sum_subset
    · rintro ⟨i, j⟩ hij
      simp only [mem_map, mem_antidiagonal,
        Function.Embedding.coe_prodMap, mem_support, Prod.exists] at hij
      obtain ⟨i, j, ⟨hx, hy, rfl⟩, rfl, rfl⟩ := hij
      simp [hx, hy, hf]
    · rintro ⟨_, _⟩ h1 h2
      contrapose! h2
      obtain ⟨i, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).1
      obtain ⟨j, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).2
      simp only [mem_map, mem_antidiagonal,
        Function.Embedding.coe_prodMap, mem_support, Prod.exists]
      simp only [mem_antidiagonal, embDomain_coeff, mem_support, ← hf,
        OrderEmbedding.eq_iff_eq] at h1
      exact ⟨i, j, h1, rfl⟩
  · rw [embDomain_of_notMem_range hg, eq_comm]
    contrapose! hg
    obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset ((mem_support _ _).2 hg)
    obtain ⟨i, _, rfl⟩ := support_embDomain_subset hi
    obtain ⟨j, _, rfl⟩ := support_embDomain_subset hj
    exact ⟨i + j, hf i j⟩

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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
hnonempty : ∃ y, ↑y - x ∈ ball K (seq 0)
⊢ False

Tactic:
obtain ⟨y, hy⟩ := hnonempty

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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
⊢ False
Module: Mathlib.Algebra.Order.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ (posSubgroup R).index = 2

Tactic:
rw [Subgroup.index_eq_two_iff]
  refine ⟨-1, fun a ↦ ?_⟩
  obtain h | h := lt_or_gt_of_ne a.ne_zero
  · simp [h, h.le]
  · simp [h, xor_comm, h.le]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: ι : 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
⊢ closure (Set.range fun s ↦ star s * s) = closure (Set.univ.pi fun i ↦ Set.range fun s ↦ star s * s)

Tactic:
congr

Goal state after:
ι : 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
⊢ (Set.range fun s ↦ star s * s) = Set.univ.pi fun i ↦ Set.range fun s ↦ star s * s
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
toSubring✝¹ : Subring K
mem_or_inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier ∨ x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h :
  { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ }.toSubring =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring
⊢ { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ } =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
K : Type u
inst✝ : Field K
toSubring✝¹ : Subring K
mem_or_inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier ∨ x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h :
  { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ }.toSubring =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring
⊢ { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ } =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }

Tactic:
congr

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

Goal state before:
pp: case neg.inl
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x < 1
⊢ x ∈ B

Tactic:
have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)
      simpa using
        B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B))
          (B.neg_mem _ B.one_mem)

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x⁻¹ ∈ A.nonunits ↔ x = 0 ∨ x ∉ A

Tactic:
mem_nonunits_iff_or,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x⁻¹ = 0 ∨ x⁻¹⁻¹ ∉ A ↔ x = 0 ∨ x ∉ A
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : FiniteResidueField K
hx : 0 ≤ x
y z : FiniteResidueField K
h : y ≤ z
⊢ y * x ≤ z * x

Tactic:
mul_comm _ x

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : FiniteResidueField K
hx : 0 ≤ x
y z : FiniteResidueField K
h : y ≤ z
⊢ x * y ≤ x * z
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ Classical.ofNonempty (FiniteResidueField.mk (FiniteElement.mk x h)) = f (FiniteResidueField.mk (FiniteElement.mk x h))

Tactic:
congr

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ Classical.ofNonempty = f
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : 0 ≤ mk x
⊢ ∀ ⦃b : K⦄, b ∈ {x | 0 ≤ mk x} → x ≤ b → stdPart x ≤ stdPart b

Tactic:
y

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : 0 ≤ mk x
y : K
⊢ y ∈ {x | 0 ≤ mk x} → x ≤ y → stdPart x ≤ stdPart y
Module: Mathlib.Algebra.Order.Ring.StandardPart

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

Tactic:
← FiniteElement.neg_mk,

Goal state after:
case pos
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : 0 ≤ mk x
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (-FiniteElement.mk x ?pos✝) =
    -(Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h✝)

case pos
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : 0 ≤ mk x
⊢ 0 ≤ mk x
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 : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -c • x < a
hc : c = 0
⊢ f.eval (-c • x) < ↑↑f ⟨a, ha⟩

Tactic:
rw [hc] at ⊢ hac

Goal state after:
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 : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -0 • x < a
hc : c = 0
⊢ f.eval (-0 • x) < ↑↑f ⟨a, ha⟩
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.coeff dk

Tactic:
congr

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.degree.succ - 1 - (k + 1) = dk
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
this : f = f.extend hx
⊢ (↑f).domain = (↑(f.extend hx)).domain

Tactic:
congr

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
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x : ↥(sSupFun hc).domain
⊢ ∀ ⦃b : ↥(sSupFun hc).domain⦄, x < b → ↑(sSupFun hc) x < ↑(sSupFun hc) b

Tactic:
y

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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
⊢ x < y → ↑(sSupFun hc) x < ↑(sSupFun hc) y
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]
⊢ (aevalAeval x y) (swap ((monomial n) a)) = (aevalAeval y x) ((monomial n) a)

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

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

Tactic:
show 0 = f 0 by simp

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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
this : ↑(sSupFun hc) (y - x) = ↑f ⟨↑(y - x), hf⟩
f' : Partial seed
left✝ : f' ∈ c
hf' : ↑f' = f
hmono : StrictMono ↑f
⊢ ↑f 0 < ↑f ⟨↑(y - x), hf⟩
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ ∃ q, p = X ^ n + q ∧ q.natDegree < n

Tactic:
refine ⟨p.eraseLead, ?_, ?_⟩
  · nth_rewrite 1 [← p.eraseLead_add_C_mul_X_pow]
    rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]
  · refine p.eraseLead_natDegree_le.trans_lt ?_
    rw [hp.natDegree_eq]
    lia

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 : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (p.natDegree * n)

Tactic:
← hq.natDegree_eq

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (p.natDegree * q.natDegree)
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bg) (Polynomial.map i g) =
    i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)

Tactic:
congr

Goal state after:
case e_a.e_a.e_x.e_a
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ bg = bf
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ IsChain R (destutter' R a (b :: c :: l))

Tactic:
simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ (((R a b → R b c → R a b) ∧ (R a b → R b c → IsChain R (b :: destutter' R c l))) ∧
      (R a b → ¬R b c → IsChain R (a :: destutter' R b l))) ∧
    (¬R a b → R a c → IsChain R (a :: destutter' R c l))
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 1 x = 1 • x ^ 0

Tactic:
← C_1,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ (C 1).smeval x = 1 • x ^ 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
⊢ (trinomial k m n u v 1).Monic

Tactic:
by
  nontriviality R
  exact trinomial_leadingCoeff hkm hmn one_ne_zero

Goal state after: