awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ 0 < embedRealFun (y - x)
have this : (↑{ num := 1, den := n + 1, den_nz := sorry, reduced := sorry } : ℝ) ∈ ratLt' (y - x)
Tactic: have : (Rat.mk' 1 (n + 1) (by simp) (by simp) : ℝ) ∈ ratLt' (y - x) := by
    simpa using hn.trans_lt <| nsmul_lt_nsmul_left hyz (show n < n + 1 by simp)
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
⊢ embedRealFun.{u_1} (M := M) 1 = 1
have a : embedRealFun.{u_1} (M := M) 1 ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
a : embedRealFun.{u_1} (M := M) 1 ≤ 1
⊢ embedRealFun.{u_1} (M := M) 1 = 1
have a₁ : 1 ≤ embedRealFun.{u_1} (M := M) 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
⊢ embedRealFun.{u_1} (M := M) 1 ≤ 1
have a : ∀ b ∈ ratLt'.{u_1} (M := M) 1, b ≤ 1
Tactic: apply csSup_le (ratLt'_nonempty 1)
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
⊢ ∀ b ∈ ratLt'.{u_1} (M := M) 1, b ≤ 1
have a : ∀ (x : ℚ), HSMul.hSMul (β := M) x.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑x.den : ℤ) 1 → LE.le (α := ℝ) (↑x : ℝ) 1
Tactic: suffices ∀ (x : ℚ), x.num • (1 : M) < (x.den : ℤ) • (1 : M) → (x : ℝ) ≤ 1 by simpa using this
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℚ
hx : HSMul.hSMul (β := M) x.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑x.den : ℤ) 1
⊢ LE.le (α := ℝ) (↑x : ℝ) 1
have a : x ≤ 1
Tactic: suffices x ≤ 1 by norm_cast
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
⊢ 1 ≤ embedRealFun.{u_1} (M := M) 1
have a : ∀ b ∈ upperBounds (ratLt'.{u_1} (M := M) 1), 1 ≤ b
Tactic: rw [le_csSup_iff (ratLt'_bddAbove (1 : M)) (ratLt'_nonempty 1)]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
⊢ ∀ (b : ℝ), (∀ x ∈ ratLt'.{u_1} (M := M) 1, x ≤ b) → 1 ≤ b
have a : ∀ (x : ℝ),
  (∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑y.den : ℤ) 1 → (↑y : ℝ) ≤ x) → 1 ≤ x
Tactic: suffices ∀ (x : ℝ), (∀ (y : ℚ), y.num • (1 : M) < (y.den : ℤ) • 1 → y ≤ x) → 1 ≤ x by
      simpa using this
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑y.den : ℤ) 1 → (↑y : ℝ) ≤ x
⊢ 1 ≤ x
have h' : ∀ (y : ℚ) (hy : y < 1), (↑y : ℝ) ≤ x
Tactic: have h' (y : ℚ) (hy : y < 1) : y ≤ x :=
      h _ ((smul_lt_smul_iff_of_pos_right zero_lt_one).mpr (by simpa using (Rat.lt_iff _ _).mp hy))
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑y.den : ℤ) 1 → (↑y : ℝ) ≤ x
h' : ∀ (y : ℚ) (hy : y < 1), (↑y : ℝ) ≤ x
⊢ 1 ≤ x
have a : ∀ (h' : x < 1), ∃ y < 1, x < (↑y : ℝ)
Tactic: contrapose! h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑y.den : ℤ) 1 → (↑y : ℝ) ≤ x
h' : x < 1
⊢ ∃ y < 1, x < (↑y : ℝ)
have a : ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hy : LT.lt (α := ℝ) (↑y : ℝ) 1), ∃ y < 1, x < (↑y : ℝ)
Tactic: obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
inst_4 : ZeroLEOneClass M
inst_5 : NeZero.{u_1} (R := M) 1
inst_6 : Archimedean M
x : ℝ
h : ∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑y.den : ℤ) 1 → (↑y : ℝ) ≤ x
h' : x < 1
y : ℚ
hxy : x < (↑y : ℝ)
hy : LT.lt (α := ℝ) (↑y : ℝ) 1
⊢ y < 1
have norm_cast : ∀ (hy : y < 1), y < 1
Tactic: norm_cast at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
have inl : Subsingleton M → ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
Tactic: cases subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
inl : Subsingleton M → ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
have inr : Nontrivial M → ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
Tactic: cases subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
h : Nontrivial M
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
have inr : ∀ (a : M) (ha : a ≠ 0), ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
Tactic: obtain ⟨a, ha⟩ := exists_ne (0 : M)
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
h : Nontrivial M
a : M
ha : a ≠ 0
one : One M := { one := |a| }
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
have this : ZeroLEOneClass M
Tactic: have : ZeroLEOneClass M := ⟨abs_nonneg a⟩
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
h : Nontrivial M
a : M
ha : a ≠ 0
one : One M := { one := |a| }
this : ZeroLEOneClass M
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
have this₁ : NeZero.{u_1} (R := M) 1
Tactic: have : NeZero (1 : M) := ⟨abs_ne_zero.mpr ha⟩
-- Lean 4 proof step from Mathlib.Data.Real.Hom (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Ring S
inst_4 : LinearOrder S
inst_5 : IsOrderedAddMonoid S
inst_6 : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
r : R
h : 0 ≤ r
⊢ LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) r : S)
have obtain : ∀ (s : R) (h : 0 ≤ s * s), LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) (s * s) : S)
Tactic: obtain ⟨s, rfl⟩ := hR r h
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Data.Real.Hom (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Ring S
inst_4 : LinearOrder S
inst_5 : IsOrderedAddMonoid S
inst_6 : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) (s * s) : S)
have rw : 0 ≤ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) s : S) ((f : (a : R) → S) s : S)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hr : r < 0
⊢ r.sign = -1
have rw : Eq (α := ℝ) (if r < 0 then -1 else if 0 < r then 1 else 0) (-1)
Tactic: rw [sign, if_pos hr]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hr : r < 0
rw : Eq (α := ℝ) (if r < 0 then -1 else if 0 < r then 1 else 0) (-1)
⊢ r.sign = -1
have rw₁ : Eq (α := ℝ) (-1) (-1)
Tactic: rw [sign, if_pos hr]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hr : 0 < r
⊢ r.sign = 1
have rw : Eq (α := ℝ) (if r < 0 then -1 else if 0 < r then 1 else 0) 1
Tactic: rw [sign, if_pos hr, if_neg hr.not_gt]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hr : 0 < r
rw : Eq (α := ℝ) (if r < 0 then -1 else if 0 < r then 1 else 0) 1
⊢ r.sign = 1
have rw₁ : Eq (α := ℝ) (if r < 0 then -1 else 1) 1
Tactic: rw [sign, if_pos hr, if_neg hr.not_gt]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hr : 0 < r
rw : Eq (α := ℝ) (if r < 0 then -1 else if 0 < r then 1 else 0) 1
rw₁ : Eq (α := ℝ) (if r < 0 then -1 else 1) 1
⊢ r.sign = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [sign, if_pos hr, if_neg hr.not_gt]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
⊢ sign 0 = 0
have rw : Eq (α := ℝ) (if LT.lt (α := ℝ) 0 0 then -1 else if LT.lt (α := ℝ) 0 0 then 1 else 0) 0
Tactic: rw [sign, if_neg (lt_irrefl _), if_neg (lt_irrefl _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
rw : Eq (α := ℝ) (if LT.lt (α := ℝ) 0 0 then -1 else if LT.lt (α := ℝ) 0 0 then 1 else 0) 0
⊢ sign 0 = 0
have rw₁ : Eq (α := ℝ) (if LT.lt (α := ℝ) 0 0 then 1 else 0) 0
Tactic: rw [sign, if_neg (lt_irrefl _), if_neg (lt_irrefl _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
rw : Eq (α := ℝ) (if LT.lt (α := ℝ) 0 0 then -1 else if LT.lt (α := ℝ) 0 0 then 1 else 0) 0
rw₁ : Eq (α := ℝ) (if LT.lt (α := ℝ) 0 0 then 1 else 0) 0
⊢ sign 0 = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [sign, if_neg (lt_irrefl _), if_neg (lt_irrefl _)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
have inl : ∀ (hn : r < 0), r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
have inr : sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
inr : sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
have inr₁ : ∀ (hp : 0 < r), r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
⊢ r.sign = 0 ↔ r = 0
have refine : ∀ (h : r.sign = 0), r = 0
Tactic: refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
h : r.sign = 0
⊢ r = 0
have inl : ∀ (hn : r < 0), r = 0
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
h : r.sign = 0
inl : ∀ (hn : r < 0), r = 0
⊢ r = 0
have inr : ∀ (h : sign 0 = 0), Eq (α := ℝ) 0 0
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
h : r.sign = 0
inl : ∀ (hn : r < 0), r = 0
inr : ∀ (h : sign 0 = 0), Eq (α := ℝ) 0 0
⊢ r = 0
have inr₁ : ∀ (hp : 0 < r), r = 0
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (hypothesis)
Goal:
r : ℝ
h : r.sign = 0
hn : r < 0
⊢ r = 0
have h₁ : Eq (α := ℝ) 1 0
Tactic: rw [sign_of_neg hn, neg_eq_zero] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Data.Real.Sign (hypothesis)
Goal:
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ r = 0
have h₁ : Eq (α := ℝ) 1 0
Tactic: rw [sign_of_pos hp] at h
Cleared hypotheses: h, hp
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inl : ∀ (hn : z < 0), sign (↑z : ℝ) = (↑z.sign : ℝ)
Tactic: obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
inl : ∀ (hn : z < 0), sign (↑z : ℝ) = (↑z.sign : ℝ)
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inr : sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)
Tactic: obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
inl : ∀ (hn : z < 0), sign (↑z : ℝ) = (↑z.sign : ℝ)
inr : sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inr₁ : ∀ (hp : 0 < z), sign (↑z : ℝ) = (↑z.sign : ℝ)
Tactic: obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
hn : z < 0
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inl : Eq (α := ℝ) (-1) (↑z.sign : ℝ)
Tactic: rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg,
      Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
hn : z < 0
inl : Eq (α := ℝ) (-1) (↑z.sign : ℝ)
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inl₁ : Eq (α := ℝ) (-1) (↑(-1) : ℝ)
Tactic: rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg,
      Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
hn : z < 0
inl : Eq (α := ℝ) (-1) (↑z.sign : ℝ)
inl₁ : Eq (α := ℝ) (-1) (↑(-1) : ℝ)
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inl₂ : Eq (α := ℝ) (-1) (-(↑1 : ℝ))
Tactic: rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg,
      Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
hn : z < 0
inl : Eq (α := ℝ) (-1) (↑z.sign : ℝ)
inl₁ : Eq (α := ℝ) (-1) (↑(-1) : ℝ)
inl₂ : Eq (α := ℝ) (-1) (-(↑1 : ℝ))
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inl₃ : Eq (α := ℝ) (-1) (-1)
Tactic: rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg,
      Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
⊢ sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)
have inr : sign 0 = (↑(Int.sign 0) : ℝ)
Tactic: rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
inr : sign 0 = (↑(Int.sign 0) : ℝ)
⊢ sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)
have inr₁ : Eq (α := ℝ) 0 (↑(Int.sign 0) : ℝ)
Tactic: rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
inr : sign 0 = (↑(Int.sign 0) : ℝ)
inr₁ : Eq (α := ℝ) 0 (↑(Int.sign 0) : ℝ)
⊢ sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)
have inr₂ : Eq (α := ℝ) 0 (↑0 : ℝ)
Tactic: rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
inr : sign 0 = (↑(Int.sign 0) : ℝ)
inr₁ : Eq (α := ℝ) 0 (↑(Int.sign 0) : ℝ)
inr₂ : Eq (α := ℝ) 0 (↑0 : ℝ)
⊢ sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)
have inr₃ : Eq (α := ℝ) 0 0
Tactic: rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
hp : 0 < z
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inr : Eq (α := ℝ) 1 (↑z.sign : ℝ)
Tactic: rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
hp : 0 < z
inr : Eq (α := ℝ) 1 (↑z.sign : ℝ)
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inr₁ : Eq (α := ℝ) 1 (↑1 : ℝ)
Tactic: rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
z : ℤ
hp : 0 < z
inr : Eq (α := ℝ) 1 (↑z.sign : ℝ)
inr₁ : Eq (α := ℝ) 1 (↑1 : ℝ)
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)
have inr₂ : Eq (α := ℝ) 1 1
Tactic: rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
⊢ (-r).sign = -r.sign
have inl : ∀ (hn : r < 0), (-r).sign = -r.sign
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), (-r).sign = -r.sign
⊢ (-r).sign = -r.sign
have inr : sign (-0) = -sign 0
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), (-r).sign = -r.sign
inr : sign (-0) = -sign 0
⊢ (-r).sign = -r.sign
have inr₁ : ∀ (hp : 0 < r), (-r).sign = -r.sign
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hn : r < 0
⊢ (-r).sign = -r.sign
have inl : (-r).sign = - -1
Tactic: rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hn : r < 0
inl : (-r).sign = - -1
⊢ (-r).sign = -r.sign
have inl₁ : Eq (α := ℝ) 1 (- -1)
Tactic: rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hn : r < 0
inl : (-r).sign = - -1
inl₁ : Eq (α := ℝ) 1 (- -1)
⊢ (-r).sign = -r.sign
have inl₂ : Eq (α := ℝ) 1 1
Tactic: rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
⊢ sign (-0) = -sign 0
have inr : sign (-0) = -0
Tactic: rw [sign_zero, neg_zero, sign_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
inr : sign (-0) = -0
⊢ sign (-0) = -sign 0
have inr₁ : sign 0 = 0
Tactic: rw [sign_zero, neg_zero, sign_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
inr : sign (-0) = -0
inr₁ : sign 0 = 0
⊢ sign (-0) = -sign 0
have inr₂ : Eq (α := ℝ) 0 0
Tactic: rw [sign_zero, neg_zero, sign_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hp : 0 < r
⊢ (-r).sign = -r.sign
have inr : (-r).sign = -1
Tactic: rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hp : 0 < r
inr : (-r).sign = -1
⊢ (-r).sign = -r.sign
have inr₁ : Eq (α := ℝ) (-1) (-1)
Tactic: rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
⊢ 0 ≤ r.sign * r
have inl : ∀ (hn : r < 0), 0 ≤ r.sign * r
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), 0 ≤ r.sign * r
⊢ 0 ≤ r.sign * r
have inr : 0 ≤ sign 0 * 0
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), 0 ≤ r.sign * r
inr : 0 ≤ sign 0 * 0
⊢ 0 ≤ r.sign * r
have inr₁ : ∀ (hp : 0 < r), 0 ≤ r.sign * r
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hn : r < 0
⊢ 0 ≤ r.sign * r
have inl : 0 ≤ -1 * r
Tactic: rw [sign_of_neg hn]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
⊢ 0 ≤ sign 0 * 0
have inr : LE.le (α := ℝ) 0 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r
have inr : 0 ≤ r
Tactic: rw [sign_of_pos hp, one_mul]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hr : r ≠ 0
⊢ 0 < r.sign * r
have refine : ∀ (h : 0 = r.sign * r), r = 0
Tactic: refine lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_
-- Lean 4 proof step from Mathlib.Data.Real.Sign (hypothesis)
Goal:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
⊢ r = 0
have hs0 : r.sign = 0
Tactic: have hs0 := (zero_eq_mul.mp h).resolve_right hr
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
⊢ r.sign⁻¹ = r.sign
have inl : ∀ (hn : r.sign = -1), r.sign⁻¹ = r.sign
Tactic: obtain hn | hz | hp := sign_apply_eq r
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r.sign = -1), r.sign⁻¹ = r.sign
⊢ r.sign⁻¹ = r.sign
have inr : ∀ (hz : r.sign = 0), r.sign⁻¹ = r.sign
Tactic: obtain hn | hz | hp := sign_apply_eq r
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r.sign = -1), r.sign⁻¹ = r.sign
inr : ∀ (hz : r.sign = 0), r.sign⁻¹ = r.sign
⊢ r.sign⁻¹ = r.sign
have inr₁ : ∀ (hp : r.sign = 1), r.sign⁻¹ = r.sign
Tactic: obtain hn | hz | hp := sign_apply_eq r
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign
have inl : Eq (α := ℝ) (-1)⁻¹ (-1)
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign
have inr : Eq (α := ℝ) 0⁻¹ 0
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign
have inr : Eq (α := ℝ) 1⁻¹ 1
Tactic: rw [hp]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
⊢ r⁻¹.sign = r.sign
have inl : ∀ (hn : r < 0), r⁻¹.sign = r.sign
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), r⁻¹.sign = r.sign
⊢ r⁻¹.sign = r.sign
have inr : sign 0⁻¹ = sign 0
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
inl : ∀ (hn : r < 0), r⁻¹.sign = r.sign
inr : sign 0⁻¹ = sign 0
⊢ r⁻¹.sign = r.sign
have inr₁ : ∀ (hp : 0 < r), r⁻¹.sign = r.sign
Tactic: obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hn : r < 0
⊢ r⁻¹.sign = r.sign
have inl : r⁻¹.sign = -1
Tactic: rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hn : r < 0
inl : r⁻¹.sign = -1
⊢ r⁻¹.sign = r.sign
have inl₁ : Eq (α := ℝ) (-1) (-1)
Tactic: rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
⊢ sign 0⁻¹ = sign 0
have inr : sign 0⁻¹ = 0
Tactic: rw [sign_zero, inv_zero, sign_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
inr : sign 0⁻¹ = 0
⊢ sign 0⁻¹ = sign 0
have inr₁ : sign 0 = 0
Tactic: rw [sign_zero, inv_zero, sign_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
inr : sign 0⁻¹ = 0
inr₁ : sign 0 = 0
⊢ sign 0⁻¹ = sign 0
have inr₂ : Eq (α := ℝ) 0 0
Tactic: rw [sign_zero, inv_zero, sign_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign
have inr : r⁻¹.sign = 1
Tactic: rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]
-- Lean 4 proof step from Mathlib.Data.Real.Sign (goal)
Goal:
r : ℝ
hp : 0 < r
inr : r⁻¹.sign = 1
⊢ r⁻¹.sign = r.sign
have inr₁ : Eq (α := ℝ) 1 1
Tactic: rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]
-- Lean 4 proof step from Mathlib.Data.Real.Sqrt (goal)
Goal:
x : ℝ≥0
⊢ HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) = x
have rw : HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 = x
Tactic: rw [← sq, sq_sqrt]