mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = b1.gcd a2 * b2

Tactic:
cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = 1 * b2
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑q ^ 2
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
← cast_pow

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((c1, c2), d1, d2).2.1.gcd ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2 = ((c1, c2), d1, d2).2.2

Tactic:
cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ 1 * ((c1, c2), d1, d2).2.2 = ((c1, c2), d1, d2).2.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
s : Finset ι
hf : ∀ i ∈ s, (f i).IsMultiplicative
⊢ (∏ i ∈ s, f i).IsMultiplicative

Tactic:
induction s using Finset.cons_induction
  case empty => simp
  case cons a s ha ih =>
    rw [Finset.prod_cons]
    exact (hf a (by grind)).mul (by grind)

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

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a = mk b
⊢ mk (f a) = mk (f b)

Tactic:
rw [← orderHom_mk, ← orderHom_mk, h]

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

Goal state before:
pp: case mp
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
hx : x ∈ I
z : M
hz : ∃ c, x = c * z
hz' : Minimal (fun x ↦ x ∈ {x | x ∈ I}) z
⊢ ∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x

Tactic:
rcases hz with ⟨y, rfl⟩

Goal state after:
case mp
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
z : M
hz' : Minimal (fun x ↦ x ∈ {x | x ∈ I}) z
y : M
hx : y * z ∈ I
⊢ ∃ y_1 z_1, Minimal (fun x ↦ x ∈ I) z_1 ∧ y_1 * z_1 = y * z
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
⊢ x ∈ range #s → c - ↑x ∈ Ioc (c - ↑(#s)) c

Tactic:
mx

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - ↑x ∈ Ioc (c - ↑(#s)) c
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
⊢ x ∈ ↑(range #s) → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c - ↑x) x = (fun x ↦ c - ↑x) x₂ → x = x₂

Tactic:
mx

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ ↑(range #s)
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c - ↑x) x = (fun x ↦ c - ↑x) x₂ → x = x₂
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
⊢ x ∈ ↑(Ioc (c - ↑(#s)) c) → x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)

Tactic:
mx

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
⊢ x ∈ range #s → c + ↑x ∈ Ico c (c + ↑(#s))

Tactic:
mx

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c + ↑x ∈ Ico c (c + ↑(#s))
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
⊢ x ∈ ↑(range #s) → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c + ↑x) x = (fun x ↦ c + ↑x) x₂ → x = x₂

Tactic:
mx

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ ↑(range #s)
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c + ↑x) x = (fun x ↦ c + ↑x) x₂ → x = x₂
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
⊢ x ∈ ↑(Ico c (c + ↑(#s))) → x ∈ (fun x ↦ c + ↑x) '' ↑(range #s)

Tactic:
mx

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.GroupWithZero.Bounds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ BddAbove (g '' range f)

Tactic:
apply hg.map_bddAbove (by rintro x ⟨a, rfl⟩; exact hf0 a)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ (upperBounds (range f) ∩ {x | 0 ≤ x}).Nonempty
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ n • |a| = (n • 1) • |a|

Tactic:
smul_assoc,

Goal state after:
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ n • |a| = n • 1 • |a|
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc_of_not_isMax ha b

Goal state after:
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 α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ s - t = s + -t

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Goal state after:
case refine_1
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s - t).toProd.1 = (s + -t).toProd.1

case refine_2
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s - t).toProd.2 = (s + -t).toProd.2
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 α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ -(s + t) = -t + -s

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Goal state after:
case refine_1
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.1 = (-t + -s).toProd.1

case refine_2
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.2 = (-t + -s).toProd.2
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 α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : s + t = 0
⊢ -s = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h

Goal state after:
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s t : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
hab : a + b = 0
h : pure a + pure b = 0
⊢ -pure a = pure b
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
⊢ s / t = s * t⁻¹

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
⊢ (s / t).toProd.1 = (s * t⁻¹).toProd.1

case refine_2
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
⊢ (s / t).toProd.2 = (s * t⁻¹).toProd.2
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
⊢ (s * t)⁻¹.toProd.1 = (t⁻¹ * s⁻¹).toProd.1

case refine_2
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
⊢ (s * t)⁻¹.toProd.2 = (t⁻¹ * s⁻¹).toProd.2
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : x ≠ 0
⊢ 0 < x.orderTop ↔ 0 < x.order

Tactic:
by
  simp_all [orderTop_of_ne_zero hx, order_of_ne hx]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V✝ : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝³ x✝² : R
x✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ ((x✝³ * x✝²) • x✝¹).coeff x✝ = (x✝³ • x✝² • x✝¹).coeff x✝

Tactic:
simp [mul_smul]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
⊢ (∃ i,
        (∀ j < i,
            (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a)).coeff j =
              (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b)).coeff j) ∧
          (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a)).coeff i <
            (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b)).coeff i) ∨
      { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a =
        { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ↔
    (∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i) ∨ a = b

Tactic:
simp only [Function.Embedding.coeFn_mk, ofLex_toLex, EmbeddingLike.apply_eq_iff_eq]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
⊢ (∃ i,
        (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j) ∧
          (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex b)).coeff i) ∨
      embDomain f (ofLex a) = embDomain f (ofLex b) ↔
    (∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i) ∨ a = b
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
this : 0 < ↑(f (f.support.min' hsupport))
⊢ (seed.coeff (f.support.min' hsupport)) 0 < (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport))

Tactic:
by
    apply (seed.strictMono_coeff (f.support.min' hsupport))
    simpa using! this

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ x, ((single a) r).coeff x_1.1 * ((single b) s).coeff x_1.2 = 0

Tactic:
mem_antidiagonal

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ (x_1 : Γ × Γ),
    x_1.1 ∈ ((single a) r).support ∧ x_1.2 ∈ ((single b) s).support ∧ x_1.1 + x_1.2 = x →
      ((single a) r).coeff x_1.1 * ((single b) s).coeff x_1.2 = 0
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.inr
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
this : Units.mk0 x h_1 ∈ B.unitGroup
⊢ x ∈ B

Tactic:
exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)

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

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : A.valuation ↑x = 1
⊢ x ∈ B.unitGroup

Tactic:
apply_fun A.mapOfLE B h at hx

Goal state after:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : (A.mapOfLE B h) (A.valuation ↑x) = (A.mapOfLE B h) 1
⊢ x ∈ B.unitGroup
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
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ stdPart x + stdPart (-y) = stdPart x + -stdPart y

pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (-y)

Tactic:
stdPart_neg

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ stdPart x + -stdPart y = stdPart x + -stdPart y

K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (-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 y : K
hx : 0 < mk x
⊢ stdPart (-y) = -stdPart y

Tactic:
stdPart_neg

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
⊢ -stdPart y = -stdPart 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 : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ x < f r

Tactic:
by
  rw [← neg_lt_neg_iff, ← map_neg]
  apply lt_of_lt_stdPart <;> simpa

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝¹ : k + 1 < ((monomial n) x).coeffList.length
h₁✝ : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < n + 1
this : ((monomial n) x).natDegree.succ = n + 1
⊢ ((monomial n) x).coeffList.get ⟨k + 1, h₁✝¹⟩ = (x :: List.replicate n 0).get ⟨k + 1, h₁✝⟩

Tactic:
simpa [coeffList, withBotSucc_degree_eq_natDegree_add_one h]
      using Polynomial.coeff_monomial_of_ne _ (by lia)

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * (n + 1))

Tactic:
mul_add,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * n + m * 1)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:

Tactic:
_ ≤ 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.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 Df + i Dg = i b ^ N * (eval (i a * bf) (Polynomial.map i f) + eval (i a * bf) (Polynomial.map i g))

Tactic:
mul_add,

Goal state after:
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 Df + i Dg = i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)
Module: Mathlib.Algebra.Polynomial.Mirror

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

Tactic:
by_cases hp : p = 0
  · rw [hp, mirror_zero]
  nontriviality R
  rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
    tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]
  rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * 0).mirror = p.mirror * mirror 0

Tactic:
mul_zero,

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ mirror 0 = p.mirror * mirror 0