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

Goal state before:
pp: case e'_8
ι : 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
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ ↑s = ⇑(Equiv.symm σ) ⁻¹' ↑s

Tactic:
·

Goal state after:
case e'_8
ι : 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
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ ↑s = ⇑(Equiv.symm σ) ⁻¹' ↑s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case cons.inr.inl
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons y s hi)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : mk (a y) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a y)
hy : y ∈ Finset.cons y s hi
⊢ s.min' hs ≤ y

pp: case cons.inr.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ s.min' hs ≤ y

Tactic:
·

Goal state after:
case cons.inr.inl
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons y s hi)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : mk (a y) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a y)
hy : y ∈ Finset.cons y s hi
⊢ s.min' hs ≤ y
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case cons.inr.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ s.min' hs ≤ y

Tactic:
·

Goal state after:
case cons.inr.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ s.min' hs ≤ y
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case h
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ mk a⁻¹ < mk (b / a)

pp: case hneg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ a⁻¹ ≤ 1

Tactic:
·

Goal state after:
case h
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ mk a⁻¹ < mk (b / a)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case hneg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ a⁻¹ ≤ 1

Tactic:
·

Goal state after:
case hneg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ a⁻¹ ≤ 1
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case pos
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 : x ≤ 1
⊢ ∃ n, x ≤ y ^ n

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
⊢ ∃ n, x ≤ y ^ n

Tactic:
·

Goal state after:
case pos
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 : x ≤ 1
⊢ ∃ n, x ≤ y ^ n
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
⊢ ∃ n, x ≤ y ^ n

Tactic:
·

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
⊢ ∃ n, x ≤ y ^ n
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk a ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s

pp: case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk b ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s

Tactic:
·

Goal state after:
case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk a ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s
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
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk b ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s

Tactic:
·

Goal state after:
case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk b ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s
Module: Mathlib.Algebra.Order.Archimedean.Class

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

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:
·

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 ⊤
Module: Mathlib.Algebra.Order.Archimedean.Class

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

pp: 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

Tactic:
·

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
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
inst✝ : MulArchimedean M
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
⊢ mk a ha = B

Tactic:
induction B using ind with | mk b hb

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
inst✝ : MulArchimedean M
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ mk a ha = mk b hb
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case refine_1
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
⊢ (if h : a = 1 then ⊤ else ↑(f ⟨a, h⟩)) = if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)

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:
·

Goal state after:
case refine_1
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
⊢ (if h : a = 1 then ⊤ else ↑(f ⟨a, h⟩)) = if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : a ≤ 0
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

pp: case inr
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : a ≤ 0
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
·

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case pos
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : a = 1
hb : b = 1
⊢ ⊤ = ⊤

pp: case neg
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : a = 1
hb : ¬b = 1
⊢ ⊤ = ↑(f ⟨b, hb⟩)

pp: case pos
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : b = 1
⊢ ↑(f ⟨a, ha⟩) = ⊤

pp: case neg
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : ¬b = 1
⊢ ↑(f ⟨a, ha⟩) = ↑(f ⟨b, hb⟩)

Tactic:
·

Goal state after:
case pos
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : a = 1
hb : b = 1
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inl
K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a : K
⊢ ⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0

pp: case inr
K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a : K
n : ℕ
hn : n > 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Tactic:
·

Goal state after:
case inl
K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a : K
⊢ ⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0
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
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : a = 1
hb : ¬b = 1
⊢ ⊤ = ↑(f ⟨b, hb⟩)

pp: case pos
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : b = 1
⊢ ↑(f ⟨a, ha⟩) = ⊤

pp: case neg
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : ¬b = 1
⊢ ↑(f ⟨a, ha⟩) = ↑(f ⟨b, hb⟩)

Tactic:
·

Goal state after:
case neg
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : a = 1
hb : ¬b = 1
⊢ ⊤ = ↑(f ⟨b, hb⟩)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case pos
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : b = 1
⊢ ↑(f ⟨a, ha⟩) = ⊤

pp: case neg
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : ¬b = 1
⊢ ↑(f ⟨a, ha⟩) = ↑(f ⟨b, hb⟩)

Tactic:
·

Goal state after:
case pos
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : b = 1
⊢ ↑(f ⟨a, ha⟩) = ⊤
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
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : ¬b = 1
⊢ ↑(f ⟨a, ha⟩) = ↑(f ⟨b, hb⟩)

Tactic:
·

Goal state after:
case neg
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 ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : ¬b = 1
⊢ ↑(f ⟨a, ha⟩) = ↑(f ⟨b, hb⟩)
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inl
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉₊ < b * a

pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
·

Goal state after:
case inl
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉₊ < b * a
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
·

Goal state after:
case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a
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:
·

Goal state after:
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 ≠ ⊤
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inl
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉₊ / b⌉₊ ≤ b * (↑⌈(b - 1)⁻¹⌉₊ / b)

pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ ≤ b * a

Tactic:
·

Goal state after:
case inl
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉₊ / b⌉₊ ≤ b * (↑⌈(b - 1)⁻¹⌉₊ / b)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
hAB : mk a ha ≤ B
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ B

Tactic:
induction B using ind with | mk b hb

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
hAB : mk a ha ≤ mk b hb
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ (mk b hb)
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inl
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊

pp: case inl.hb
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ b ≠ 0

Tactic:
·

Goal state after:
case inl
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inl.hb
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ b ≠ 0

Tactic:
·

Goal state after:
case inl.hb
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ b ≠ 0
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case top
n : ℕ
hn₀ : ↑n ≠ 0
⊢ ↑n ≤ ⌈∞⌉ₑ ↔ ↑↑n - 1 < ∞

pp: case coe
n : ℕ
hn₀ : ↑n ≠ 0
x✝ : ℝ≥0
⊢ ↑n ≤ ⌈↑x✝⌉ₑ ↔ ↑↑n - 1 < ↑x✝

Tactic:
·

Goal state after:
case top
n : ℕ
hn₀ : ↑n ≠ 0
⊢ ↑n ≤ ⌈∞⌉ₑ ↔ ↑↑n - 1 < ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case coe
n : ℕ
hn₀ : ↑n ≠ 0
x✝ : ℝ≥0
⊢ ↑n ≤ ⌈↑x✝⌉ₑ ↔ ↑↑n - 1 < ↑x✝

Tactic:
·

Goal state after:
case coe
n : ℕ
hn₀ : ↑n ≠ 0
x✝ : ℝ≥0
⊢ ↑n ≤ ⌈↑x✝⌉ₑ ↔ ↑↑n - 1 < ↑x✝
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ ≤ b * a

Tactic:
·

Goal state after:
case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ ≤ b * a