awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : ℝ
⊢ ((↑x : EReal) * (↑y : EReal)).abs = (↑x : EReal).abs * (↑y : EReal).abs

Tactic:
simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]

Premises used: ENNReal.ofReal_mul, abs_mul, EReal.coe_mul, EReal.abs_def, abs_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
h : 0 < x
top_pos : (↑x : EReal).abs ≠ 0
⊢ (⊤ * (↑x : EReal)).abs = EReal.abs ⊤ * (↑x : EReal).abs

Tactic:
rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]

Premises used: EReal.top_mul_coe_of_pos, EReal.abs_top, ENNReal.top_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
h : 0 < x
top_pos : ¬x = 0
⊢ (↑x : EReal).abs ≠ 0

Tactic:
rw [Ne, abs_eq_zero_iff, coe_eq_zero]

Premises used: EReal.abs_eq_zero_iff, Ne, EReal.coe_eq_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
h : 0 < x
⊢ ¬x = 0

Tactic:
h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
h : 0 < x
⊢ ¬x = 0

Tactic:
exact h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : (x * y).abs = x.abs * y.abs
neg_left : (-(x * y)).abs = (-x).abs * y.abs
neg_left₁ : (x * y).abs = (-x).abs * y.abs
neg_left₂ neg_left₃ neg_left₄ neg_left₅ : (x * y).abs = x.abs * y.abs
⊢ (-x * y).abs = (-x).abs * y.abs

Tactic:
rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]

Premises used: EReal.abs_neg, neg_mul
-- Module: Mathlib.Data.EReal.Inv
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
neg_left : ∀ {x y : EReal} (h : (x * y).abs = x.abs * y.abs), (-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]

Premises used: EReal.abs_neg, EReal.abs_eq_zero_iff, ENNReal.ofReal_mul, abs_mul, EReal.abs_top, Ne, MulZeroClass.mul_zero, ENNReal.top_mul, EReal.abs_zero, EReal.mul_comm, EReal.coe_eq_zero, mul_comm, EReal.coe_mul, EReal.abs_def, neg_mul, symm, abs_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType) (1 : SignType)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) ⊥ : SignType) (-1 : SignType)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) (↑x : EReal) : SignType)
    ((sign : (a : ℝ) → SignType) x : SignType)

Tactic:
simp only [sign, OrderHom.coe_mk, EReal.coe_pos, EReal.coe_neg']

Premises used: EReal.coe_neg', OrderHom.coe_mk, EReal.coe_pos, SignType.sign
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : SignType
zero : (↑(↑SignType.zero : ℝ) : EReal) = (↑SignType.zero : EReal)
neg : (↑(↑SignType.neg : ℝ) : EReal) = (↑SignType.neg : EReal)
pos : (↑(↑SignType.pos : ℝ) : EReal) = (↑SignType.pos : EReal)
⊢ (↑(↑x : ℝ) : EReal) = (↑x : EReal)

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (↑(↑zero : ℝ) : EReal) = (↑zero : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (↑(↑neg : ℝ) : EReal) = (↑neg : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (↑(↑pos : ℝ) : EReal) = (↑pos : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Inv
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)
rw₃ 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)

Tactic:
rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]

Premises used: EReal.coe_neg, EReal.sign_coe, Left.sign_neg
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ 0) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) 0 : SignType)

Tactic:
simp only [mul_zero, sign_zero]

Premises used: sign_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (sign : (a : EReal) → SignType) (HMul.hMul (α := EReal) ⊤ ⊤) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) ⊤ : SignType)
      ((sign : (a : EReal) → SignType) ⊤ : SignType)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Inv
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)
symm :
  (sign : (a : EReal) → SignType) (y * x) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : EReal) → SignType) x : SignType)
      ((sign : (a : EReal) → SignType) y : SignType)
symm₁ symm₂ symm₃ symm₄ :
  (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:
rwa [mul_comm, EReal.mul_comm]

Premises used: EReal.mul_comm, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
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:
simp only [← coe_mul, sign_coe, _root_.sign_mul]

Premises used: EReal.sign_coe, sign_mul, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Inv
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)
top_pos₃ top_pos₄ : Eq (α := SignType) 1 1
⊢ (sign : (a : EReal) → SignType) (⊤ * (↑x : EReal)) =
    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)]

Premises used: Iff.mpr, EReal.top_mul_coe_of_pos, sign_pos, EReal.sign_top, EReal.coe_pos, one_mul
-- Module: Mathlib.Data.EReal.Inv
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)
neg_left₄ 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)

Tactic:
rw [neg_mul, sign_neg, sign_neg, h, neg_mul]

Premises used: neg_mul, EReal.sign_neg
-- Module: Mathlib.Data.EReal.Inv
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)
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)
⊢ (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]

Premises used: sign_zero, EReal.sign_coe, sign_mul, MulZeroClass.mul_zero, EReal.sign_top, EReal.mul_comm, mul_comm, EReal.coe_mul, neg_mul, symm, EReal.sign_neg, one_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥) : EReal) = ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (↑((sign : (a : EReal) → SignType) ⊤) : EReal) * (↑(EReal.abs ⊤) : EReal) = ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
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)
rw₄ rw₅ : (↑x : EReal) = (↑x : EReal)
⊢ (↑((sign : (a : EReal) → SignType) (↑x : EReal)) : EReal) * (↑(↑x : EReal).abs : EReal) = (↑x : EReal)

Tactic:
rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]

Premises used: sign_mul_abs, EReal.sign_coe, EReal.coe_coe_sign, EReal.coe_mul, EReal.coe_abs
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
rw : (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) = x
rw₁ rw₂ : x = x
⊢ (↑x.abs : EReal) * (↑((sign : (a : EReal) → SignType) x) : EReal) = x

Tactic:
rw [EReal.mul_comm, EReal.sign_mul_abs]

Premises used: EReal.mul_comm, EReal.sign_mul_abs
-- Module: Mathlib.Data.EReal.Inv
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
mpr :
  x = y →
    x.abs = y.abs ∧
      Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
⊢ x.abs = y.abs ∧
      Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType) ↔
    x = y

Tactic:
constructor
-- Module: Mathlib.Data.EReal.Inv
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)
mp₃ mp₄ :
  (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal) =
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
⊢ x = y

Tactic:
rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]

Premises used: EReal.sign_mul_abs
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
⊢ x.abs = x.abs ∧
    Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) x : SignType)

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
⊢ x.abs = x.abs ∧
    Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) x : SignType)

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Data.EReal.Inv
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
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
⊢ 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
-- Module: Mathlib.Data.EReal.Inv
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

Tactic:
(sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)

Premises used: OrderHom.monotone, LE.le.lt_or_eq, Or.imp_right, SignType.sign
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : x ≤ y
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
⊢ 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:
refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)

Premises used: OrderHom.monotone, LE.le.lt_or_eq, Or.imp_right, SignType.sign
-- Module: Mathlib.Data.EReal.Inv
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) : 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

Premises used: EReal.sign_mul_abs
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : x ≤ y
hs : Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
h₁ :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
⊢ Eq (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)

Tactic:
rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h

Premises used: EReal.sign_mul_abs
-- Module: Mathlib.Data.EReal.Inv
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
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
⊢ (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:
cases hy : sign y

Premises used: DFunLike.coe, SignType.sign
-- Module: Mathlib.Data.EReal.Inv
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
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
⊢ (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:
rw [hs, hy] at h ⊢
-- Module: Mathlib.Data.EReal.Inv
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
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
⊢ (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:
rw [hs, hy] at h ⊢
-- Module: Mathlib.Data.EReal.Inv
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
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
⊢ (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:
rw [hs, hy] at h ⊢
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
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:
simp
-- Module: Mathlib.Data.EReal.Inv
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
mp : neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs

Tactic:
left