awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
⊢ LE.le (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m ≤ n
have rw : (↑m : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
⊢ LE.le (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m ≤ n
have rw₁ : (↑(↑m : ℝ) : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
rw₁ : (↑(↑m : ℝ) : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
⊢ LE.le (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m ≤ n
have rw₂ : LE.le (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m ≤ n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
rw₁ : (↑(↑m : ℝ) : EReal) ≤ (↑(↑n : ℝ) : EReal) ↔ m ≤ n
rw₂ : LE.le (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m ≤ n
⊢ LE.le (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m ≤ n
have rw₃ : m ≤ n ↔ m ≤ n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
⊢ LT.lt (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m < n
have rw : (↑m : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
⊢ LT.lt (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m < n
have rw₁ : (↑(↑m : ℝ) : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
rw₁ : (↑(↑m : ℝ) : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
⊢ LT.lt (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m < n
have rw₂ : LT.lt (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m < n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑m : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
rw₁ : (↑(↑m : ℝ) : EReal) < (↑(↑n : ℝ) : EReal) ↔ m < n
rw₂ : LT.lt (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ m < n
⊢ LT.lt (α := EReal) (↑m : EReal) (↑n : EReal) ↔ m < n
have rw₃ : m < n ↔ m < n
Tactic: rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
⊢ (↑(m * n) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
have rw : (↑(↑(m * n) : ℝ) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
Tactic: rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑(↑(m * n) : ℝ) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
⊢ (↑(m * n) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
have rw₁ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑n : EReal)
Tactic: rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑(↑(m * n) : ℝ) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
rw₁ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑n : EReal)
⊢ (↑(m * n) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
have rw₂ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
Tactic: rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑(↑(m * n) : ℝ) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
rw₁ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑n : EReal)
rw₂ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
⊢ (↑(m * n) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
have rw₃ : (↑(HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
Tactic: rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
m n : ℕ
rw : (↑(↑(m * n) : ℝ) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
rw₁ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑n : EReal)
rw₂ : (↑(↑(m * n) : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
rw₃ : (↑(HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
⊢ (↑(m * n) : EReal) = HMul.hMul (α := EReal) (↑m : EReal) (↑n : EReal)
have rw₄ : (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal) = (↑(↑m : ℝ) : EReal) * (↑(↑n : ℝ) : EReal)
Tactic: rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x_1 : (↑{⊥, ⊤}ᶜ : Type)
x : EReal
hx : Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
⊢ (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) ⋯)
      ((fun (x : (↑{⊥, ⊤}ᶜ : Type)) ↦ (↑x : EReal).toReal)
        (Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) x hx)) =
    Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) x hx
have lift : x ≠ ⊤ ∧ x ≠ ⊥
Tactic: lift x to ℝ
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
x_1 : (↑{⊥, ⊤}ᶜ : Type)
x : EReal
hx : Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x
lift : x ≠ ⊤ ∧ x ≠ ⊥
⊢ (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) ⋯)
      ((fun (x : (↑{⊥, ⊤}ᶜ : Type)) ↦ (↑x : EReal).toReal)
        (Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) x hx)) =
    Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) x hx
have lift₁ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ (↑x : EReal)),
  (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) sorry)
      ((fun (x : (↑{⊥, ⊤}ᶜ : Type)) ↦ (↑x : EReal).toReal)
        (Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) hx)) =
    Subtype.mk (p := fun (x : EReal) ↦ Membership.mem (γ := Set EReal) {⊥, ⊤}ᶜ x) (↑x : EReal) hx
Tactic: lift x to ℝ
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
⊢ x.abs = 0 ↔ x = 0
have bot : EReal.abs ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
bot : EReal.abs ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0
⊢ x.abs = 0 ↔ x = 0
have coe : ∀ (a : ℝ), (↑a : EReal).abs = 0 ↔ (↑a : EReal) = 0
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
bot : EReal.abs ⊥ = 0 ↔ Eq (α := EReal) ⊥ 0
coe : ∀ (a : ℝ), (↑a : EReal).abs = 0 ↔ (↑a : EReal) = 0
⊢ x.abs = 0 ↔ x = 0
have top : EReal.abs ⊤ = 0 ↔ Eq (α := EReal) ⊤ 0
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
⊢ EReal.abs 0 = 0
have rw : Eq (α := EReal) 0 0
Tactic: rw [abs_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
⊢ (↑(↑x : EReal).abs : EReal) = (↑|x| : EReal)
have rw : (↑(↑((Real.nnabs : (a : ℝ) → NNReal) x) : ℝ≥0∞) : EReal) = (↑(↑((Real.nnabs : (a : ℝ) → NNReal) x) : ℝ) : EReal)
Tactic: rw [abs_def, ← Real.coe_nnabs, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
⊢ (-(↑x : EReal)).abs = (↑x : EReal).abs
have rw : (-(↑x : EReal)).abs = ENNReal.ofReal |x|
Tactic: rw [abs_def, ← coe_neg, abs_def, abs_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw : (-(↑x : EReal)).abs = ENNReal.ofReal |x|
⊢ (-(↑x : EReal)).abs = (↑x : EReal).abs
have rw₁ : (↑(-x) : EReal).abs = ENNReal.ofReal |x|
Tactic: rw [abs_def, ← coe_neg, abs_def, abs_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw : (-(↑x : EReal)).abs = ENNReal.ofReal |x|
rw₁ : (↑(-x) : EReal).abs = ENNReal.ofReal |x|
⊢ (-(↑x : EReal)).abs = (↑x : EReal).abs
have rw₂ : ENNReal.ofReal |(-x)| = ENNReal.ofReal |x|
Tactic: rw [abs_def, ← coe_neg, abs_def, abs_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw : (-(↑x : EReal)).abs = ENNReal.ofReal |x|
rw₁ : (↑(-x) : EReal).abs = ENNReal.ofReal |x|
rw₂ : ENNReal.ofReal |(-x)| = ENNReal.ofReal |x|
⊢ (-(↑x : EReal)).abs = (↑x : EReal).abs
have rw₃ : ENNReal.ofReal |x| = ENNReal.ofReal |x|
Tactic: rw [abs_def, ← coe_neg, abs_def, abs_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (x * y).abs = x.abs * y.abs
⊢ (y * x).abs = y.abs * x.abs
have symm : (y * x).abs = x.abs * y.abs
Tactic: rwa [mul_comm, EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
h : 0 < x
⊢ (⊤ * (↑x : EReal)).abs = EReal.abs ⊤ * (↑x : EReal).abs
have top_pos : (↑x : EReal).abs ≠ 0
Tactic: rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
h : 0 < x
⊢ (↑x : EReal).abs ≠ 0
have top_pos : ¬x = 0
Tactic: rw [Ne, abs_eq_zero_iff, coe_eq_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (x * y).abs = x.abs * y.abs
⊢ (-x * y).abs = (-x).abs * y.abs
have neg_left : (-(x * y)).abs = (-x).abs * y.abs
Tactic: rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : (x * y).abs = x.abs * y.abs
neg_left : (-(x * y)).abs = (-x).abs * y.abs
⊢ (-x * y).abs = (-x).abs * y.abs
have neg_left₁ : (x * y).abs = (-x).abs * y.abs
Tactic: rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
⊢ (x * y).abs = x.abs * y.abs
have top_zero : (HMul.hMul (α := EReal) ⊤ 0).abs = EReal.abs ⊤ * EReal.abs 0
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero : (HMul.hMul (α := EReal) ⊤ 0).abs = EReal.abs ⊤ * EReal.abs 0
⊢ (x * y).abs = x.abs * y.abs
have top_top : (HMul.hMul (α := EReal) ⊤ ⊤).abs = EReal.abs ⊤ * EReal.abs ⊤
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero : (HMul.hMul (α := EReal) ⊤ 0).abs = EReal.abs ⊤ * EReal.abs 0
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).abs = EReal.abs ⊤ * EReal.abs ⊤
⊢ (x * y).abs = x.abs * y.abs
have symm : ∀ {x y : EReal} (h : (x * y).abs = x.abs * y.abs), (y * x).abs = y.abs * x.abs
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero : (HMul.hMul (α := EReal) ⊤ 0).abs = EReal.abs ⊤ * EReal.abs 0
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).abs = EReal.abs ⊤ * EReal.abs ⊤
symm : ∀ {x y : EReal} (h : (x * y).abs = x.abs * y.abs), (y * x).abs = y.abs * x.abs
⊢ (x * y).abs = x.abs * y.abs
have coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).abs = (↑x : EReal).abs * (↑y : EReal).abs
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero : (HMul.hMul (α := EReal) ⊤ 0).abs = EReal.abs ⊤ * EReal.abs 0
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).abs = EReal.abs ⊤ * EReal.abs ⊤
symm : ∀ {x y : EReal} (h : (x * y).abs = x.abs * y.abs), (y * x).abs = y.abs * x.abs
coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).abs = (↑x : EReal).abs * (↑y : EReal).abs
⊢ (x * y).abs = x.abs * y.abs
have top_pos : ∀ (x : ℝ) (h : 0 < x), (⊤ * (↑x : EReal)).abs = EReal.abs ⊤ * (↑x : EReal).abs
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero : (HMul.hMul (α := EReal) ⊤ 0).abs = EReal.abs ⊤ * EReal.abs 0
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).abs = EReal.abs ⊤ * EReal.abs ⊤
symm : ∀ {x y : EReal} (h : (x * y).abs = x.abs * y.abs), (y * x).abs = y.abs * x.abs
coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).abs = (↑x : EReal).abs * (↑y : EReal).abs
top_pos : ∀ (x : ℝ) (h : 0 < x), (⊤ * (↑x : EReal)).abs = EReal.abs ⊤ * (↑x : EReal).abs
⊢ (x * y).abs = x.abs * y.abs
have neg_left : ∀ {x y : EReal} (h : (x * y).abs = x.abs * y.abs), (-x * y).abs = (-x).abs * y.abs
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : SignType
⊢ (↑(↑x : ℝ) : EReal) = (↑x : EReal)
have zero : (↑(↑zero : ℝ) : EReal) = (↑zero : EReal)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : SignType
zero : (↑(↑SignType.zero : ℝ) : EReal) = (↑SignType.zero : EReal)
⊢ (↑(↑x : ℝ) : EReal) = (↑x : EReal)
have neg : (↑(↑neg : ℝ) : EReal) = (↑neg : EReal)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : SignType
zero : (↑(↑SignType.zero : ℝ) : EReal) = (↑SignType.zero : EReal)
neg : (↑(↑SignType.neg : ℝ) : EReal) = (↑SignType.neg : EReal)
⊢ (↑(↑x : ℝ) : EReal) = (↑x : EReal)
have pos : (↑(↑pos : ℝ) : EReal) = (↑pos : EReal)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) (-(↑x : EReal)) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have rw : Eq (α := SignType) ((sign : (a : EReal) → SignType) (↑(-x) : EReal) : SignType)
  (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
Tactic: rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw :
  Eq (α := SignType) ((sign : (a : EReal) → SignType) (↑(-x) : EReal) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) (-(↑x : EReal)) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have rw₁ : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (-x) : SignType)
  (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
Tactic: rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw :
  Eq (α := SignType) ((sign : (a : EReal) → SignType) (↑(-x) : EReal) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
rw₁ :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (-x) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) (-(↑x : EReal)) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have rw₂ : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (-x) : SignType) (-(sign : (a : ℝ) → SignType) x : SignType)
Tactic: rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw :
  Eq (α := SignType) ((sign : (a : EReal) → SignType) (↑(-x) : EReal) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
rw₁ :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (-x) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
rw₂ : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (-x) : SignType) (-(sign : (a : ℝ) → SignType) x : SignType)
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) (-(↑x : EReal)) : SignType)
    (-(sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have rw₃ : Eq (α := SignType) (-(sign : (a : ℝ) → SignType) x : SignType) (-(sign : (a : ℝ) → SignType) x : SignType)
Tactic: rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
⊢ (sign : (a : EReal) → SignType) (y * x) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) y : SignType)
      ((sign : (a : EReal) → SignType) x : SignType)
have symm : (sign : (a : EReal) → SignType) (y * x) =
  HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
    ((sign : (a : EReal) → SignType) y : SignType)
Tactic: rwa [mul_comm, EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
h : 0 < x
⊢ (sign : (a : EReal) → SignType) (⊤ * (↑x : EReal)) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have top_pos : (sign : (a : EReal) → SignType) ⊤ =
  HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
    ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
Tactic: rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
h : 0 < x
top_pos :
  (sign : (a : EReal) → SignType) ⊤ =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
⊢ (sign : (a : EReal) → SignType) (⊤ * (↑x : EReal)) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have top_pos₁ : 1 = HMul.hMul (α := SignType) (β := SignType) (1 : SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
Tactic: rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
h : 0 < x
top_pos :
  (sign : (a : EReal) → SignType) ⊤ =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
top_pos₁ :
  1 = HMul.hMul (α := SignType) (β := SignType) (1 : SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
⊢ (sign : (a : EReal) → SignType) (⊤ * (↑x : EReal)) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have top_pos₂ : Eq (α := SignType) (1 : SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
Tactic: rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
h : 0 < x
top_pos :
  (sign : (a : EReal) → SignType) ⊤ =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
top_pos₁ :
  1 = HMul.hMul (α := SignType) (β := SignType) (1 : SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
top_pos₂ : Eq (α := SignType) (1 : SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
⊢ (sign : (a : EReal) → SignType) (⊤ * (↑x : EReal)) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
have top_pos₃ : Eq (α := SignType) 1 1
Tactic: rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
⊢ (sign : (a : EReal) → SignType) (-x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (-x) : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
have neg_left : (sign : (a : EReal) → SignType) (-(x * y)) =
  HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (-x) : SignType)
    ((sign : (a : EReal) → SignType) y : SignType)
Tactic: rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h :
  (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
neg_left :
  (sign : (a : EReal) → SignType) (-(x * y)) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (-x) : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
⊢ (sign : (a : EReal) → SignType) (-x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (-x) : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
have neg_left₁ : -(sign : (a : EReal) → SignType) (x * y) =
  HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (-x) : SignType)
    ((sign : (a : EReal) → SignType) y : SignType)
Tactic: rw [neg_mul, sign_neg, sign_neg, h, neg_mul]