awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)
have rw : 0 ≤ b - a - (↑⌊(b - a) / p⌋ : α) * p ∧ b - a - (↑⌊(b - a) / p⌋ : α) * p < p
Tactic: rw [Set.mem_Ico, zsmul_eq_mul, ← sub_nonneg, add_comm, sub_right_comm, ← sub_lt_iff_lt_add,
    sub_right_comm _ _ a]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv (p := p) hp a b = -⌊(a + p - b) / p⌋
have refine : b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)
Tactic: refine toIocDiv_eq_of_sub_zsmul_mem_Ioc hp ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)
have rw : a < b + (↑⌊(a + p - b) / p⌋ : α) * p ∧ 0 ≤ a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p
Tactic: rw [Set.mem_Ioc, zsmul_eq_mul, Int.cast_neg, neg_mul, sub_neg_eq_add, ← sub_nonneg,
    sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + (↑⌊(a + p - b) / p⌋ : α) * p ∧ 0 ≤ a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p
have refine : a < b + (↑⌊(a + p - b) / p⌋ : α) * p
Tactic: refine ⟨?_, Int.sub_floor_div_mul_nonneg _ hp⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + (↑⌊(a + p - b) / p⌋ : α) * p
have rw : a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p < p
Tactic: rw [← add_lt_add_iff_right p, add_assoc, add_comm b, ← sub_lt_iff_lt_add, add_comm (_ * _), ←
    sub_lt_iff_lt_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod (p := p) hp a b = a + Int.fract ((b - a) / p) * p
have rw : b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - (↑⌊(b - a) / p⌋ : α)) * p
Tactic: rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - (↑⌊(b - a) / p⌋ : α)) * p
have simp : b - (↑⌊(b - a) / p⌋ : α) * p = a + (b - a - (↑⌊(b - a) / p⌋ : α) * p)
Tactic: simp [field, -Int.self_sub_floor]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocMod (p := p) hp a b = a + p - Int.fract ((a + p - b) / p) * p
have rw : b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - (↑⌊(a + p - b) / p⌋ : α)) * p
Tactic: rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - (↑⌊(a + p - b) / p⌋ : α)) * p
have simp : b + (↑⌊(a + p - b) / p⌋ : α) * p = a + p - (a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p)
Tactic: simp [field, -Int.self_sub_floor]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ioc (a + n • p) (a + (n + 1) • p)) univ
have refine : ∀ (b : α), ∃ (i : ℤ), b ∈ Ioc (a + i • p) (a + (i + 1) • p)
Tactic: refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ (i : ℤ), b ∈ Ioc (a + i • p) (a + (i + 1) • p)
have hl : a < b - toIocDiv hp a b • p
Tactic: rcases sub_toIocDiv_zsmul_mem_Ioc hp a b with ⟨hl, hr⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
⊢ ∃ (i : ℤ), b ∈ Ioc (a + i • p) (a + (i + 1) • p)
have hr : b - toIocDiv hp a b • p ≤ a + p
Tactic: rcases sub_toIocDiv_zsmul_mem_Ioc hp a b with ⟨hl, hr⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ ∃ (i : ℤ), b ∈ Ioc (a + i • p) (a + (i + 1) • p)
have refine : b ≤ a + (toIocDiv hp a b + 1) • p
Tactic: refine ⟨toIocDiv hp a b, ⟨lt_sub_iff_add_lt.mp hl, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b + 1) • p
have rw : b ≤ a + toIocDiv hp a b • p + p
Tactic: rw [add_smul, one_smul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + toIocDiv hp a b • p + p
have h : a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p
Tactic: convert! sub_le_iff_le_add.mp hr using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ico (a + n • p) (a + (n + 1) • p)) univ
have refine : ∀ (b : α), ∃ (i : ℤ), b ∈ Ico (a + i • p) (a + (i + 1) • p)
Tactic: refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ (i : ℤ), b ∈ Ico (a + i • p) (a + (i + 1) • p)
have hl : a ≤ b - toIcoDiv hp a b • p
Tactic: rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
⊢ ∃ (i : ℤ), b ∈ Ico (a + i • p) (a + (i + 1) • p)
have hr : b - toIcoDiv hp a b • p < a + p
Tactic: rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ ∃ (i : ℤ), b ∈ Ico (a + i • p) (a + (i + 1) • p)
have refine : b < a + (toIcoDiv hp a b + 1) • p
Tactic: refine ⟨toIcoDiv hp a b, ⟨le_sub_iff_add_le.mp hl, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b + 1) • p
have rw : b < a + toIcoDiv hp a b • p + p
Tactic: rw [add_smul, one_smul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + toIcoDiv hp a b • p + p
have h : a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p
Tactic: convert! sub_lt_iff_lt_add.mp hr using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
hs : s.OrdConnected
⊢ (a • s).OrdConnected
have rw : (a • (↑(upperClosure s) : Set α) ∩ a • (↑(lowerClosure s) : Set α)).OrdConnected
Tactic: rw [← hs.upperClosure_inter_lowerClosure, smul_set_inter]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet (s * t)
have rw : IsUpperSet.{u_1} (α := α) (⋃ a ∈ s, a • t)
Tactic: rw [← smul_eq_mul, ← Set.iUnion_smul_set]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t)
have rw : IsUpperSet (t * s)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsLowerSet (s / t)
have rw : IsLowerSet (s * t⁻¹)
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s / t)
have rw : IsUpperSet (s * t⁻¹)
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : UpperSet α
⊢ Set.Ici 1 * (↑s : Set α) ⊆ (↑s : Set α)
have rw : ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Ici 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)
Tactic: rw [← smul_eq_mul, ← Set.iUnion_smul_set]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : UpperSet α
⊢ s * 1 = s
have rw : 1 * s = s
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : LowerSet α
⊢ Set.Iic 1 * (↑s : Set α) ⊆ (↑s : Set α)
have rw : ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Iic 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)
Tactic: rw [← smul_eq_mul, ← Set.iUnion_smul_set]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : LowerSet α
⊢ s * 1 = s
have rw : 1 * s = s
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ s * (↑(upperClosure t) : Set α) = (↑(upperClosure (s * t)) : Set α)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋃ a ∈ s, a • (↑(upperClosure t) : Set α))
  (⋃ i ∈ s, (↑(HSMul.hSMul (β := UpperSet α) i (upperClosure t)) : Set α))
Tactic: simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul,
    UpperSet.coe_iInf₂]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ s * (↑(lowerClosure t) : Set α) = (↑(lowerClosure (s * t)) : Set α)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋃ a ∈ s, a • (↑(lowerClosure t) : Set α))
  (⋃ i ∈ s, (↑(HSMul.hSMul (β := LowerSet α) i (lowerClosure t)) : Set α))
Tactic: simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul,
    LowerSet.coe_iSup₂]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ (↑(upperClosure s) : Set α) * t = (↑(upperClosure (s * t)) : Set α)
have simp_rw : t * (↑(upperClosure s) : Set α) = (↑(upperClosure (t * s)) : Set α)
Tactic: simp_rw [mul_comm _ t]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ (↑(lowerClosure s) : Set α) * t = (↑(lowerClosure (s * t)) : Set α)
have simp_rw : t * (↑(lowerClosure s) : Set α) = (↑(lowerClosure (t * s)) : Set α)
Tactic: simp_rw [mul_comm _ t]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ (↑(upperClosure (s * t)) : Set α) = (↑(HMul.hMul (α := UpperSet α) (upperClosure s) (upperClosure t)) : Set α)
have rw : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure s) : Set α) * (↑(upperClosure t) : Set α)
Tactic: rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure s) : Set α) * (↑(upperClosure t) : Set α)
⊢ (↑(upperClosure (s * t)) : Set α) = (↑(HMul.hMul (α := UpperSet α) (upperClosure s) (upperClosure t)) : Set α)
have rw₁ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure ((↑(upperClosure s) : Set α) * t)) : Set α)
Tactic: rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure s) : Set α) * (↑(upperClosure t) : Set α)
rw₁ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure ((↑(upperClosure s) : Set α) * t)) : Set α)
⊢ (↑(upperClosure (s * t)) : Set α) = (↑(HMul.hMul (α := UpperSet α) (upperClosure s) (upperClosure t)) : Set α)
have rw₂ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure (↑(upperClosure (s * t)) : Set α)) : Set α)
Tactic: rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure s) : Set α) * (↑(upperClosure t) : Set α)
rw₁ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure ((↑(upperClosure s) : Set α) * t)) : Set α)
rw₂ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure (↑(upperClosure (s * t)) : Set α)) : Set α)
⊢ (↑(upperClosure (s * t)) : Set α) = (↑(HMul.hMul (α := UpperSet α) (upperClosure s) (upperClosure t)) : Set α)
have rw₃ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure (s * t)) : Set α)
Tactic: rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ (↑(lowerClosure (s * t)) : Set α) = (↑(HMul.hMul (α := LowerSet α) (lowerClosure s) (lowerClosure t)) : Set α)
have rw : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure s) : Set α) * (↑(lowerClosure t) : Set α)
Tactic: rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure s) : Set α) * (↑(lowerClosure t) : Set α)
⊢ (↑(lowerClosure (s * t)) : Set α) = (↑(HMul.hMul (α := LowerSet α) (lowerClosure s) (lowerClosure t)) : Set α)
have rw₁ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure ((↑(lowerClosure s) : Set α) * t)) : Set α)
Tactic: rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure s) : Set α) * (↑(lowerClosure t) : Set α)
rw₁ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure ((↑(lowerClosure s) : Set α) * t)) : Set α)
⊢ (↑(lowerClosure (s * t)) : Set α) = (↑(HMul.hMul (α := LowerSet α) (lowerClosure s) (lowerClosure t)) : Set α)
have rw₂ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure (↑(lowerClosure (s * t)) : Set α)) : Set α)
Tactic: rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure s) : Set α) * (↑(lowerClosure t) : Set α)
rw₁ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure ((↑(lowerClosure s) : Set α) * t)) : Set α)
rw₂ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure (↑(lowerClosure (s * t)) : Set α)) : Set α)
⊢ (↑(lowerClosure (s * t)) : Set α) = (↑(HMul.hMul (α := LowerSet α) (lowerClosure s) (lowerClosure t)) : Set α)
have rw₃ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure (s * t)) : Set α)
Tactic: rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : Zero α
a : WithTop α
ha : a ≠ ⊤
⊢ (↑a.untop₀ : WithTop α) = a
have obtain : ∀ (b : α) (hb : (↑b : WithTop α) = a), (↑a.untop₀ : WithTop α) = a
Tactic: obtain ⟨b, hb⟩ := WithTop.ne_top_iff_exists.1 ha
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : Add α
a b : WithTop α
c : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ untopD c (a + b) = untopD c a + untopD c b
have lift : ∀ (a : α), untopD c ((↑a : WithTop α) + b) = untopD c (↑a : WithTop α) + untopD c b
Tactic: lift a to α using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : Add α
b : WithTop α
c : α
hb : b ≠ ⊤
a : α
⊢ untopD c ((↑a : WithTop α) + b) = untopD c (↑a : WithTop α) + untopD c b
have lift : ∀ (b : α), untopD c ((↑a : WithTop α) + (↑b : WithTop α)) = untopD c (↑a : WithTop α) + untopD c (↑b : WithTop α)
Tactic: lift b to α using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
⊢ LE.le.{u_1} (α := α) 0 (untop₀ ⊤) ↔ LE.le.{u_1} (α := WithTop α) 0 ⊤
have top : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
top : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
⊢ LE.le.{u_1} (α := α) 0 (untop₀ ⊤) ↔ LE.le.{u_1} (α := WithTop α) 0 ⊤
have top₁ : LE.le.{u_1} (α := WithTop α) 0 ⊤ → LE.le.{u_1} (α := α) 0 (untop₀ ⊤)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
top : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
top₁ : LE.le.{u_1} (α := WithTop α) 0 ⊤ → LE.le.{u_1} (α := α) 0 (untop₀ ⊤)
top₂ top₃ top₄ : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
⊢ LE.le.{u_1} (α := α) 0 (untop₀ ⊤) ↔ LE.le.{u_1} (α := WithTop α) 0 ⊤
have top₅ : LE.le.{u_1} (α := WithTop α) 0 ⊤ → LE.le.{u_1} (α := α) 0 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
⊢ 0 ≤ a.untop₀ ↔ 0 ≤ a
have top : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) ↔ LE.le.{u_1} (α := WithTop α) 0 ⊤
Tactic: cases a with
  | top => tauto
  | coe a => simp
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
top : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) ↔ LE.le.{u_1} (α := WithTop α) 0 ⊤
⊢ 0 ≤ a.untop₀ ↔ 0 ≤ a
have coe : ∀ (a : α), 0 ≤ (↑a : WithTop α).untop₀ ↔ 0 ≤ (↑a : WithTop α)
Tactic: cases a with
  | top => tauto
  | coe a => simp
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
h : a.untop₀ ≤ b.untop₀
⊢ a ≤ b
have lift : ∀ (a : α) (h : (↑a : WithTop α).untop₀ ≤ b.untop₀), (↑a : WithTop α) ≤ b
Tactic: lift a to α using ha
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
a : α
h : (↑a : WithTop α).untop₀ ≤ b.untop₀
⊢ (↑a : WithTop α) ≤ b
have pos : ∀ (hb : b = ⊤), (↑a : WithTop α) ≤ b
Tactic: by_cases hb : b = ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
a : α
h : (↑a : WithTop α).untop₀ ≤ b.untop₀
pos : ∀ (hb : b = ⊤), (↑a : WithTop α) ≤ b
⊢ (↑a : WithTop α) ≤ b
have neg : ∀ (hb : ¬b = ⊤), (↑a : WithTop α) ≤ b
Tactic: by_cases hb : b = ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
a : α
h : (↑a : WithTop α).untop₀ ≤ b.untop₀
hb : ¬b = ⊤
⊢ (↑a : WithTop α) ≤ b
have neg : ∀ (b : α) (h : (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀), (↑a : WithTop α) ≤ (↑b : WithTop α)
Tactic: lift b to α using hb
Cleared hypotheses: b, h, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
hb : b ≠ ⊤
h : a ≤ b
⊢ a.untop₀ ≤ b.untop₀
have lift : ∀ (b : α) (h : a ≤ (↑b : WithTop α)), a.untop₀ ≤ (↑b : WithTop α).untop₀
Tactic: lift b to α using hb
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
b : α
h : a ≤ (↑b : WithTop α)
⊢ a.untop₀ ≤ (↑b : WithTop α).untop₀
have pos : ∀ (ha : a = ⊤), a.untop₀ ≤ (↑b : WithTop α).untop₀
Tactic: by_cases ha : a = ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
b : α
h : a ≤ (↑b : WithTop α)
pos : ∀ (ha : a = ⊤), a.untop₀ ≤ (↑b : WithTop α).untop₀
⊢ a.untop₀ ≤ (↑b : WithTop α).untop₀
have neg : ∀ (ha : ¬a = ⊤), a.untop₀ ≤ (↑b : WithTop α).untop₀
Tactic: by_cases ha : a = ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
b : α
h : a ≤ (↑b : WithTop α)
ha : ¬a = ⊤
⊢ a.untop₀ ≤ (↑b : WithTop α).untop₀
have neg : ∀ (a : α) (h : (↑a : WithTop α) ≤ (↑b : WithTop α)), (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀
Tactic: lift a to α using ha
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a.untop₀ ≤ b.untop₀ ↔ a ≤ b
have lift : ∀ (a : α), (↑a : WithTop α).untop₀ ≤ b.untop₀ ↔ (↑a : WithTop α) ≤ b
Tactic: lift a to α using ha
Cleared hypotheses: a, ha