awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Embedding
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
this :
  ∀ (x : ℚ), HSMul.hSMul (β := M) x.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑x.den : ℤ) 1 → LE.le (α := ℝ) (↑x : ℝ) 1
⊢ ∀ b ∈ ratLt'.{u_1} (M := M) 1, b ≤ 1

Tactic:
simpa using this
-- Module: Mathlib.Data.Real.Embedding
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 : ∀ (x : ℚ), HSMul.hSMul (β := M) x.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑x.den : ℤ) 1 → LE.le (α := ℝ) (↑x : ℝ) 1
⊢ ∀ b ∈ ratLt'.{u_1} (M := M) 1, b ≤ 1

Tactic:
suffices ∀ (x : ℚ), x.num • (1 : M) < (x.den : ℤ) • (1 : M) → (x : ℝ) ≤ 1 by simpa using this
-- Module: Mathlib.Data.Real.Embedding
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
this : x ≤ 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : x ≤ 1
⊢ LE.le (α := ℝ) (↑x : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Data.Real.Embedding
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
a : x ≤ 1
⊢ LE.le (α := ℝ) (↑x : ℝ) 1

Tactic:
suffices x ≤ 1 by norm_cast
-- Module: Mathlib.Data.Real.Embedding
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
⊢ x ≤ 1

Tactic:
simpa [Rat.le_iff] using ((smul_lt_smul_iff_of_pos_right zero_lt_one).mp hx).le

Premises used: smul_lt_smul_iff_of_pos_right, LT.lt.le, zero_lt_one, Iff.mp, Rat.le_iff
-- Module: Mathlib.Data.Real.Embedding
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 : ∀ b ∈ upperBounds (ratLt'.{u_1} (M := M) 1), 1 ≤ b
⊢ 1 ≤ embedRealFun.{u_1} (M := M) 1

Tactic:
rw [le_csSup_iff (ratLt'_bddAbove (1 : M)) (ratLt'_nonempty 1)]

Premises used: le_csSup_iff, Archimedean.ratLt'_nonempty, OfNat.ofNat, Archimedean.ratLt'_bddAbove
-- Module: Mathlib.Data.Real.Embedding
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
this :
  ∀ (x : ℝ),
    (∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑y.den : ℤ) 1 → (↑y : ℝ) ≤ x) → 1 ≤ x
⊢ ∀ (b : ℝ), (∀ x ∈ ratLt'.{u_1} (M := M) 1, x ≤ b) → 1 ≤ b

Tactic:
simpa using this
-- Module: Mathlib.Data.Real.Embedding
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 :
  ∀ (x : ℝ),
    (∀ (y : ℚ), HSMul.hSMul (β := M) y.num 1 < HSMul.hSMul (α := ℤ) (β := M) (↑y.den : ℤ) 1 → (↑y : ℝ) ≤ x) → 1 ≤ x
⊢ ∀ (b : ℝ), (∀ x ∈ ratLt'.{u_1} (M := M) 1, x ≤ b) → 1 ≤ b

Tactic:
suffices ∀ (x : ℝ), (∀ (y : ℚ), y.num • (1 : M) < (y.den : ℤ) • 1 → y ≤ x) → 1 ≤ x by
      simpa using this
-- Module: Mathlib.Data.Real.Embedding
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
y : ℚ
hy : y < 1
⊢ y.num < (↑y.den : ℤ)

Tactic:
simpa using (Rat.lt_iff _ _).mp hy

Premises used: Rat.lt_iff, Iff.mp
-- Module: Mathlib.Data.Real.Embedding
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
⊢ ∀ (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))
-- Module: Mathlib.Data.Real.Embedding
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
a : ∀ (h' : x < 1), ∃ y < 1, x < (↑y : ℝ)
⊢ 1 ≤ x

Tactic:
contrapose! h'
-- Module: Mathlib.Data.Real.Embedding
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
a : ∀ (y : ℚ) (hxy : x < (↑y : ℝ)) (hy : LT.lt (α := ℝ) (↑y : ℝ) 1), ∃ y < 1, x < (↑y : ℝ)
⊢ ∃ y < 1, x < (↑y : ℝ)

Tactic:
obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'

Premises used: exists_rat_btwn
-- Module: Mathlib.Data.Real.Embedding
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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (hy : y < 1), y < 1
⊢ y < 1

Tactic:
norm_cast at hy
-- Module: Mathlib.Data.Real.Embedding
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, x < (↑y : ℝ)

Tactic:
exact ⟨y, (by norm_cast at hy), hxy⟩
-- Module: Mathlib.Data.Real.Embedding
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) → ℝ)
inr : Nontrivial M → ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)

Tactic:
cases subsingleton_or_nontrivial M

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
h : Subsingleton M
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)

Tactic:
⟨0, Function.injective_of_subsingleton _⟩

Premises used: Function.injective_of_subsingleton, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
h : Subsingleton M
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)

Tactic:
exact ⟨0, Function.injective_of_subsingleton _⟩
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
h : Nontrivial M
inr : ∀ (a : M) (ha : a ≠ 0), ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)

Tactic:
obtain ⟨a, ha⟩ := exists_ne (0 : M)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Data.Real.Embedding
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| }
⊢ ZeroLEOneClass M

Tactic:
have : ZeroLEOneClass M := ⟨abs_nonneg a⟩
-- Module: Mathlib.Data.Real.Embedding
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
⊢ NeZero.{u_1} (R := M) 1

Tactic:
have : NeZero (1 : M) := ⟨abs_ne_zero.mpr ha⟩
-- Module: Mathlib.Data.Real.Embedding
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_1 : ZeroLEOneClass M
this : NeZero.{u_1} (R := M) 1
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)

Tactic:
⟨embedReal M, embedReal_injective M⟩

Premises used: Archimedean.embedReal, Archimedean.embedReal_injective, Exists.intro
-- Module: Mathlib.Data.Real.Embedding
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_1 : ZeroLEOneClass M
this : NeZero.{u_1} (R := M) 1
⊢ ∃ (f : M →+o ℝ), Function.Injective (α := M) (β := ℝ) (⇑f : (a : M) → ℝ)

Tactic:
exact ⟨embedReal M, embedReal_injective M⟩
-- Module: Mathlib.Data.Real.Hom
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
⊢ Nonempty.{max 1 (u_1 + 1)} (α →+*o ℝ)

Tactic:
⟨ConditionallyCompleteLinearOrderedField.inducedOrderRingHom α ℝ⟩

Premises used: Real, ConditionallyCompleteLinearOrderedField.inducedOrderRingHom, Nonempty.intro
-- Module: Mathlib.Data.Real.Hom
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
obtain : ∀ (s : R) (h : 0 ≤ s * s), LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) (s * s) : S)
⊢ LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) r : S)

Tactic:
obtain ⟨s, rfl⟩ := hR r h

Premises used: rfl
-- Module: Mathlib.Data.Real.Hom
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
rw : 0 ≤ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) s : S) ((f : (a : R) → S) s : S)
⊢ LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) (s * s) : S)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.Data.Real.Hom
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
⊢ 0 ≤ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) s : S) ((f : (a : R) → S) s : S)

Tactic:
apply mul_self_nonneg

Premises used: mul_self_nonneg
-- Module: Mathlib.Data.Real.Hom
Goal:
F : Type u_1
inst : FunLike F ℝ ℝ
inst_1 : RingHomClass F ℝ ℝ
f : F
r : ℝ
⊢ (f : (a : ℝ) → ℝ) r = r

Tactic:
DFunLike.congr_fun (Unique.eq_default (RingHomClass.toRingHom f)) r

Premises used: DFunLike.congr_fun, Unique.eq_default, RingHomClass.toRingHom
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hr : r < 0
rw : Eq (α := ℝ) (if r < 0 then -1 else if 0 < r then 1 else 0) (-1)
rw₁ rw₂ : Eq (α := ℝ) (-1) (-1)
⊢ r.sign = -1

Tactic:
rw [sign, if_pos hr]

Premises used: Real.sign, if_pos
-- Module: Mathlib.Data.Real.Sign
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
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ r.sign = 1

Tactic:
rw [sign, if_pos hr, if_neg hr.not_gt]

Premises used: Real.sign, if_pos, LT.lt.not_gt, if_neg
-- Module: Mathlib.Data.Real.Sign
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
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ sign 0 = 0

Tactic:
rw [sign, if_neg (lt_irrefl _), if_neg (lt_irrefl _)]

Premises used: lt_irrefl, Real.sign, if_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Real.Sign
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
inr₁ : ∀ (hp : 0 < r), r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r < 0
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
Or.inl <| sign_of_neg hn

Premises used: Or.inl, Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r < 0
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
exact Or.inl <| sign_of_neg hn

Premises used: Or.inl, Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

Tactic:
Or.inr <| Or.inl <| sign_zero

Premises used: Real.sign_zero, Or.inl, Or.inr
-- Module: Mathlib.Data.Real.Sign
Goal:
⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

Tactic:
exact Or.inr <| Or.inl <| sign_zero

Premises used: Real.sign_zero, Or.inl, Or.inr
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
Or.inr <| Or.inr <| sign_of_pos hp

Premises used: Real.sign_of_pos, Or.inr
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
exact Or.inr <| Or.inr <| sign_of_pos hp

Premises used: Real.sign_of_pos, Or.inr
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : r ≠ 0
⊢ r.sign = -1 ∨ r.sign = 1

Tactic:
h.lt_or_gt.imp sign_of_neg sign_of_pos

Premises used: Real.sign_of_pos, Or.imp, Real.sign_of_neg, Ne.lt_or_gt
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
⊢ r.sign = 0 ↔ r = 0

Tactic:
⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩

Premises used: Real.sign_zero, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
refine : ∀ (h : r.sign = 0), r = 0
⊢ r.sign = 0 ↔ r = 0

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : r.sign = 0
inl : ∀ (hn : r < 0), r = 0
inr : ∀ (h : sign 0 = 0), Eq (α := ℝ) 0 0
inr₁ : ∀ (hp : 0 < r), r = 0
⊢ r = 0

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : r.sign = 0
hn : r < 0
⊢ Eq (α := ℝ) 1 0

Tactic:
rw [sign_of_neg hn, neg_eq_zero] at h

Premises used: neg_eq_zero, Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : r.sign = 0
hn : r < 0
h₁ : Eq (α := ℝ) 1 0
⊢ r < 0

Tactic:
rw [sign_of_neg hn, neg_eq_zero] at h

Premises used: neg_eq_zero, Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : Eq (α := ℝ) 1 0
hn : r < 0
⊢ r = 0

Tactic:
(one_ne_zero h).elim

Premises used: False.elim, one_ne_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : Eq (α := ℝ) 1 0
hn : r < 0
⊢ r = 0

Tactic:
exact (one_ne_zero h).elim

Premises used: False.elim, one_ne_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
h : sign 0 = 0
⊢ Eq (α := ℝ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ Eq (α := ℝ) 1 0

Tactic:
rw [sign_of_pos hp] at h

Premises used: Real.sign_of_pos
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : r.sign = 0
hp : 0 < r
h₁ : Eq (α := ℝ) 1 0
⊢ 0 < r

Tactic:
rw [sign_of_pos hp] at h

Premises used: Real.sign_of_pos
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : Eq (α := ℝ) 1 0
hp : 0 < r
⊢ r = 0

Tactic:
(one_ne_zero h).elim

Premises used: False.elim, one_ne_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
h : Eq (α := ℝ) 1 0
hp : 0 < r
⊢ r = 0

Tactic:
exact (one_ne_zero h).elim

Premises used: False.elim, one_ne_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
z : ℤ
inl : ∀ (hn : z < 0), sign (↑z : ℝ) = (↑z.sign : ℝ)
inr : sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)
inr₁ : ∀ (hp : 0 < z), sign (↑z : ℝ) = (↑z.sign : ℝ)
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)

Tactic:
obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Real.Sign
Goal:
z : ℤ
hn : z < 0
inl : Eq (α := ℝ) (-1) (↑z.sign : ℝ)
inl₁ : Eq (α := ℝ) (-1) (↑(-1) : ℝ)
inl₂ : Eq (α := ℝ) (-1) (-(↑1 : ℝ))
inl₃ inl₄ : Eq (α := ℝ) (-1) (-1)
⊢ sign (↑z : ℝ) = (↑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]

Premises used: Iff.mpr, Int.cast_neg, Int.sign_eq_neg_one_of_neg, Int.cast_lt_zero, Real.sign_of_neg, Int.cast_one
-- Module: Mathlib.Data.Real.Sign
Goal:
inr : sign 0 = (↑(Int.sign 0) : ℝ)
inr₁ : Eq (α := ℝ) 0 (↑(Int.sign 0) : ℝ)
inr₂ : Eq (α := ℝ) 0 (↑0 : ℝ)
inr₃ inr₄ : Eq (α := ℝ) 0 0
⊢ sign (↑0 : ℝ) = (↑(Int.sign 0) : ℝ)

Tactic:
rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]

Premises used: Int.cast_zero, Real.sign_zero, Int.sign_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
z : ℤ
hp : 0 < z
inr : Eq (α := ℝ) 1 (↑z.sign : ℝ)
inr₁ : Eq (α := ℝ) 1 (↑1 : ℝ)
inr₂ inr₃ : Eq (α := ℝ) 1 1
⊢ sign (↑z : ℝ) = (↑z.sign : ℝ)

Tactic:
rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]

Premises used: Iff.mpr, Real.sign_of_pos, Int.cast_pos, Int.sign_eq_one_of_pos, Int.cast_one
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
inl : ∀ (hn : r < 0), (-r).sign = -r.sign
inr : sign (-0) = -sign 0
inr₁ : ∀ (hp : 0 < r), (-r).sign = -r.sign
⊢ (-r).sign = -r.sign

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r < 0
inl : (-r).sign = - -1
inl₁ : Eq (α := ℝ) 1 (- -1)
inl₂ inl₃ : Eq (α := ℝ) 1 1
⊢ (-r).sign = -r.sign

Tactic:
rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]

Premises used: Iff.mpr, neg_pos, neg_neg, Real.sign_of_pos, Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
inr : sign (-0) = -0
inr₁ : sign 0 = 0
inr₂ inr₃ : Eq (α := ℝ) 0 0
⊢ sign (-0) = -sign 0

Tactic:
rw [sign_zero, neg_zero, sign_zero]

Premises used: Real.sign_zero, neg_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : 0 < r
inr : (-r).sign = -1
inr₁ inr₂ : Eq (α := ℝ) (-1) (-1)
⊢ (-r).sign = -r.sign

Tactic:
rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]

Premises used: Iff.mpr, neg_lt_zero, Real.sign_of_pos, Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
inl : ∀ (hn : r < 0), 0 ≤ r.sign * r
inr : 0 ≤ sign 0 * 0
inr₁ : ∀ (hp : 0 < r), 0 ≤ r.sign * r
⊢ 0 ≤ r.sign * r

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r < 0
inl : 0 ≤ -1 * r
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_neg hn]

Premises used: Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r < 0
⊢ LE.le (α := ℝ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r

Tactic:
exact mul_nonneg_of_nonpos_of_nonpos (by simp) hn.le

Premises used: LT.lt.le, mul_nonneg_of_nonpos_of_nonpos
-- Module: Mathlib.Data.Real.Sign
Goal:
inr inr₁ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ sign 0 * 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : 0 < r
inr : 0 ≤ r
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_pos hp, one_mul]

Premises used: Real.sign_of_pos, one_mul
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : 0 < r
⊢ 0 ≤ r

Tactic:
hp.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : 0 < r
⊢ 0 ≤ r

Tactic:
exact hp.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hr : r ≠ 0
⊢ 0 < r.sign * r

Tactic:
lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_

Premises used: Real.sign_mul_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hr : r ≠ 0
refine : ∀ (h : 0 = r.sign * r), r = 0
⊢ 0 < r.sign * r

Tactic:
refine lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_

Premises used: Real.sign_mul_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
⊢ r.sign = 0

Tactic:
have hs0 := (zero_eq_mul.mp h).resolve_right hr
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
hs0 : r.sign = 0
⊢ r = 0

Tactic:
sign_eq_zero_iff.mp hs0

Premises used: Real.sign_eq_zero_iff, Iff.mp
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
hs0 : r.sign = 0
⊢ r = 0

Tactic:
exact sign_eq_zero_iff.mp hs0

Premises used: Real.sign_eq_zero_iff, Iff.mp
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
inl : ∀ (hn : r.sign = -1), r.sign⁻¹ = r.sign
inr : ∀ (hz : r.sign = 0), r.sign⁻¹ = r.sign
inr₁ : ∀ (hp : r.sign = 1), r.sign⁻¹ = r.sign
⊢ r.sign⁻¹ = r.sign

Tactic:
obtain hn | hz | hp := sign_apply_eq r

Premises used: Real.sign_apply_eq
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r.sign = -1
inl : Eq (α := ℝ) (-1)⁻¹ (-1)
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hn]
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r.sign = -1
⊢ Eq (α := ℝ) (-1)⁻¹ (-1)

Tactic:
simp
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hz : r.sign = 0
inr : Eq (α := ℝ) 0⁻¹ 0
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hz]
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hz : r.sign = 0
⊢ Eq (α := ℝ) 0⁻¹ 0

Tactic:
inv_zero

Premises used: inv_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hz : r.sign = 0
⊢ Eq (α := ℝ) 0⁻¹ 0

Tactic:
exact inv_zero

Premises used: inv_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : r.sign = 1
inr : Eq (α := ℝ) 1⁻¹ 1
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hp]
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : r.sign = 1
⊢ Eq (α := ℝ) 1⁻¹ 1

Tactic:
inv_one

Premises used: inv_one
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : r.sign = 1
⊢ Eq (α := ℝ) 1⁻¹ 1

Tactic:
exact inv_one

Premises used: inv_one
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
inl : ∀ (hn : r < 0), r⁻¹.sign = r.sign
inr : sign 0⁻¹ = sign 0
inr₁ : ∀ (hp : 0 < r), r⁻¹.sign = r.sign
⊢ r⁻¹.sign = r.sign

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hn : r < 0
inl : r⁻¹.sign = -1
inl₁ inl₂ : Eq (α := ℝ) (-1) (-1)
⊢ r⁻¹.sign = r.sign

Tactic:
rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]

Premises used: Iff.mpr, inv_lt_zero, Real.sign_of_neg
-- Module: Mathlib.Data.Real.Sign
Goal:
inr : sign 0⁻¹ = 0
inr₁ : sign 0 = 0
inr₂ inr₃ : Eq (α := ℝ) 0 0
⊢ sign 0⁻¹ = sign 0

Tactic:
rw [sign_zero, inv_zero, sign_zero]

Premises used: inv_zero, Real.sign_zero
-- Module: Mathlib.Data.Real.Sign
Goal:
r : ℝ
hp : 0 < r
inr : r⁻¹.sign = 1
inr₁ inr₂ : Eq (α := ℝ) 1 1
⊢ r⁻¹.sign = r.sign

Tactic:
rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]

Premises used: Iff.mpr, inv_pos, Real.sign_of_pos
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
⊢ HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 = x

Tactic:
sqrt.symm_apply_apply _

Premises used: NNReal.sqrt, OrderIso.symm_apply_apply
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) x 2) = x

Tactic:
sqrt.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply, NNReal.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
rw : HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 = x
rw₁ rw₂ : x = x
⊢ HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) = x

Tactic:
rw [← sq, sq_sqrt]

Premises used: sq, NNReal.sq_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
rw : (sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) x 2) = x
rw₁ rw₂ : x = x
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * x) = x

Tactic:
rw [← sq, sqrt_sq]

Premises used: NNReal.sqrt_sq, sq