awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
x y : EReal
h : x ≤ y
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
⊢ (sign : (a : EReal) → SignType) x = neg ∧ (sign : (a : EReal) → SignType) y = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ (sign : (a : EReal) → SignType) y = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ (sign : (a : EReal) → SignType) y = pos ∧ x.abs ≤ y.abs
have h₁ : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
  (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
Tactic: rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
⊢ (sign : (a : EReal) → SignType) x = neg ∧ (sign : (a : EReal) → SignType) y = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ (sign : (a : EReal) → SignType) y = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ (sign : (a : EReal) → SignType) y = pos ∧ x.abs ≤ y.abs
have mp : ∀ (hy : (sign : (a : EReal) → SignType) y = zero),
  (sign : (a : EReal) → SignType) x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ zero = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ zero = pos ∧ x.abs ≤ y.abs
Tactic: cases hy : sign y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
mp :
  ∀ (hy : (sign : (a : EReal) → SignType) y = zero),
    (sign : (a : EReal) → SignType) x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨
      (sign : (a : EReal) → SignType) x = zero ∧ zero = zero ∨
        (sign : (a : EReal) → SignType) x = pos ∧ zero = pos ∧ x.abs ≤ y.abs
⊢ (sign : (a : EReal) → SignType) x = neg ∧ (sign : (a : EReal) → SignType) y = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ (sign : (a : EReal) → SignType) y = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ (sign : (a : EReal) → SignType) y = pos ∧ x.abs ≤ y.abs
have mp₁ : ∀ (hy : (sign : (a : EReal) → SignType) y = neg),
  (sign : (a : EReal) → SignType) x = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ neg = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ neg = pos ∧ x.abs ≤ y.abs
Tactic: cases hy : sign y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
mp :
  ∀ (hy : (sign : (a : EReal) → SignType) y = zero),
    (sign : (a : EReal) → SignType) x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨
      (sign : (a : EReal) → SignType) x = zero ∧ zero = zero ∨
        (sign : (a : EReal) → SignType) x = pos ∧ zero = pos ∧ x.abs ≤ y.abs
mp₁ :
  ∀ (hy : (sign : (a : EReal) → SignType) y = neg),
    (sign : (a : EReal) → SignType) x = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨
      (sign : (a : EReal) → SignType) x = zero ∧ neg = zero ∨
        (sign : (a : EReal) → SignType) x = pos ∧ neg = pos ∧ x.abs ≤ y.abs
⊢ (sign : (a : EReal) → SignType) x = neg ∧ (sign : (a : EReal) → SignType) y = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ (sign : (a : EReal) → SignType) y = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ (sign : (a : EReal) → SignType) y = pos ∧ x.abs ≤ y.abs
have mp₂ : ∀ (hy : (sign : (a : EReal) → SignType) y = pos),
  (sign : (a : EReal) → SignType) x = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ pos = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Tactic: cases hy : sign y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
hy : (sign : (a : EReal) → SignType) y = zero
⊢ (sign : (a : EReal) → SignType) x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ zero = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ zero = pos ∧ x.abs ≤ y.abs
have mp : ∀ (h : (↑zero : EReal) * (↑x.abs : EReal) ≤ (↑zero : EReal) * (↑y.abs : EReal))
  (hs :
    Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType))
  (hy : (sign : (a : EReal) → SignType) y = zero),
  zero = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ zero = zero ∧ zero = zero ∨ zero = pos ∧ zero = pos ∧ x.abs ≤ y.abs
Tactic: rw [hs, hy] at h ⊢
Cleared hypotheses: h, hs, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
hy : (sign : (a : EReal) → SignType) y = neg
⊢ (sign : (a : EReal) → SignType) x = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ neg = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ neg = pos ∧ x.abs ≤ y.abs
have mp : ∀ (h : (↑neg : EReal) * (↑x.abs : EReal) ≤ (↑neg : EReal) * (↑y.abs : EReal))
  (hs :
    Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType))
  (hy : (sign : (a : EReal) → SignType) y = neg),
  neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs
Tactic: rw [hs, hy] at h ⊢
Cleared hypotheses: h, hs, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
hy : (sign : (a : EReal) → SignType) y = pos
⊢ (sign : (a : EReal) → SignType) x = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨
    (sign : (a : EReal) → SignType) x = zero ∧ pos = zero ∨
      (sign : (a : EReal) → SignType) x = pos ∧ pos = pos ∧ x.abs ≤ y.abs
have mp : ∀ (h : (↑pos : EReal) * (↑x.abs : EReal) ≤ (↑pos : EReal) * (↑y.abs : EReal))
  (hs :
    Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType))
  (hy : (sign : (a : EReal) → SignType) y = pos),
  pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Tactic: rw [hs, hy] at h ⊢
Cleared hypotheses: h, hs, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (↑neg : EReal) * (↑x.abs : EReal) ≤ (↑neg : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
hy : (sign : (a : EReal) → SignType) y = neg
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs
have mp : neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs
Tactic: left
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (↑pos : EReal) * (↑x.abs : EReal) ≤ (↑pos : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
hy : (sign : (a : EReal) → SignType) y = pos
⊢ pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
have mp : pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Tactic: right
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (↑pos : EReal) * (↑x.abs : EReal) ≤ (↑pos : EReal) * (↑y.abs : EReal)
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
hy : (sign : (a : EReal) → SignType) y = pos
⊢ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
have mp : pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Tactic: right
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (sign : (a : EReal) → SignType) x = neg ∧ (sign : (a : EReal) → SignType) y = neg ∧ y.abs ≤ x.abs
⊢ x ≤ y
have mpr : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
  (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
Tactic: rw [← x.sign_mul_abs, ← y.sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (sign : (a : EReal) → SignType) x = zero ∧ (sign : (a : EReal) → SignType) y = zero
⊢ x ≤ y
have mpr : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
  (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
Tactic: rw [← x.sign_mul_abs, ← y.sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (sign : (a : EReal) → SignType) x = pos ∧ (sign : (a : EReal) → SignType) y = pos ∧ x.abs ≤ y.abs
⊢ x ≤ y
have mpr : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
  (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
Tactic: rw [← x.sign_mul_abs, ← y.sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y z : EReal
⊢ x * y * z = x * (y * z)
have rw : (x * y * z).abs = (x * (y * z)).abs ∧
  Eq (α := SignType) ((sign : (a : EReal) → SignType) (x * y * z) : SignType)
    ((sign : (a : EReal) → SignType) (x * (y * z)) : SignType)
Tactic: rw [← sign_eq_and_abs_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
x0 : 0 < x
a b : EReal
h : a ≤ b
⊢ LE.le (α := EReal)
    ((fun (x : { x : EReal // 0 < x }) (y : EReal) ↦ (↑x : EReal) * y) (Subtype.mk (p := fun (x : EReal) ↦ 0 < x) x x0)
      a)
    ((fun (x : { x : EReal // 0 < x }) (y : EReal) ↦ (↑x : EReal) * y) (Subtype.mk (p := fun (x : EReal) ↦ 0 < x) x x0)
      b)
have simp : ∀
  (h :
    LT.lt (α := SignType) ((sign : (a : EReal) → SignType) a : SignType)
        ((sign : (a : EReal) → SignType) b : SignType) ∨
      (sign : (a : EReal) → SignType) a = neg ∧ (sign : (a : EReal) → SignType) b = neg ∧ b.abs ≤ a.abs ∨
        (sign : (a : EReal) → SignType) a = zero ∧ (sign : (a : EReal) → SignType) b = zero ∨
          (sign : (a : EReal) → SignType) a = pos ∧ (sign : (a : EReal) → SignType) b = pos ∧ a.abs ≤ b.abs),
  LT.lt (α := SignType) ((sign : (a : EReal) → SignType) a : SignType) ((sign : (a : EReal) → SignType) b : SignType) ∨
    (sign : (a : EReal) → SignType) a = neg ∧ (sign : (a : EReal) → SignType) b = neg ∧ x.abs * b.abs ≤ x.abs * a.abs ∨
      (sign : (a : EReal) → SignType) a = zero ∧ (sign : (a : EReal) → SignType) b = zero ∨
        (sign : (a : EReal) → SignType) a = pos ∧
          (sign : (a : EReal) → SignType) b = pos ∧ x.abs * a.abs ≤ x.abs * b.abs
Tactic: simp only [le_iff_sign, EReal.sign_mul, sign_pos x0, one_mul, EReal.abs_mul] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ a * c ≤ b * c
have rw : -c * b ≤ -c * a
Tactic: rw [mul_comm a c, mul_comm b c, ← neg_le_neg_iff, ← neg_mul c b, ← neg_mul c a]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -c * a
have hc₁ : 0 ≤ -c
Tactic: rw [← neg_zero, EReal.le_neg] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a_1 : EReal
n : ℕ
a : ℝ
ha : (↑a : EReal) ≠ ⊤
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
have obtain : ∀ (m : ℕ) (an_m : a * (↑n : ℝ) ≤ (↑m : ℝ)), ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
Tactic: obtain ⟨m, an_m⟩ := exists_nat_ge (a * n)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a_1 : EReal
n : ℕ
a : ℝ
ha : (↑a : EReal) ≠ ⊤
m : ℕ
an_m : a * (↑n : ℝ) ≤ (↑m : ℝ)
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
have h : (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
Tactic: use m
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a_1 : EReal
n : ℕ
a : ℝ
ha : (↑a : EReal) ≠ ⊤
m : ℕ
an_m : a * (↑n : ℝ) ≤ (↑m : ℝ)
⊢ (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
have h : (↑a : EReal) * (↑(↑n : ℝ) : EReal) ≤ (↑m : EReal)
Tactic: rwa [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, ← EReal.coe_mul, EReal.coe_le_coe_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a_1 : EReal
n : ℕ
a : ℝ
ha : (↑a : EReal) ≠ ⊤
m : ℕ
an_m : a * (↑n : ℝ) ≤ (↑m : ℝ)
h : (↑a : EReal) * (↑(↑n : ℝ) : EReal) ≤ (↑m : EReal)
⊢ (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
have h₁ : (↑a : EReal) * (↑(↑n : ℝ) : EReal) ≤ (↑(↑m : ℝ) : EReal)
Tactic: rwa [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, ← EReal.coe_mul, EReal.coe_le_coe_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a_1 : EReal
n : ℕ
a : ℝ
ha : (↑a : EReal) ≠ ⊤
m : ℕ
an_m : a * (↑n : ℝ) ≤ (↑m : ℝ)
h : (↑a : EReal) * (↑(↑n : ℝ) : EReal) ≤ (↑m : EReal)
h₁ : (↑a : EReal) * (↑(↑n : ℝ) : EReal) ≤ (↑(↑m : ℝ) : EReal)
⊢ (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
have h₂ : (↑(a * (↑n : ℝ)) : EReal) ≤ (↑(↑m : ℝ) : EReal)
Tactic: rwa [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, ← EReal.coe_mul, EReal.coe_le_coe_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
⊢ min (-x) (-y) = -max x y
have inl : ∀ (h : x ≤ y), min (-x) (-y) = -max x y
Tactic: rcases le_total x y with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
inl : ∀ (h : x ≤ y), min (-x) (-y) = -max x y
⊢ min (-x) (-y) = -max x y
have inr : ∀ (h : y ≤ x), min (-x) (-y) = -max x y
Tactic: rcases le_total x y with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
⊢ max (-x) (-y) = -min x y
have inl : ∀ (h : x ≤ y), max (-x) (-y) = -min x y
Tactic: rcases le_total x y with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
inl : ∀ (h : x ≤ y), max (-x) (-y) = -min x y
⊢ max (-x) (-y) = -min x y
have inr : ∀ (h : y ≤ x), max (-x) (-y) = -min x y
Tactic: rcases le_total x y with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
⊢ (↑0⁻¹ : EReal) = 0
have rw : (↑0 : EReal) = 0
Tactic: rw [GroupWithZero.inv_zero, coe_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
rw : (↑0 : EReal) = 0
⊢ (↑0⁻¹ : EReal) = 0
have rw₁ : Eq (α := EReal) 0 0
Tactic: rw [GroupWithZero.inv_zero, coe_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
⊢ Eq (α := EReal) 1⁻¹ 1
have nth_rw : (↑1 : EReal)⁻¹ = 1
Tactic: nth_rw 1 [← coe_one, ← coe_inv 1, _root_.inv_one, coe_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
nth_rw : (↑1 : EReal)⁻¹ = 1
⊢ Eq (α := EReal) 1⁻¹ 1
have nth_rw₁ : (↑1⁻¹ : EReal) = 1
Tactic: nth_rw 1 [← coe_one, ← coe_inv 1, _root_.inv_one, coe_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
nth_rw : (↑1 : EReal)⁻¹ = 1
nth_rw₁ : (↑1⁻¹ : EReal) = 1
⊢ Eq (α := EReal) 1⁻¹ 1
have nth_rw₂ : (↑1 : EReal) = 1
Tactic: nth_rw 1 [← coe_one, ← coe_inv 1, _root_.inv_one, coe_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
nth_rw : (↑1 : EReal)⁻¹ = 1
nth_rw₁ : (↑1⁻¹ : EReal) = 1
nth_rw₂ : (↑1 : EReal) = 1
⊢ Eq (α := EReal) 1⁻¹ 1
have nth_rw₃ : Eq (α := EReal) 1 1
Tactic: nth_rw 1 [← coe_one, ← coe_inv 1, _root_.inv_one, coe_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
⊢ (-a)⁻¹ = -a⁻¹
have bot : Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
bot : Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
⊢ (-a)⁻¹ = -a⁻¹
have coe : ∀ (a : ℝ), (-(↑a : EReal))⁻¹ = -(↑a : EReal)⁻¹
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
bot : Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
coe : ∀ (a : ℝ), (-(↑a : EReal))⁻¹ = -(↑a : EReal)⁻¹
⊢ (-a)⁻¹ = -a⁻¹
have top : Eq (α := EReal) (-⊤)⁻¹ (-⊤⁻¹)
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
⊢ Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
have bot : Eq (α := EReal) ⊤⁻¹ (-⊥⁻¹)
Tactic: rw [neg_bot, inv_top, inv_bot, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
bot : Eq (α := EReal) ⊤⁻¹ (-⊥⁻¹)
⊢ Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
have bot₁ : Eq (α := EReal) 0 (-⊥⁻¹)
Tactic: rw [neg_bot, inv_top, inv_bot, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
bot : Eq (α := EReal) ⊤⁻¹ (-⊥⁻¹)
bot₁ : Eq (α := EReal) 0 (-⊥⁻¹)
⊢ Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
have bot₂ : Eq (α := EReal) 0 (-0)
Tactic: rw [neg_bot, inv_top, inv_bot, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
bot : Eq (α := EReal) ⊤⁻¹ (-⊥⁻¹)
bot₁ : Eq (α := EReal) 0 (-⊥⁻¹)
bot₂ : Eq (α := EReal) 0 (-0)
⊢ Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
have bot₃ : Eq (α := EReal) 0 0
Tactic: rw [neg_bot, inv_top, inv_bot, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
⊢ Eq (α := EReal) (-⊤)⁻¹ (-⊤⁻¹)
have top : Eq (α := EReal) ⊥⁻¹ (-⊤⁻¹)
Tactic: rw [neg_top, inv_bot, inv_top, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
top : Eq (α := EReal) ⊥⁻¹ (-⊤⁻¹)
⊢ Eq (α := EReal) (-⊤)⁻¹ (-⊤⁻¹)
have top₁ : Eq (α := EReal) 0 (-⊤⁻¹)
Tactic: rw [neg_top, inv_bot, inv_top, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
top : Eq (α := EReal) ⊥⁻¹ (-⊤⁻¹)
top₁ : Eq (α := EReal) 0 (-⊤⁻¹)
⊢ Eq (α := EReal) (-⊤)⁻¹ (-⊤⁻¹)
have top₂ : Eq (α := EReal) 0 (-0)
Tactic: rw [neg_top, inv_bot, inv_top, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
top : Eq (α := EReal) ⊥⁻¹ (-⊤⁻¹)
top₁ : Eq (α := EReal) 0 (-⊤⁻¹)
top₂ : Eq (α := EReal) 0 (-0)
⊢ Eq (α := EReal) (-⊤)⁻¹ (-⊤⁻¹)
have top₃ : Eq (α := EReal) 0 0
Tactic: rw [neg_top, inv_bot, inv_top, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ a⁻¹⁻¹ = a
have rw : (↑a.toReal : EReal)⁻¹⁻¹ = (↑a.toReal : EReal)
Tactic: rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
rw : (↑a.toReal : EReal)⁻¹⁻¹ = (↑a.toReal : EReal)
⊢ a⁻¹⁻¹ = a
have rw₁ : (↑a.toReal⁻¹ : EReal)⁻¹ = (↑a.toReal : EReal)
Tactic: rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
rw : (↑a.toReal : EReal)⁻¹⁻¹ = (↑a.toReal : EReal)
rw₁ : (↑a.toReal⁻¹ : EReal)⁻¹ = (↑a.toReal : EReal)
⊢ a⁻¹⁻¹ = a
have rw₂ : (↑a.toReal⁻¹⁻¹ : EReal) = (↑a.toReal : EReal)
Tactic: rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
rw : (↑a.toReal : EReal)⁻¹⁻¹ = (↑a.toReal : EReal)
rw₁ : (↑a.toReal⁻¹ : EReal)⁻¹ = (↑a.toReal : EReal)
rw₂ : (↑a.toReal⁻¹⁻¹ : EReal) = (↑a.toReal : EReal)
⊢ a⁻¹⁻¹ = a
have rw₃ : (↑a.toReal : EReal) = (↑a.toReal : EReal)
Tactic: rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_pos : 0 < x
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
have top_pos : ⊤⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
Tactic: rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_pos : 0 < x
top_pos : ⊤⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
have top_pos₁ : 0 = 0 * (↑x : EReal)⁻¹
Tactic: rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_pos : 0 < x
top_pos : ⊤⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
top_pos₁ : 0 = 0 * (↑x : EReal)⁻¹
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
have top_pos₂ : Eq (α := EReal) 0 0
Tactic: rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
have top_neg : ⊥⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
Tactic: rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
top_neg : ⊥⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
have top_neg₁ : 0 = ⊤⁻¹ * (↑x : EReal)⁻¹
Tactic: rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
top_neg : ⊥⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
top_neg₁ : 0 = ⊤⁻¹ * (↑x : EReal)⁻¹
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
have top_neg₂ : 0 = 0 * (↑x : EReal)⁻¹
Tactic: rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
top_neg : ⊥⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
top_neg₁ : 0 = ⊤⁻¹ * (↑x : EReal)⁻¹
top_neg₂ : 0 = 0 * (↑x : EReal)⁻¹
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
have top_neg₃ : Eq (α := EReal) 0 0
Tactic: rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_pos : 0 < x
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
have pos_bot : ⊥⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
Tactic: rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_pos : 0 < x
pos_bot : ⊥⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
have pos_bot₁ : 0 = (↑x : EReal)⁻¹ * 0
Tactic: rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_pos : 0 < x
pos_bot : ⊥⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
pos_bot₁ : 0 = (↑x : EReal)⁻¹ * 0
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
have pos_bot₂ : Eq (α := EReal) 0 0
Tactic: rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : ℝ
⊢ ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
have coe_coe : (↑(x * y) : EReal)⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
Tactic: rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : ℝ
coe_coe : (↑(x * y) : EReal)⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
⊢ ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
have coe_coe₁ : (↑(x * y)⁻¹ : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
Tactic: rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : ℝ
coe_coe : (↑(x * y) : EReal)⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
coe_coe₁ : (↑(x * y)⁻¹ : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
⊢ ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
have coe_coe₂ : (↑(x⁻¹ * y⁻¹) : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
Tactic: rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : ℝ
coe_coe : (↑(x * y) : EReal)⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
coe_coe₁ : (↑(x * y)⁻¹ : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
coe_coe₂ : (↑(x⁻¹ * y⁻¹) : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
⊢ ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
have coe_coe₃ : (↑x⁻¹ : EReal) * (↑y⁻¹ : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
Tactic: rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]