awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ (↑⌈a⌉₊ : R) < a + 1

Tactic:
lt_ceil.1 <| (Nat.lt_succ_self _).trans_le (ceil_add_one ha).ge

Premises used: Eq.ge, Nat.lt_succ_self, Nat.ceil_add_one, LT.lt.trans_le, Iff.mp, Nat.lt_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
rw : a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉₊ : R) (↑⌈b⌉₊ : R)
⊢ ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊

Tactic:
rw [ceil_le, Nat.cast_add]

Premises used: Nat.cast_add, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h₁ : a ≤ (↑⌈a⌉₊ : R)
h₂ : b ≤ (↑⌈b⌉₊ : R)
⊢ a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉₊ : R) (↑⌈b⌉₊ : R)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
⊢ a ≤ (↑⌈a⌉₊ : R)

Tactic:
apply le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
⊢ b ≤ (↑⌈b⌉₊ : R)

Tactic:
apply le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
inl : ∀ (han : a ≤ (↑n : R)), ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
inr : ∀ (hna : (↑n : R) ≤ a), ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n

Tactic:
obtain han | hna := le_total a n

Premises used: le_total, Nat.cast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ (↑n : R)
inl : 0 = ⌈a⌉₊ - n
inl₁ : ⌈a⌉₊ - n = 0
inl₂ : ⌈a⌉₊ ≤ n
inl₃ inl₄ inl₅ inl₆ : a ≤ (↑n : R)
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n

Tactic:
rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]

Premises used: Iff.mpr, Nat.ceil_eq_zero, tsub_nonpos_of_le, tsub_eq_zero_iff_le, eq_comm, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
hna : (↑n : R) ≤ a
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n

Tactic:
eq_tsub_of_add_eq ?_

Premises used: eq_tsub_of_add_eq
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
hna : (↑n : R) ≤ a
inr : ⌈a - (↑n : R)⌉₊ + n = ⌈a⌉₊
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n

Tactic:
refine eq_tsub_of_add_eq ?_

Premises used: eq_tsub_of_add_eq
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
hna : (↑n : R) ≤ a
inr : 0 ≤ a - (↑n : R)
⊢ ⌈a - (↑n : R)⌉₊ + n = ⌈a⌉₊

Tactic:
rw [← ceil_add_natCast, tsub_add_cancel_of_le hna]

Premises used: tsub_add_cancel_of_le, Nat.ceil_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
hna : (↑n : R) ≤ a
⊢ 0 ≤ a - (↑n : R)

Tactic:
le_tsub_of_add_le_left ((add_zero _).trans_le hna)

Premises used: le_tsub_of_add_le_left, Eq.trans_le, add_zero
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
hna : (↑n : R) ≤ a
⊢ 0 ≤ a - (↑n : R)

Tactic:
exact le_tsub_of_add_le_left ((add_zero _).trans_le hna)

Premises used: le_tsub_of_add_le_left, Eq.trans_le, add_zero
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
⊢ ⌈a - 1⌉₊ = ⌈a⌉₊ - 1

Tactic:
simpa using ceil_sub_natCast a 1

Premises used: Nat.ceil_sub_natCast, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
inst_7 : n.AtLeastTwo
⊢ ⌈a - OfNat.ofNat n⌉₊ = ⌈a⌉₊ - OfNat.ofNat n

Tactic:
ceil_sub_natCast a n

Premises used: Nat.ceil_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
⊢ a - 1 < (↑⌊a⌋₊ : R)

Tactic:
sub_lt_iff_lt_add.2 <| lt_floor_add_one a

Premises used: Iff.mpr, sub_lt_iff_lt_add, Nat.lt_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - (↑⌊a⌋₊ : R)| ≤ 1

Tactic:
abs_le.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_le, And.intro
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
refine_1 : -1 ≤ a - (↑⌊a⌋₊ : R)
refine_2 : a - (↑⌊a⌋₊ : R) ≤ 1
⊢ |a - (↑⌊a⌋₊ : R)| ≤ 1

Tactic:
refine abs_le.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_le, And.intro
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - (↑⌊a⌋₊ : R)

Tactic:
simpa using (floor_le ha).trans (le_add_of_nonneg_right zero_le_one)

Premises used: zero_le_one, le_add_of_nonneg_right, Nat.floor_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a - (↑⌊a⌋₊ : R) ≤ 1

Tactic:
simpa [add_comm] using (lt_floor_add_one a).le

Premises used: LT.lt.le, add_comm, Nat.lt_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |(↑⌊a⌋₊ : R) - a| ≤ 1

Tactic:
abs_sub_comm a ⌊a⌋₊ ▸ abs_sub_floor_le ha

Premises used: Eq.rec, Nat.cast, Nat.abs_sub_floor_le, Nat.floor, abs_sub_comm
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - (↑⌈a⌉₊ : R)| ≤ 1

Tactic:
abs_le.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_le, And.intro
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
refine_1 : -1 ≤ a - (↑⌈a⌉₊ : R)
refine_2 : a - (↑⌈a⌉₊ : R) ≤ 1
⊢ |a - (↑⌈a⌉₊ : R)| ≤ 1

Tactic:
refine abs_le.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_le, And.intro
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - (↑⌈a⌉₊ : R)

Tactic:
simpa using (ceil_lt_add_one ha).le

Premises used: Nat.ceil_lt_add_one, LT.lt.le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a - (↑⌈a⌉₊ : R) ≤ 1

Tactic:
simpa using (le_ceil a).trans (le_add_of_nonneg_left zero_le_one)

Premises used: zero_le_one, Nat.le_ceil, LE.le.trans, le_add_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |(↑⌈a⌉₊ : R) - a| ≤ 1

Tactic:
abs_sub_comm a ⌈a⌉₊ ▸ abs_sub_ceil_le ha

Premises used: Eq.rec, Nat.abs_sub_ceil_le, Nat.cast, Nat.ceil, abs_sub_comm
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
⊢ 0 ≤ a ↔ 0 ≤ b

Tactic:
simpa only [cast_zero] using h 0

Premises used: Nat.cast_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
⊢ 0 ≤ a ↔ 0 ≤ b

Tactic:
have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
inl : ∀ (ha : a < 0), ⌊a⌋₊ = ⌊b⌋₊
inr : ∀ (ha : 0 ≤ a), ⌊a⌋₊ = ⌊b⌋₊
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
obtain ha | ha := lt_or_ge a 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
inl : 0 = ⌊b⌋₊
inl₁ inl₂ : Eq (α := ℕ) 0 0
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_ge <| h₀.not.mp ha.not_ge)]

Premises used: Iff.not, LT.lt.le, le_of_not_ge, Nat.floor_of_nonpos, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
(le_floor <| (h _).1 <| floor_le ha).antisymm (le_floor <| (h _).2 <| floor_le <| h₀.1 ha)

Premises used: Iff.mpr, LE.le.antisymm, Iff.mp, Nat.floor_le, Nat.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
exact (le_floor <| (h _).1 <| floor_le ha).antisymm (le_floor <| (h _).2 <| floor_le <| h₀.1 ha)

Premises used: Iff.mpr, LE.le.antisymm, Iff.mp, Nat.floor_le, Nat.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
h : ∀ (n : ℕ), a ≤ (↑n : R) ↔ b ≤ (↑n : S)
⊢ ⌈a⌉₊ = ⌈b⌉₊

Tactic:
(ceil_le.2 <| (h _).2 <| le_ceil _).antisymm <| ceil_le.2 <| (h _).1 <| le_ceil _

Premises used: Iff.mpr, LE.le.antisymm, Iff.mp, Nat.le_ceil, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
F : Type u_4
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
inst_8 : IsStrictOrderedRing R
inst_9 : IsStrictOrderedRing S
f : F
hf : StrictMono.{u_1, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℕ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
rw₁ rw₂ : (↑n : R) ≤ a ↔ (↑n : R) ≤ a
⊢ LE.le.{u_3} (α := S) ((↑n : S) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a

Tactic:
rw [← map_natCast f, hf.le_iff_le]

Premises used: map_natCast, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
F : Type u_4
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_1, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℕ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑n : R) : S) ↔ a ≤ (↑n : R)
rw₁ rw₂ : a ≤ (↑n : R) ↔ a ≤ (↑n : R)
⊢ LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((↑n : S) : S) ↔ a ≤ (↑n : R)

Tactic:
rw [← map_natCast f, hf.le_iff_le]

Premises used: map_natCast, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
⊢ Subsingleton.{u_3 + 1} (FloorSemiring R)

Tactic:
⟨fun H₁ H₂ => ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
refine : ∀ (H₁ H₂ : FloorSemiring R), H₁ = H₂
⊢ Subsingleton.{u_3 + 1} (FloorSemiring R)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
⊢ Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)

Tactic:
have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil.l_unique H₂.gc_ceil) fun n => rfl
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
h :
  ∀ (a : R),
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
      @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
⊢ Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)

Tactic:
ext a
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h :
  ∀ (h : a < 0),
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
      @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
h₁ :
  ∀ (h : 0 ≤ a),
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
      @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
⊢ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a

Tactic:
rcases lt_or_ge a 0 with h | h

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : a < 0
h₁ h₂ : a < 0
⊢ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a

Tactic:
rw [H₁.floor_of_neg, H₂.floor_of_neg]

Premises used: FloorSemiring.floor_of_neg
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : a < 0
⊢ a < 0

Tactic:
h
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : a < 0
⊢ a < 0

Tactic:
exact h
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : 0 ≤ a
⊢ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a

Tactic:
eq_of_forall_le_iff fun n => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : 0 ≤ a
h₁ :
  ∀ (n : ℕ),
    n ≤ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a ↔
      n ≤ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
⊢ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a

Tactic:
refine eq_of_forall_le_iff fun n => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : 0 ≤ a
n : ℕ
h₁ h₂ : 0 ≤ a
⊢ n ≤ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a ↔
    n ≤ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a

Tactic:
rw [H₁.gc_floor, H₂.gc_floor]

Premises used: FloorSemiring.gc_floor
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

Tactic:
h
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

Tactic:
exact h
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
⊢ Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)

Tactic:
have : H₁.floor = H₂.floor := by
    ext a
    rcases lt_or_ge a 0 with h | h
    · rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h
    · refine eq_of_forall_le_iff fun n => ?_
      rw [H₁.gc_floor, H₂.gc_floor] <;> exact h
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this_1 :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
mk :
  ∀ (floor ceil : R → ℕ) (floor_of_neg : ∀ {a : R} (ha : a < 0), floor a = 0)
    (gc_floor : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor a ↔ (↑n : R) ≤ a) (gc_ceil : GaloisConnection ceil Nat.cast)
    (this :
      Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
        (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _))
    (this :
      Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
        (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)),
    { floor := floor, ceil := ceil, floor_of_neg := @floor_of_neg, gc_floor := @gc_floor, gc_ceil := gc_ceil :
        FloorSemiring R } =
      H₂
⊢ H₁ = H₂

Tactic:
cases H₁
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₂ : FloorSemiring R
floor ceil : R → ℕ
floor_of_neg : ∀ {a : R} (ha : a < 0), floor a = 0
gc_floor : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor a ↔ (↑n : R) ≤ a
gc_ceil : GaloisConnection ceil Nat.cast
this_1 :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
mk :
  ∀ (floor_1 ceil_1 : R → ℕ) (floor_of_neg_1 : ∀ {a : R} (ha : a < 0), floor_1 a = 0)
    (gc_floor_1 : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor_1 a ↔ (↑n : R) ≤ a)
    (gc_ceil_1 : GaloisConnection ceil_1 Nat.cast)
    (this :
      Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
        (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _))
    (this :
      Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
        (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)),
    { floor := floor, ceil := ceil, floor_of_neg := @floor_of_neg, gc_floor := @gc_floor, gc_ceil := gc_ceil :
        FloorSemiring R } =
      { floor := floor_1, ceil := ceil_1, floor_of_neg := @floor_of_neg_1, gc_floor := @gc_floor_1,
        gc_ceil := gc_ceil_1 }
⊢ { floor := floor, ceil := ceil, floor_of_neg := @floor_of_neg, gc_floor := @gc_floor, gc_ceil := gc_ceil :
      FloorSemiring R } =
    H₂

Tactic:
cases H₂
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
floor ceil : R → ℕ
floor_of_neg : ∀ {a : R} (ha : a < 0), floor a = 0
gc_floor : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor a ↔ (↑n : R) ≤ a
gc_ceil : GaloisConnection ceil Nat.cast
floor_1 ceil_1 : R → ℕ
floor_of_neg_1 : ∀ {a : R} (ha : a < 0), floor_1 a = 0
gc_floor_1 : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor_1 a ↔ (↑n : R) ≤ a
gc_ceil_1 : GaloisConnection ceil_1 Nat.cast
this_1 :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
⊢ { floor := floor, ceil := ceil, floor_of_neg := @floor_of_neg, gc_floor := @gc_floor, gc_ceil := gc_ceil :
      FloorSemiring R } =
    { floor := floor_1, ceil := ceil_1, floor_of_neg := @floor_of_neg_1, gc_floor := @gc_floor_1, gc_ceil := gc_ceil_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
inl : ∀ (ha : a ≤ 1), |a ^ n|ₘ = |a|ₘ ^ n
inr : ∀ (ha : 1 ≤ a), |a ^ n|ₘ = |a|ₘ ^ n
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
obtain ha | ha := le_total a 1

Premises used: le_total, OfNat.ofNat