awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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]
-- 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)
neg_left₁ :
  -(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₃ : -HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType) =
  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)
neg_left₁ :
  -(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)
neg_left₃ :
  -HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
        ((sign : (a : EReal) → SignType) y : SignType) =
    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₄ : -HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType) =
  -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
⊢ (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
have top_zero : (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ 0) =
  HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
    ((sign : (a : EReal) → SignType) 0 : SignType)
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ 0) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) 0 : SignType)
⊢ (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
have top_top : (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ ⊤) =
  HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
    ((sign : (a : EReal) → SignType) ⊤ : SignType)
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ 0) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) 0 : SignType)
top_top :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ ⊤) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) ⊤ : SignType)
⊢ (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
have symm : ∀ {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)
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ 0) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) 0 : SignType)
top_top :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ ⊤) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) ⊤ : SignType)
symm :
  ∀ {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)
⊢ (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
have coe_coe : ∀ (x y : ℝ),
  (sign : (a : EReal) → SignType) ((↑x : EReal) * (↑y : EReal)) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
      ((sign : (a : EReal) → SignType) (↑y : EReal) : SignType)
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ 0) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) 0 : SignType)
top_top :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ ⊤) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) ⊤ : SignType)
symm :
  ∀ {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)
coe_coe :
  ∀ (x y : ℝ),
    (sign : (a : EReal) → SignType) ((↑x : EReal) * (↑y : EReal)) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
        ((sign : (a : EReal) → SignType) (↑y : EReal) : SignType)
⊢ (sign : (a : EReal) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
have top_pos : ∀ (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)
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
top_zero :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ 0) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) 0 : SignType)
top_top :
  (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ ⊤) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) ⊤ : SignType)
symm :
  ∀ {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)
coe_coe :
  ∀ (x y : ℝ),
    (sign : (a : EReal) → SignType) ((↑x : EReal) * (↑y : EReal)) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
        ((sign : (a : EReal) → SignType) (↑y : EReal) : SignType)
top_pos :
  ∀ (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)
⊢ (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 : ∀ {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)
Tactic: induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
⊢ (↑((sign : (a : EReal) → SignType) (↑x : EReal)) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
have rw : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
Tactic: rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
⊢ (↑((sign : (a : EReal) → SignType) (↑x : EReal)) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
have rw₁ : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑|x| : EReal) = (↑x : EReal)
Tactic: rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
rw₁ : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑|x| : EReal) = (↑x : EReal)
⊢ (↑((sign : (a : EReal) → SignType) (↑x : EReal)) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
have rw₂ : (↑(↑((sign : (a : ℝ) → SignType) x) : ℝ) : EReal) * (↑|x| : EReal) = (↑x : EReal)
Tactic: rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
rw₁ : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑|x| : EReal) = (↑x : EReal)
rw₂ : (↑(↑((sign : (a : ℝ) → SignType) x) : ℝ) : EReal) * (↑|x| : EReal) = (↑x : EReal)
⊢ (↑((sign : (a : EReal) → SignType) (↑x : EReal)) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
have rw₃ : (↑((↑((sign : (a : ℝ) → SignType) x) : ℝ) * |x|) : EReal) = (↑x : EReal)
Tactic: rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
rw : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
rw₁ : (↑((sign : (a : ℝ) → SignType) x) : EReal) * (↑|x| : EReal) = (↑x : EReal)
rw₂ : (↑(↑((sign : (a : ℝ) → SignType) x) : ℝ) : EReal) * (↑|x| : EReal) = (↑x : EReal)
rw₃ : (↑((↑((sign : (a : ℝ) → SignType) x) : ℝ) * |x|) : EReal) = (↑x : EReal)
⊢ (↑((sign : (a : EReal) → SignType) (↑x : EReal)) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)
have rw₄ : (↑x : EReal) = (↑x : EReal)
Tactic: rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
⊢ (↑x.abs : EReal) * (↑((sign : (a : EReal) → SignType) x) : EReal) = x
have rw : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) = x
Tactic: rw [EReal.mul_comm, EReal.sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
rw : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) = x
⊢ (↑x.abs : EReal) * (↑((sign : (a : EReal) → SignType) x) : EReal) = x
have rw₁ : x = x
Tactic: rw [EReal.mul_comm, EReal.sign_mul_abs]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
⊢ x.abs = y.abs ∧
      Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType) ↔
    x = y
have mp : x.abs = y.abs ∧
    Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType) →
  x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
mp :
  x.abs = y.abs ∧
      Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType) →
    x = y
⊢ x.abs = y.abs ∧
      Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType) ↔
    x = y
have mpr : x = y →
  x.abs = y.abs ∧
    Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
habs : x.abs = y.abs
hsign : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
⊢ x = y
have mp : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) = y
Tactic: rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
habs : x.abs = y.abs
hsign : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
mp : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) = y
⊢ x = y
have mp₁ : (↑((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, habs, hsign]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
habs : x.abs = y.abs
hsign : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
mp : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) = y
mp₁ :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) =
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
⊢ x = y
have mp₂ : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑y.abs : EReal) =
  (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
Tactic: rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
habs : x.abs = y.abs
hsign : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
mp : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) = y
mp₁ :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) =
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
mp₂ :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑y.abs : EReal) =
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
⊢ x = y
have mp₃ : (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal) =
  (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
Tactic: rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
⊢ x ≤ y ↔
    LT.lt (α := 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 : x ≤ y →
  LT.lt (α := 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
mp :
  x ≤ y →
    LT.lt (α := 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
⊢ x ≤ y ↔
    LT.lt (α := 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 mpr : LT.lt (α := 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 →
  x ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x y : EReal
h : x ≤ y
⊢ LT.lt (α := 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 : ∀
  (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
Tactic: refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)