mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ g * (b.1 / g) * (b.2 / g) = n

Tactic:
Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _),

Goal state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ b.1 * (b.2 / g) = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ 0 = g 0

Tactic:
ArithmeticFunction.map_zero

Goal state after:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ ↑(#s) ^ n * ((∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i) ≤ ↑(#s) ^ n * (↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i)

Tactic:
by
        gcongr _ * ?_
        exact ((monovaryOn_self ..).pow_left₀ hf _).sum_mul_sum_le_card_mul_sum

Goal state after:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rw [geom_sum_Ico' h'x.ne hmn]

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
⊢ (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
⊢ (f ^ k).IsMultiplicative

Tactic:
induction k

Goal state after:
case zero
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
⊢ (f ^ 0).IsMultiplicative

case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n✝ : ℕ
a✝ : (f ^ n✝).IsMultiplicative
⊢ (f ^ (n✝ + 1)).IsMultiplicative
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
h✝ : mk a < mk b
hneg : a ≤ 1
h : |a|ₘ⁻¹ < b ∧ b < |a|ₘ
⊢ a < b

Tactic:
mabs_eq_inv_self.mpr hneg,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h✝ : mk a < mk b
hneg : a ≤ 1
h : a⁻¹⁻¹ < b ∧ b < a⁻¹
⊢ a < b
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case neg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : 1 < x
hxy : mk x = mk y
left✝ : ∃ m, |y|ₘ ≤ |x|ₘ ^ m
m : ℕ
hm : |x|ₘ ≤ |y|ₘ ^ m
⊢ ∃ n, x ≤ y ^ n

Tactic:
rw [mabs_eq_self.mpr hx.le, mabs_eq_self.mpr hy.le] at hm

Goal state after:
case neg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : 1 < x
hxy : mk x = mk y
left✝ : ∃ m, |y|ₘ ≤ |x|ₘ ^ m
m : ℕ
hm : x ≤ y ^ m
⊢ ∃ n, x ≤ y ^ n
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
⊢ subgroup t ≤ subgroup s

Tactic:
obtain rfl | hs := eq_or_ne s ⊤

Goal state after:
case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
t : UpperSet (MulArchimedeanClass M)
hst : ⊤ ≤ t
⊢ subgroup t ≤ subgroup ⊤

case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
hs : s ≠ ⊤
⊢ subgroup t ≤ subgroup s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case refine_2
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
⊢ MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A ≠ ⊤

Tactic:
· induction A using MulArchimedeanClass.ind with | mk a
    simpa using MulArchimedeanClass.mk_eq_top_iff.not.mp hA

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
x✝ : ℝ≥0∞
⊢ ↑(⨆ i, f i) ≤ x✝ ↔ ⨆ i, ↑(f i) ≤ x✝

Tactic:
by simp [← le_floor]

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

Goal state before:
pp: case mk
G : Type u_1
inst✝ : CommGroup G
q : GroupCone G
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } = q

Tactic:
cases q

Goal state after:
case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ r ∩ s, x + #(s \ r) • (c - ↑(#s)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s))

Tactic:
card_sdiff_comm

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s))

s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ #s = #r
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ s ∩ r, x + #(r \ s) • (c + ↑(#s)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s))

Tactic:
card_sdiff_comm

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s))

s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ #r = #s
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]
  exact map_add_left_Ioc _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ h

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

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun x ↦ (ofLex x).1) '' Function.support fun g ↦ (x.coeff g.1).coeff g.2).IsPWO

pp: case refine_2
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ∀ (a : Γ), {y | toLex (a, y) ∈ Function.support fun g ↦ (x.coeff g.1).coeff g.2}.IsPWO

Tactic:
· refine Set.IsPWO.mono x.isPWO_support' ?_
      simp_rw [Set.image_subset_iff, support_subset_iff, Set.mem_preimage, Function.mem_support]
      exact fun _ ↦ ne_zero_of_coeff_ne_zero

Goal state after:
case refine_2
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ∀ (a : Γ), {y | toLex (a, y) ∈ Function.support fun g ↦ (x.coeff g.1).coeff g.2}.IsPWO
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
⊢ (embDomain f x).support ⊆ ⇑f '' x.support

Tactic:
intro g

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
g : Γ'
⊢ g ∈ (embDomain f x).support → g ∈ ⇑f '' x.support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex a).coeff i < (ofLex b).coeff i
⊢ a ≤ b ∨ b ≤ a

Tactic:
exact Or.inl (le_of_lt ⟨i, hji, hi⟩)

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

Goal state before:
pp: case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ∀ g' ∈ (ofLex x).support, i ≤ g'

Tactic:
intro g

Goal state after:
case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
g : Γ
⊢ g ∈ (ofLex x).support → i ≤ g
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
⊢ ∀ (a : G), 0 < a → 0 < (orderAddMonoidHom G) a

Tactic:
intro g

Goal state after:
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
g : G
⊢ 0 < g → 0 < (orderAddMonoidHom G) g
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
heq : (ofLex x).orderTop = (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
· -- when `x` and `y` have the same order, this reduces to
    -- `archimedeanClass_le_iff_of_orderTop_eq`
    simpa [heq] using archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex heq

Goal state after:
case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff
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
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
⊢ StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support

Tactic:
intro x hx y hy hxy

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ (fun i ↦ ArchimedeanClass.mk ↑(f i)) x < (fun i ↦ ArchimedeanClass.mk ↑(f i)) y
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝⁴ : Zero Γ
inst✝³ : PartialOrder Γ
inst✝² : Zero R
inst✝¹ : One R
inst✝ : NeZero 1
⊢ orderTop 1 = 0

Tactic:
by
  rw [← single_zero_one, orderTop_single one_ne_zero, WithTop.coe_eq_zero]

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

Goal state before:
pp: case mk
R : Type u_1
inst✝ : Ring R
q : RingCone R
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } = q

Tactic:
cases q

Goal state after:
case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
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 x < f y
⊢ f (x + y) = f y

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

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

Goal state before:
pp: case mk
R : Type u_1
inst✝ : CommRing R
q : RingPreordering R
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) q
⊢ { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ } = q

Tactic:
cases q

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✝¹, 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'✝ }
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.single.inl
α : 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 b✝ : α
h : x ≤ b✝
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.tail.inl
α : 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 b✝ c✝ : α
a✝ : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x b✝
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧
h : b✝ ≤ c✝
⊢ Quotient.lift f H ⟦b✝⟧ ≤ Quotient.lift f H ⟦c✝⟧

Tactic:
| inl h =>

Goal state after:
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
⊢ toLex { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ } =
    k • toLex { coeff := f.evalCoeff x, isPWO_support' := ⋯ }

Tactic:
rw [← toLex_smul, toLex.injective.eq_iff]

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
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ } = k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ }
Module: Mathlib.RingTheory.Valuation.ValuationSubring

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

Tactic:
rcases A.mem_or_inv_mem z with hh | hh

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

case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1
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 : x ∈ B.nonunits
h_1 : x ∉ A.nonunits
⊢ False

Tactic:
exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

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 : x ∈ B.principalUnitGroup
h_1 : x ∉ A.principalUnitGroup
⊢ False

Tactic:
exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝ : Add α
a b : WithTop α
c : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ untopD c (a + b) = untopD c a + untopD c b

Tactic:
lift a to α using ha

Goal state after:
α : Type u_1
inst✝ : Add α
b : WithTop α
c : α
hb : b ≠ ⊤
a : α
⊢ untopD c (↑a + b) = untopD c ↑a + untopD c b
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
h : a.untop₀ ≤ b.untop₀
⊢ a ≤ b

Tactic:
lift a to α using ha

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
b : WithTop α
a : α
h : (↑a).untop₀ ≤ b.untop₀
⊢ ↑a ≤ b
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a : WithTop α
b : α
h : a ≤ ↑b
ha : ¬a = ⊤
⊢ a.untop₀ ≤ (↑b).untop₀

Tactic:
lift a to α using ha

Goal state after:
case neg
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
b a : α
h : ↑a ≤ ↑b
⊢ (↑a).untop₀ ≤ (↑b).untop₀
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a.untop₀ ≤ b.untop₀ ↔ a ≤ b

Tactic:
lift a to α using ha

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ (↑a).untop₀ ≤ b.untop₀ ↔ ↑a ≤ b
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ (max a b).untop₀ = max a.untop₀ b.untop₀

Tactic:
lift a to α using ha

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ (max (↑a) b).untop₀ = max (↑a).untop₀ b.untop₀
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ (min a b).untop₀ = min a.untop₀ b.untop₀

Tactic:
lift a to α using ha

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ (min (↑a) b).untop₀ = min (↑a).untop₀ b.untop₀
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ stdPart x⁻¹ = 0⁻¹

Tactic:
stdPart_of_mk_ne_zero,

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ 0 = 0⁻¹

case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ mk x⁻¹ ≠ 0