awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Bounds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty
have right : Membership.mem (γ := Set β) {x : β | 0 ≤ x} b
Tactic: use b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Bounds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ Membership.mem (γ := Set β) {x : β | 0 ≤ x} b
have hb₁ : ∀ (a : α), f a ≤ b
Tactic: simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab : a ≤ b
c : α
⊢ a * c ≤ b * c
have inl : a * 0 ≤ b * 0
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab : a ≤ b
c : α
inl : a * 0 ≤ b * 0
⊢ a * c ≤ b * c
have inr : ∀ (hc : c ≠ 0), a * c ≤ b * c
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab : a ≤ b
c : α
hc : c ≠ 0
⊢ a * c ≤ b * c
have inr : ∀ (hab : a ≤ a), a * c ≤ a * c
Tactic: obtain rfl | hab := hab.eq_or_lt
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab : a ≤ b
c : α
hc : c ≠ 0
inr : ∀ (hab : a ≤ a), a * c ≤ a * c
⊢ a * c ≤ b * c
have inr₁ : ∀ (hab : a < b), a * c ≤ b * c
Tactic: obtain rfl | hab := hab.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : Additive αᵒᵈ
⊢ ⊤ + a = ⊤
have hab : Eq (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) (⊤ + a) : αᵒᵈ) : α)
  ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) ⊤ : αᵒᵈ) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : (Additive α)ᵒᵈ
⊢ ⊤ + a = ⊤
have h : Eq (α := α)
  ((Additive.toMul : (a : Additive α) → α)
      ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (⊤ + a) : Additive α) :
    α)
  ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : (Additive α)ᵒᵈ
⊢ Eq (α := α)
    ((Additive.toMul : (a : Additive α) → α)
        ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (⊤ + a) : Additive α) :
      α)
    ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) :
      α)
have h : HMul.hMul (α := α) (β := α) (⊥ : α)
    ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) a : Additive α) :
      α) =
  ⊥
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → IsAddLeftRegular x
have simp : ∀ (a : α), ¬a = ⊥ → IsRegular a
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst_1 : NoZeroDivisors α
hn : n ≠ 0
⊢ 0 < a ^ n ↔ 0 < a
have simp_rw : a ^ n ≠ 0 ↔ a ≠ 0
Tactic: simp_rw [pos_iff_ne_zero, pow_ne_zero_iff hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ a * c⁻¹ < b
have contrapose! : ∀ (h : b ≤ a * c⁻¹), b * c ≤ a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ b⁻¹ * a < c
have rw : ∀ (h : a < c * b), a * b⁻¹ < c
Tactic: rw [mul_comm] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
⊢ b < d
have ha : a ≠ 0
Tactic: have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d
have hh₁ : a⁻¹ ≤ c⁻¹
Tactic: rw [← inv_le_inv₀ ha.pos hc] at hh
Cleared hypotheses: hh, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ Eq.{u_1 + 1} (α := Additive αᵒᵈ) (-⊤) ⊤
have hab : Eq.{u_1 + 1} (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) (-⊤) : αᵒᵈ) : α)
  ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) ⊤ : αᵒᵈ) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ Eq.{u_1 + 1} (α := (Additive α)ᵒᵈ) (-⊤) ⊤
have h : Eq.{u_1 + 1} (α := α)
  ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (-⊤) : Additive α) :
    α)
  ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ Eq.{u_1 + 1} (α := α)
    ((Additive.toMul : (a : Additive α) → α)
        ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (-⊤) : Additive α) :
      α)
    ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) :
      α)
have h : Eq.{u_1 + 1} (α := α) ⊥⁻¹ ⊥
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → x + -x = 0
have simp : ∀ (a : α),
  ¬a = ⊥ →
    HAdd.hAdd (α := (Additive α)ᵒᵈ) (β := (Additive α)ᵒᵈ)
        ((OrderDual.toDual : (a : Additive α) → (Additive α)ᵒᵈ)
            ((Additive.ofMul : (a : α) → Additive α) a : Additive α) :
          (Additive α)ᵒᵈ)
        (-(OrderDual.toDual : (a : Additive α) → (Additive α)ᵒᵈ)
              ((Additive.ofMul : (a : α) → Additive α) a : Additive α) :
          (Additive α)ᵒᵈ) =
      0
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
⊢ DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
have refine_1 : ∀ (H : DenselyOrdered α), Nontrivial.{u_1} αˣ
Tactic: refine ⟨fun H ↦ ⟨?_, ?_⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
refine_1 : ∀ (H : DenselyOrdered α), Nontrivial.{u_1} αˣ
⊢ DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
have refine_2 : ∀ (H : DenselyOrdered α), DenselyOrdered.{u_1} αˣ
Tactic: refine ⟨fun H ↦ ⟨?_, ?_⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
refine_1 : ∀ (H : DenselyOrdered α), Nontrivial.{u_1} αˣ
refine_2 : ∀ (H : DenselyOrdered α), DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
have refine_3 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ →
  ∀ (H₁ : Nontrivial.{u_1} αˣ) (H₂ : DenselyOrdered.{u_1} αˣ), DenselyOrdered α
Tactic: refine ⟨fun H ↦ ⟨?_, ?_⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ Nontrivial.{u_1} αˣ
have refine_1 : ∀ (x : α) (hx : 0 < x) (hx' : x < 1), Nontrivial.{u_1} αˣ
Tactic: obtain ⟨x, hx, hx'⟩ := exists_between (zero_lt_one' α)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ DenselyOrdered.{u_1} αˣ
have refine_2 : ∀ (x y : αˣ) (h : x < y), ∃ (a : αˣ), x < a ∧ a < y
Tactic: refine ⟨fun x y h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x y : αˣ
h : x < y
⊢ ∃ (a : αˣ), x < a ∧ a < y
have refine_2 : ∀ (z : α) (hz : (↑x : α) < z ∧ z < (↑y : α)), ∃ (a : αˣ), x < a ∧ a < y
Tactic: obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered α
have refine_3 : ∀ (x y : α) (h : x < y), ∃ (a : α), x < a ∧ a < y
Tactic: refine ⟨fun x y h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x y : α
h : x < y
⊢ ∃ (a : α), x < a ∧ a < y
have refine_3 : ∀ (y : αˣ) (h : x < (↑y : α)), ∃ (a : α), x < a ∧ a < (↑y : α)
Tactic: lift y to αˣ using (ne_zero_of_lt h).isUnit
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x : α
y : αˣ
h : x < (↑y : α)
⊢ ∃ (a : α), x < a ∧ a < (↑y : α)
have refine_3 : ∀ (h : 0 < (↑y : α)), ∃ (a : α), 0 < a ∧ a < (↑y : α)
Tactic: obtain rfl | hx := eq_zero_or_pos x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x : α
y : αˣ
h : x < (↑y : α)
refine_3 : ∀ (h : 0 < (↑y : α)), ∃ (a : α), 0 < a ∧ a < (↑y : α)
⊢ ∃ (a : α), x < a ∧ a < (↑y : α)
have refine_3₁ : ∀ (hx : 0 < x), ∃ (a : α), x < a ∧ a < (↑y : α)
Tactic: obtain rfl | hx := eq_zero_or_pos x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y : αˣ
h : 0 < (↑y : α)
⊢ ∃ (a : α), 0 < a ∧ a < (↑y : α)
have refine_3 : ∀ (z : αˣ) (hz : 1 < z), ∃ (a : α), 0 < a ∧ a < (↑y : α)
Tactic: obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x : α
y : αˣ
h : x < (↑y : α)
hx : 0 < x
⊢ ∃ (a : α), x < a ∧ a < (↑y : α)
have refine_3 : ∀ (x : αˣ) (h : (↑x : α) < (↑y : α)) (hx : 0 < (↑x : α)), ∃ (a : α), (↑x : α) < a ∧ a < (↑y : α)
Tactic: lift x to αˣ using hx.ne'.isUnit
Cleared hypotheses: x, h, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y x : αˣ
h : (↑x : α) < (↑y : α)
hx : 0 < (↑x : α)
⊢ ∃ (a : α), (↑x : α) < a ∧ a < (↑y : α)
have refine_3 : ∀ (z : αˣ) (hz : x < z) (hz' : z < y), ∃ (a : α), (↑x : α) < a ∧ a < (↑y : α)
Tactic: obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
⊢ Nontrivial.{u_1} αˣ
have this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
Tactic: have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
⊢ Nontrivial.{u_1} αˣ
have inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → Nontrivial.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → Nontrivial.{u_1} αˣ
⊢ Nontrivial.{u_1} αˣ
have inr : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → Nontrivial.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
⊢ DenselyOrdered.{u_1} αˣ
have this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
Tactic: have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ
have inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ
have inr : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
Tactic: have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inr : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inl₃ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₃ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inr₂ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₃ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₂ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inr₃ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₃ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₂ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inr₃ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inl₄ inl₅ inl₆ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₇ inl₈ inl₉ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inr₄ : ¬DenselyOrdered α → DenselyOrdered.{u_1} αˣ → ¬Nontrivial.{u_1} αˣ → DenselyOrdered α
Tactic: tauto
Cleared hypotheses: this