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

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β ((inducedOrderRingHom β γ).toRingHom a✝)

pp: case e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β ((inducedOrderRingHom β γ).toRingHom b✝)

Tactic:
<;>

Goal state after:
case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β ((inducedOrderRingHom β γ).toRingHom a✝)

case e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β ((inducedOrderRingHom β γ).toRingHom b✝)
Module: Mathlib.Algebra.Order.Archimedean.Real.Hom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedAddMonoid R
inst✝³ : Ring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedAddMonoid S
inst✝ : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ 0 ≤ f s * f s

Tactic:
apply mul_self_nonneg

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

pp: case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
⊢ (∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)) → f = g

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
⊢ f = g → ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)

case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
⊢ (∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)) → f = g
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

Tactic:
← Order.succ_eq_add_one,

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (succ i) = (partialSups f) i ⊔ disjointed f (succ i)
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

Tactic:
by_cases hi : IsMax i
  · have : i + 1 = i := by
      have h : i ≤ i + 1 := by
        rw [← Order.succ_eq_add_one]
        apply Order.le_succ
      exact le_antisymm (hi h) h
    simp only [this, left_eq_sup, ge_iff_le, disjointed, sdiff_le_iff]
    apply le_trans (le_partialSups _ _) le_sup_right
  · rw [← Order.succ_eq_add_one, disjointed_succ _ hi]
    simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
p : ℕ
a✝ : p ∈ x.primeFactors ∪ y.primeFactors
h : x.factorization p ≤ y.factorization p
⊢ f (p ^ (x.lcm y).factorization p) * f (p ^ (x.gcd y).factorization p) =
    f (p ^ x.factorization p) * f (p ^ y.factorization p)

pp: case neg.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
p : ℕ
a✝ : p ∈ x.primeFactors ∪ y.primeFactors
h : y.factorization p ≤ x.factorization p
⊢ f (p ^ (x.lcm y).factorization p) * f (p ^ (x.gcd y).factorization p) =
    f (p ^ x.factorization p) * f (p ^ y.factorization p)

Tactic:
<;>

Goal state after:
case neg.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
p : ℕ
a✝ : p ∈ x.primeFactors ∪ y.primeFactors
h : x.factorization p ≤ y.factorization p
⊢ f (p ^ (x.lcm y).factorization p) * f (p ^ (x.gcd y).factorization p) =
    f (p ^ x.factorization p) * f (p ^ y.factorization p)

case neg.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
p : ℕ
a✝ : p ∈ x.primeFactors ∪ y.primeFactors
h : y.factorization p ≤ x.factorization p
⊢ f (p ^ (x.lcm y).factorization p) * f (p ^ (x.gcd y).factorization p) =
    f (p ^ x.factorization p) * f (p ^ y.factorization p)
Module: Mathlib.Algebra.Order.Field.Pi

Goal state before:
pp: case intro.inl.inl
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : a < 0
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

pp: case intro.inl.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : 0 < a
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
<;>

Goal state after:
case intro.inl.inl
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : a < 0
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

case intro.inl.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : 0 < a
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Module: Mathlib.Algebra.Order.Field.Pi

Goal state before:
pp: case intro.inl.inl
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : a < 0
b : α
hb : 0 < b
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

pp: case intro.inl.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : 0 < a
b : α
hb : 0 < b
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
<;>

Goal state after:
case intro.inl.inl
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : a < 0
b : α
hb : 0 < b
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

case intro.inl.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : 0 < a
b : α
hb : 0 < b
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : m = 1
⊢ 1 (m * n) = 1 m * 1 n

pp: case neg
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : ¬m = 1
⊢ 1 (m * n) = 1 m * 1 n

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : m = 1
⊢ 1 (m * n) = 1 m * 1 n

case neg
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : ¬m = 1
⊢ 1 (m * n) = 1 m * 1 n
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
y : ι
hy : y ∈ ↑s
z : ι
hx : z ∈ ↑s
hgxy : (g ∘ ⇑σ) z < (g ∘ ⇑σ) y
hfxy : f y < f z
τ : Perm ι := Equiv.trans (Equiv.swap z y) σ
hz : z ∈ {x | (Equiv.swap z y) x ≠ x}
left✝ : z ≠ y
⊢ z ∈ ↑s

pp: case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
z : ι
hy : z ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) z
hfxy : f z < f x
τ : Perm ι := Equiv.trans (Equiv.swap x z) σ
hz : z ∈ {x_1 | (Equiv.swap x z) x_1 ≠ x_1}
left✝ : x ≠ z
⊢ z ∈ ↑s

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
y : ι
hy : y ∈ ↑s
z : ι
hx : z ∈ ↑s
hgxy : (g ∘ ⇑σ) z < (g ∘ ⇑σ) y
hfxy : f y < f z
τ : Perm ι := Equiv.trans (Equiv.swap z y) σ
hz : z ∈ {x | (Equiv.swap z y) x ≠ x}
left✝ : z ≠ y
⊢ z ∈ ↑s

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
z : ι
hy : z ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) z
hfxy : f z < f x
τ : Perm ι := Equiv.trans (Equiv.swap x z) σ
hz : z ∈ {x_1 | (Equiv.swap x z) x_1 ≠ x_1}
left✝ : x ≠ z
⊢ z ∈ ↑s
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Semiring α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : ExistsAddOfLE α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i, f i • g (σ i) = ∑ i, f i • g i ↔ Monovary f (g ∘ ⇑σ)

Tactic:
by
  simp [(hfg.monovaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Goal state after:
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Semiring α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : ExistsAddOfLE α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i, f (σ i) • g i = ∑ i, f i • g i ↔ Antivary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.antivaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

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

Goal state before:
pp: 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

Tactic:
obtain rfl | ht := eq_or_ne t ⊤

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

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

Goal state before:
pp: case zero
ι : Type u_1
α : Type u_2
β : Type u_3
⊢ (0 + 0 - 1) / 0 = 0

pp: case succ
ι : Type u_1
α : Type u_2
β : Type u_3
n✝ : ℕ
⊢ (0 + (n✝ + 1) - 1) / (n✝ + 1) = 0

Tactic:
<;>

Goal state after:
case zero
ι : Type u_1
α : Type u_2
β : Type u_3
⊢ (0 + 0 - 1) / 0 = 0

case succ
ι : Type u_1
α : Type u_2
β : Type u_3
n✝ : ℕ
⊢ (0 + (n✝ + 1) - 1) / (n✝ + 1) = 0
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top
⊢ ⌊∞⌋ₑ = ⊤ ↔ ∞ = ∞

pp: case coe
x✝ : ℝ≥0
⊢ ⌊↑x✝⌋ₑ = ⊤ ↔ ↑x✝ = ∞

Tactic:
<;>

Goal state after:
case top
⊢ ⌊∞⌋ₑ = ⊤ ↔ ∞ = ∞

case coe
x✝ : ℝ≥0
⊢ ⌊↑x✝⌋ₑ = ⊤ ↔ ↑x✝ = ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top
⊢ ⌈∞⌉ₑ = ⊤ ↔ ∞ = ∞

pp: case coe
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ = ⊤ ↔ ↑x✝ = ∞

Tactic:
<;>

Goal state after:
case top
⊢ ⌈∞⌉ₑ = ⊤ ↔ ∞ = ∞

case coe
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ = ⊤ ↔ ↑x✝ = ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top
⊢ ⌊∞⌋ₑ < ⊤ ↔ ∞ < ∞

pp: case coe
x✝ : ℝ≥0
⊢ ⌊↑x✝⌋ₑ < ⊤ ↔ ↑x✝ < ∞

Tactic:
<;>

Goal state after:
case top
⊢ ⌊∞⌋ₑ < ⊤ ↔ ∞ < ∞

case coe
x✝ : ℝ≥0
⊢ ⌊↑x✝⌋ₑ < ⊤ ↔ ↑x✝ < ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top
⊢ ⌈∞⌉ₑ < ⊤ ↔ ∞ < ∞

pp: case coe
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ < ⊤ ↔ ↑x✝ < ∞

Tactic:
<;>

Goal state after:
case top
⊢ ⌈∞⌉ₑ < ⊤ ↔ ∞ < ∞

case coe
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ < ⊤ ↔ ↑x✝ < ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top
n : ℕ∞
⊢ n ≤ ⌊∞⌋ₑ ↔ ↑n ≤ ∞

pp: case coe
n : ℕ∞
x✝ : ℝ≥0
⊢ n ≤ ⌊↑x✝⌋ₑ ↔ ↑n ≤ ↑x✝

Tactic:
<;>

Goal state after:
case top
n : ℕ∞
⊢ n ≤ ⌊∞⌋ₑ ↔ ↑n ≤ ∞

case coe
n : ℕ∞
x✝ : ℝ≥0
⊢ n ≤ ⌊↑x✝⌋ₑ ↔ ↑n ≤ ↑x✝
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top.top
⊢ ⊤ ≤ ⌊∞⌋ₑ ↔ ↑⊤ ≤ ∞

pp: case top.coe
a✝ : ℕ
⊢ ↑a✝ ≤ ⌊∞⌋ₑ ↔ ↑↑a✝ ≤ ∞

pp: case coe.top
x✝ : ℝ≥0
⊢ ⊤ ≤ ⌊↑x✝⌋ₑ ↔ ↑⊤ ≤ ↑x✝

pp: case coe.coe
x✝ : ℝ≥0
a✝ : ℕ
⊢ ↑a✝ ≤ ⌊↑x✝⌋ₑ ↔ ↑↑a✝ ≤ ↑x✝

Tactic:
<;>

Goal state after:
case top.top
⊢ ⊤ ≤ ⌊∞⌋ₑ ↔ ↑⊤ ≤ ∞

case top.coe
a✝ : ℕ
⊢ ↑a✝ ≤ ⌊∞⌋ₑ ↔ ↑↑a✝ ≤ ∞

case coe.top
x✝ : ℝ≥0
⊢ ⊤ ≤ ⌊↑x✝⌋ₑ ↔ ↑⊤ ≤ ↑x✝

case coe.coe
x✝ : ℝ≥0
a✝ : ℕ
⊢ ↑a✝ ≤ ⌊↑x✝⌋ₑ ↔ ↑↑a✝ ≤ ↑x✝
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top
n : ℕ∞
⊢ ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ ↑n

pp: case coe
n : ℕ∞
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ ≤ n ↔ ↑x✝ ≤ ↑n

Tactic:
<;>

Goal state after:
case top
n : ℕ∞
⊢ ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ ↑n

case coe
n : ℕ∞
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ ≤ n ↔ ↑x✝ ≤ ↑n
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top.top
⊢ ⌈∞⌉ₑ ≤ ⊤ ↔ ∞ ≤ ↑⊤

pp: case top.coe
a✝ : ℕ
⊢ ⌈∞⌉ₑ ≤ ↑a✝ ↔ ∞ ≤ ↑↑a✝

pp: case coe.top
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ ≤ ⊤ ↔ ↑x✝ ≤ ↑⊤

pp: case coe.coe
x✝ : ℝ≥0
a✝ : ℕ
⊢ ⌈↑x✝⌉ₑ ≤ ↑a✝ ↔ ↑x✝ ≤ ↑↑a✝

Tactic:
<;>

Goal state after:
case top.top
⊢ ⌈∞⌉ₑ ≤ ⊤ ↔ ∞ ≤ ↑⊤

case top.coe
a✝ : ℕ
⊢ ⌈∞⌉ₑ ≤ ↑a✝ ↔ ∞ ≤ ↑↑a✝

case coe.top
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ ≤ ⊤ ↔ ↑x✝ ≤ ↑⊤

case coe.coe
x✝ : ℝ≥0
a✝ : ℕ
⊢ ⌈↑x✝⌉ₑ ≤ ↑a✝ ↔ ↑x✝ ≤ ↑↑a✝
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case refine_1
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 0 < 2⁻¹

pp: case refine_2
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 2⁻¹ < 1

pp: case refine_3
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ ↑⌈2⁻¹ / (1 - 2⁻¹)⌉₊ ≤ a

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 0 < 2⁻¹

case refine_2
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 2⁻¹ < 1

case refine_3
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ ↑⌈2⁻¹ / (1 - 2⁻¹)⌉₊ ≤ a
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : c < a * b
a' : α
hc' : c / b < a'
ha' : a' < a
⊢ ∃ a', a' < a ∧ c < a' * b

Tactic:
exact ⟨a', ha', div_lt_iff_lt_mul.1 hc'⟩

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀
⊢ 0 ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

pp: case inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀
x : M₀ˣ
⊢ ↑x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
<;>

Goal state after:
case inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀
⊢ 0 ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

case inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀
x : M₀ˣ
⊢ ↑x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

pp: case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

pp: case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : M₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

pp: case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
<;>

Goal state after:
case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : M₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
⊢ 0 ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

pp: case inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
x : N₀ˣ
⊢ ↑x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
<;>

Goal state after:
case inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
⊢ 0 ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

case inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
x : N₀ˣ
⊢ ↑x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y