awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs

Tactic:
simpa using h
-- Module: Mathlib.Data.EReal.Inv
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
mp : pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
⊢ pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
right
-- Module: Mathlib.Data.EReal.Inv
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
mp : pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
⊢ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
right
-- Module: Mathlib.Data.EReal.Inv
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 = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
simpa using h
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : LT.lt (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
⊢ x ≤ y

Tactic:
(sign.monotone.reflect_lt h).le

Premises used: OrderHom.monotone, Monotone.reflect_lt, LT.lt.le, SignType.sign
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : LT.lt (α := SignType) ((sign : (a : EReal) → SignType) x : SignType) ((sign : (a : EReal) → SignType) y : SignType)
⊢ x ≤ y

Tactic:
exact (sign.monotone.reflect_lt h).le

Premises used: OrderHom.monotone, Monotone.reflect_lt, LT.lt.le, SignType.sign
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : (sign : (a : EReal) → SignType) x = neg ∧ (sign : (a : EReal) → SignType) y = neg ∧ y.abs ≤ x.abs
mpr :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
⊢ x ≤ y

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

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

Tactic:
simp [h]
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : (sign : (a : EReal) → SignType) x = zero ∧ (sign : (a : EReal) → SignType) y = zero
mpr :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
⊢ x ≤ y

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

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

Tactic:
simp [h]
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : (sign : (a : EReal) → SignType) x = pos ∧ (sign : (a : EReal) → SignType) y = pos ∧ x.abs ≤ y.abs
mpr :
  (↑((sign : (a : EReal) → SignType) x) : EReal) * (↑x.abs : EReal) ≤
    (↑((sign : (a : EReal) → SignType) y) : EReal) * (↑y.abs : EReal)
⊢ x ≤ y

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

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

Tactic:
simp [h]
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y z : EReal
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)
⊢ x * y * z = x * (y * z)

Tactic:
rw [← sign_eq_and_abs_eq_iff_eq]

Premises used: EReal.sign_eq_and_abs_eq_iff_eq
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y z : EReal
⊢ (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:
simp only [mul_assoc, abs_mul, sign_mul, and_self_iff]

Premises used: mul_assoc, EReal.sign_mul, EReal.abs_mul, and_self_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
x0 : 0 < x
a b : EReal
h : a ≤ b
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
⊢ 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)

Tactic:
simp only [le_iff_sign, EReal.sign_mul, sign_pos x0, one_mul, EReal.abs_mul] at h ⊢

Premises used: sign_pos, EReal.sign_mul, EReal.abs_mul, EReal.le_iff_sign, one_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
x0 : 0 < x
a b : EReal
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:
h.imp_right <| Or.imp (And.imp_right <| And.imp_right (mul_le_mul_right · _)) <|
    Or.imp_right <| And.imp_right <| And.imp_right (mul_le_mul_right · _)

Premises used: EReal.abs, mul_le_mul_right, And.imp_right, Or.imp, Or.imp_right
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
x0 : 0 < x
a b : EReal
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:
exact h.imp_right <| Or.imp (And.imp_right <| And.imp_right (mul_le_mul_right · _)) <|
    Or.imp_right <| And.imp_right <| And.imp_right (mul_le_mul_right · _)

Premises used: mul_le_mul_right, And.imp_right, Or.imp, Or.imp_right
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ MulPosMono EReal

Tactic:
posMulMono_iff_mulPosMono.1 inferInstance

Premises used: inferInstance, posMulMono_iff_mulPosMono, Iff.mp
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ PosMulReflectLT EReal

Tactic:
PosMulMono.toPosMulReflectLT

Premises used: PosMulMono.toPosMulReflectLT
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ MulPosReflectLT EReal

Tactic:
MulPosMono.toMulPosReflectLT

Premises used: MulPosMono.toMulPosReflectLT
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
rw : -c * b ≤ -c * a
⊢ a * c ≤ b * c

Tactic:
rw [mul_comm a c, mul_comm b c, ← neg_le_neg_iff, ← neg_mul c b, ← neg_mul c a]

Premises used: EReal.neg_le_neg_iff, mul_comm, neg_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ 0 ≤ -c

Tactic:
rw [← neg_zero, EReal.le_neg] at hc

Premises used: EReal.le_neg, neg_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : b ≤ a
hc : 0 ≤ -c
ha : 0 ≤ -c
⊢ -c * b ≤ -c * a

Tactic:
gcongr
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
n : ℕ
⊢ (↑(x ^ n) : EReal) = (↑x : EReal) ^ n

Tactic:
map_pow (⟨⟨(↑), coe_one⟩, coe_mul⟩ : ℝ →* EReal) _ _

Premises used: WithBot.some, OneHom.mk, MonoidHom.mk, map_pow, EReal.coe_mul, EReal.coe_one, Real.toEReal
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ≥0∞
n : ℕ
⊢ (↑(x ^ n) : EReal) = (↑x : EReal) ^ n

Tactic:
map_pow (⟨⟨(↑), coe_ennreal_one⟩, coe_ennreal_mul⟩ : ℝ≥0∞ →* EReal) _ _

Premises used: OneHom.mk, MonoidHom.mk, map_pow, ENNReal.toEReal, EReal.coe_ennreal_one, EReal.coe_ennreal_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a_1 : EReal
n : ℕ
a : ℝ
ha : (↑a : EReal) ≠ ⊤
obtain : ∀ (m : ℕ) (an_m : a * (↑n : ℝ) ≤ (↑m : ℝ)), ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)

Tactic:
obtain ⟨m, an_m⟩ := exists_nat_ge (a * n)

Premises used: HMul.hMul, exists_nat_ge, Nat.cast
-- Module: Mathlib.Data.EReal.Inv
Goal:
a_1 : EReal
n : ℕ
a : ℝ
ha : (↑a : EReal) ≠ ⊤
m : ℕ
an_m : a * (↑n : ℝ) ≤ (↑m : ℝ)
h : (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)

Tactic:
use m
-- Module: Mathlib.Data.EReal.Inv
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)
h₂ : (↑(a * (↑n : ℝ)) : EReal) ≤ (↑(↑m : ℝ) : EReal)
h₃ h₄ h₅ h₆ : a * (↑n : ℝ) ≤ (↑m : ℝ)
⊢ (↑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]

Premises used: EReal.coe_le_coe_iff, EReal.coe_coe_eq_natCast, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
inl : ∀ (h : x ≤ y), min (-x) (-y) = -max x y
inr : ∀ (h : y ≤ x), min (-x) (-y) = -max x y
⊢ min (-x) (-y) = -max x y

Tactic:
rcases le_total x y with (h | h)

Premises used: le_total
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : x ≤ y
⊢ min (-x) (-y) = -max x y

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : y ≤ x
⊢ min (-x) (-y) = -max x y

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
inl : ∀ (h : x ≤ y), max (-x) (-y) = -min x y
inr : ∀ (h : y ≤ x), max (-x) (-y) = -min x y
⊢ max (-x) (-y) = -min x y

Tactic:
rcases le_total x y with (h | h)

Premises used: le_total
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : x ≤ y
⊢ max (-x) (-y) = -min x y

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Inv
Goal:
x y : EReal
h : y ≤ x
⊢ max (-x) (-y) = -min x y

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ Eq (α := EReal) ⊥⁻¹ 0

Tactic:
rfl

Premises used: EReal.inv, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ Eq (α := EReal) ⊤⁻¹ 0

Tactic:
rfl

Premises used: EReal.inv, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ (↑x⁻¹ : EReal) = (↑x : EReal)⁻¹

Tactic:
rfl

Premises used: WithBot.some, EReal.inv, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Inv
Goal:
rw : (↑0 : EReal) = 0
rw₁ rw₂ : Eq (α := EReal) 0 0
⊢ (↑0⁻¹ : EReal) = 0

Tactic:
rw [GroupWithZero.inv_zero, coe_zero]

Premises used: GroupWithZero.inv_zero, EReal.coe_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
nth_rw : (↑1 : EReal)⁻¹ = 1
nth_rw₁ : (↑1⁻¹ : EReal) = 1
nth_rw₂ : (↑1 : EReal) = 1
nth_rw₃ nth_rw₄ : Eq (α := EReal) 1 1
⊢ Eq (α := EReal) 1⁻¹ 1

Tactic:
nth_rw 1 [← coe_one, ← coe_inv 1, _root_.inv_one, coe_one]

Premises used: inv_one, EReal.coe_one, EReal.coe_inv, OfNat.ofNat
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
bot : Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)
coe : ∀ (a : ℝ), (-(↑a : EReal))⁻¹ = -(↑a : EReal)⁻¹
top : Eq (α := EReal) (-⊤)⁻¹ (-⊤⁻¹)
⊢ (-a)⁻¹ = -a⁻¹

Tactic:
induction a
-- Module: Mathlib.Data.EReal.Inv
Goal:
bot : Eq (α := EReal) ⊤⁻¹ (-⊥⁻¹)
bot₁ : Eq (α := EReal) 0 (-⊥⁻¹)
bot₂ : Eq (α := EReal) 0 (-0)
bot₃ bot₄ : Eq (α := EReal) 0 0
⊢ Eq (α := EReal) (-⊥)⁻¹ (-⊥⁻¹)

Tactic:
rw [neg_bot, inv_top, inv_bot, neg_zero]

Premises used: EReal.inv_top, EReal.inv_bot, neg_zero, EReal.neg_bot
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
⊢ (↑(-a)⁻¹ : EReal) = (↑(-a⁻¹) : EReal)

Tactic:
EReal.coe_eq_coe_iff.2 _root_.inv_neg

Premises used: Iff.mpr, inv_neg, EReal.coe_eq_coe_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
⊢ (↑(-a)⁻¹ : EReal) = (↑(-a⁻¹) : EReal)

Tactic:
exact EReal.coe_eq_coe_iff.2 _root_.inv_neg

Premises used: Iff.mpr, inv_neg, EReal.coe_eq_coe_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
top : Eq (α := EReal) ⊥⁻¹ (-⊤⁻¹)
top₁ : Eq (α := EReal) 0 (-⊤⁻¹)
top₂ : Eq (α := EReal) 0 (-0)
top₃ top₄ : Eq (α := EReal) 0 0
⊢ Eq (α := EReal) (-⊤)⁻¹ (-⊤⁻¹)

Tactic:
rw [neg_top, inv_bot, inv_top, neg_zero]

Premises used: EReal.inv_top, EReal.inv_bot, neg_zero, EReal.neg_top
-- Module: Mathlib.Data.EReal.Inv
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)
rw₃ rw₄ : (↑a.toReal : EReal) = (↑a.toReal : EReal)
⊢ a⁻¹⁻¹ = a

Tactic:
rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]

Premises used: EReal.coe_toReal, Inv.inv, inv_inv, EReal.toReal, EReal.coe_inv
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ ⊤)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊤⁻¹

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ 0)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ 0⁻¹

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ ⊥)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊥⁻¹

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (HMul.hMul (α := EReal) 0 ⊥)⁻¹ = HMul.hMul (α := EReal) 0⁻¹ ⊥⁻¹

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (HMul.hMul (α := EReal) ⊥ ⊥)⁻¹ = HMul.hMul (α := EReal) ⊥⁻¹ ⊥⁻¹

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
symm : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (b * a)⁻¹ = b⁻¹ * a⁻¹

Tactic:
rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]

Premises used: Inv.inv, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
h
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
exact h
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
x_pos : 0 < x
top_pos : ⊤⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
top_pos₁ : 0 = 0 * (↑x : EReal)⁻¹
top_pos₂ top_pos₃ : Eq (α := EReal) 0 0
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹

Tactic:
rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]

Premises used: Iff.mpr, EReal.top_mul_of_pos, MulZeroClass.zero_mul, EReal.inv_top, EReal.coe_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
x_neg : x < 0
top_neg : ⊥⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
top_neg₁ : 0 = ⊤⁻¹ * (↑x : EReal)⁻¹
top_neg₂ : 0 = 0 * (↑x : EReal)⁻¹
top_neg₃ top_neg₄ : Eq (α := EReal) 0 0
⊢ (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹

Tactic:
rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]

Premises used: Iff.mpr, MulZeroClass.zero_mul, EReal.coe_neg', EReal.inv_top, EReal.top_mul_of_neg, EReal.inv_bot
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
x_pos : 0 < x
pos_bot : ⊥⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
pos_bot₁ : 0 = (↑x : EReal)⁻¹ * 0
pos_bot₂ pos_bot₃ : Eq (α := EReal) 0 0
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹

Tactic:
rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]

Premises used: Iff.mpr, MulZeroClass.mul_zero, EReal.coe_pos, EReal.mul_bot_of_pos, EReal.inv_bot
-- Module: Mathlib.Data.EReal.Inv
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)⁻¹
coe_coe₃ : (↑x⁻¹ : EReal) * (↑y⁻¹ : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
coe_coe₄ : (↑x : EReal)⁻¹ * (↑y⁻¹ : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
coe_coe₅ coe_coe₆ : (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
⊢ ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹

Tactic:
rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]

Premises used: mul_inv, EReal.coe_mul, EReal.coe_inv
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
x_neg : x < 0
neg_bot : ⊤⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
neg_bot₁ : 0 = (↑x : EReal)⁻¹ * ⊥⁻¹
neg_bot₂ : 0 = (↑x : EReal)⁻¹ * 0
neg_bot₃ neg_bot₄ : Eq (α := EReal) 0 0
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹

Tactic:
rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]

Premises used: Iff.mpr, EReal.coe_neg', MulZeroClass.mul_zero, EReal.inv_top, EReal.inv_bot, EReal.mul_bot_of_neg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
top_top : (HMul.hMul (α := EReal) ⊤ ⊤)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊤⁻¹
top_zero : (HMul.hMul (α := EReal) ⊤ 0)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ 0⁻¹
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊥⁻¹
zero_bot : (HMul.hMul (α := EReal) 0 ⊥)⁻¹ = HMul.hMul (α := EReal) 0⁻¹ ⊥⁻¹
bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥)⁻¹ = HMul.hMul (α := EReal) ⊥⁻¹ ⊥⁻¹
symm : ∀ {a b : EReal} (h : (a * b)⁻¹ = a⁻¹ * b⁻¹), (b * a)⁻¹ = b⁻¹ * a⁻¹
top_pos : ∀ (x : ℝ) (x_pos : 0 < x), (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
top_neg : ∀ (x : ℝ) (x_neg : x < 0), (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
pos_bot : ∀ (x : ℝ) (x_pos : 0 < x), ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
neg_bot : ∀ (x : ℝ) (x_neg : x < 0), ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
induction a, b using EReal.induction₂_symm with
  | top_top | top_zero | top_bot | zero_bot | bot_bot => simp
  | @symm a b h => rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]; exact h
  | top_pos x x_pos => rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
  | top_neg x x_neg => rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
  | pos_bot x x_pos => rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
  | coe_coe x y => rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
  | neg_bot x x_neg => rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]

Premises used: mul_inv, MulZeroClass.zero_mul, MulZeroClass.mul_zero, Inv.inv, EReal.inv_top, EReal.inv_bot, mul_comm, EReal.coe_mul, EReal.coe_inv, symm, EReal.neg_bot
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
induction a, b using EReal.induction₂_symm with
  | top_top | top_zero | top_bot | zero_bot | bot_bot => simp
  | @symm a b h => rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]; exact h
  | top_pos x x_pos => rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
  | top_neg x x_neg => rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
  | pos_bot x x_pos => rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
  | coe_coe x y => rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
  | neg_bot x x_neg => rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]

Premises used: mul_inv, MulZeroClass.zero_mul, MulZeroClass.mul_zero, Inv.inv, EReal.inv_top, EReal.inv_bot, mul_comm, EReal.coe_mul, EReal.coe_inv, symm, EReal.neg_bot
-- 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:
a : ℝ
coe :
  ∀ (a_neg : a < 0),
    (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
coe₁ : (↑((sign : (a : EReal) → SignType) (↑0 : EReal)) : EReal) * (↑(↑0 : EReal).abs : EReal)⁻¹ = (↑0 : EReal)⁻¹
coe₂ :
  ∀ (a_pos : 0 < a),
    (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹

Tactic:
rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
a_neg : a < 0
coe : (↑((sign : (a : ℝ) → SignType) a) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
coe₁ : (↑(-1) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
coe₂ : -1 * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
coe₃ : -(↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
coe₄ : (-(↑(↑a : EReal).abs : EReal))⁻¹ = (↑a : EReal)⁻¹
coe₅ : (-(↑(ENNReal.ofReal |a|) : EReal))⁻¹ = (↑a : EReal)⁻¹
coe₆ : (-(↑(max |a| 0) : EReal))⁻¹ = (↑a : EReal)⁻¹
coe₇ : (-(↑|a| : EReal))⁻¹ = (↑a : EReal)⁻¹
coe₈ : (↑(-|a|) : EReal)⁻¹ = (↑a : EReal)⁻¹
coe₉ : (↑(- -a) : EReal)⁻¹ = (↑a : EReal)⁻¹
coe₁₀ coe₁₁ : (↑a : EReal)⁻¹ = (↑a : EReal)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹

Tactic:
rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, ← inv_neg, abs_def a,
        coe_ennreal_ofReal, max_eq_left (abs_nonneg a), ← coe_neg |a|, abs_of_neg a_neg, neg_neg]

Premises used: abs, abs_of_neg, EReal.coe_neg, neg_one_mul, neg_neg, EReal.sign_coe, EReal.inv_neg, max_eq_left, SignType.coe_neg_one, sign_neg, EReal.abs_def, EReal.coe_ennreal_ofReal, abs_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ (↑((sign : (a : EReal) → SignType) (↑0 : EReal)) : EReal) * (↑(↑0 : EReal).abs : EReal)⁻¹ = (↑0 : EReal)⁻¹

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
a_pos : 0 < a
coe : (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹

Tactic:
rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]

Premises used: SignType.coe_one, sign_pos, EReal.sign_coe, one_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
a_pos : 0 < a
coe : (↑|a| : EReal)⁻¹ = (↑a : EReal)⁻¹
⊢ (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹

Tactic:
simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]

Premises used: max_eq_left, EReal.abs_def, EReal.coe_ennreal_ofReal, abs_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
a_pos : 0 < a
coe : |a| = a
⊢ (↑|a| : EReal)⁻¹ = (↑a : EReal)⁻¹

Tactic:
congr
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
a_pos : 0 < a
⊢ |a| = a

Tactic:
abs_of_pos a_pos

Premises used: abs_of_pos