awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
a_pos : 0 < a
⊢ |a| = a

Tactic:
exact abs_of_pos a_pos

Premises used: abs_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥) : EReal)⁻¹ = ⊥⁻¹
top : (↑((sign : (a : EReal) → SignType) ⊤) : EReal) * (↑(EReal.abs ⊤) : EReal)⁻¹ = ⊤⁻¹
coe :
  ∀ (a : ℝ), (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs : EReal)⁻¹ = a⁻¹

Tactic:
induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · 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]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
      simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
      congr
      exact abs_of_pos a_pos

Premises used: SignType.coe_one, neg_one_mul, neg_neg, EReal.sign_coe, EReal.inv_neg, max_eq_left, SignType.coe_neg_one, OfNat.ofNat, EReal.coe_ennreal_ofReal, abs_nonneg, one_mul, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs : EReal)⁻¹ = a⁻¹

Tactic:
induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · 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]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
      simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
      congr
      exact abs_of_pos a_pos

Premises used: SignType.coe_one, neg_one_mul, neg_neg, EReal.sign_coe, EReal.inv_neg, max_eq_left, SignType.coe_neg_one, OfNat.ofNat, EReal.coe_ennreal_ofReal, abs_nonneg, one_mul, rfl, lt_trichotomy
-- 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₄ : -(↑(ENNReal.ofReal |a|)⁻¹ : 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₁₀ : (↑(-(-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, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]

Premises used: Iff.mpr, abs, abs_of_neg, EReal.coe_neg, abs_pos_of_neg, neg_one_mul, inv_neg, neg_neg, EReal.sign_coe, max_eq_left, SignType.coe_neg_one, ENNReal.ofReal_inv_of_pos, sign_neg, Inv.inv, inv_nonneg, EReal.abs_def, EReal.coe_inv, 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) = (↑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, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]

Premises used: Iff.mpr, SignType.coe_one, abs_pos_of_pos, sign_pos, EReal.sign_coe, max_eq_left, ENNReal.ofReal_inv_of_pos, inv_nonneg, EReal.abs_def, EReal.coe_inv, EReal.coe_ennreal_ofReal, abs_nonneg, one_mul
-- 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 : EReal
bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥)⁻¹ : EReal) = ⊥⁻¹
top : (↑((sign : (a : EReal) → SignType) ⊤) : EReal) * (↑(EReal.abs ⊤)⁻¹ : EReal) = ⊤⁻¹
coe :
  ∀ (a : ℝ), (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs⁻¹ : EReal) = a⁻¹

Tactic:
induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]
      congr
      exact abs_of_pos a_pos

Premises used: SignType.coe_one, neg_one_mul, inv_neg, neg_neg, EReal.sign_coe, SignType.coe_neg_one, OfNat.ofNat, EReal.coe_ennreal_ofReal, one_mul, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs⁻¹ : EReal) = a⁻¹

Tactic:
induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]
      congr
      exact abs_of_pos a_pos

Premises used: SignType.coe_one, neg_one_mul, inv_neg, neg_neg, EReal.sign_coe, SignType.coe_neg_one, OfNat.ofNat, EReal.coe_ennreal_ofReal, one_mul, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊥ ⊥⁻¹

Tactic:
inv_bot ▸ bot_lt_zero

Premises used: Eq.rec, EReal.bot_lt_zero, EReal.inv_bot, Eq.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊥ ⊥⁻¹

Tactic:
exact inv_bot ▸ bot_lt_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊥ ⊤⁻¹

Tactic:
EReal.inv_top ▸ bot_lt_zero

Premises used: Eq.rec, EReal.bot_lt_zero, EReal.inv_top, Eq.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊥ ⊤⁻¹

Tactic:
exact EReal.inv_top ▸ bot_lt_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ ⊥ < (↑x : EReal)⁻¹

Tactic:
(coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

Premises used: EReal.bot_lt_coe, Eq.rec, Inv.inv, EReal.coe_inv, Eq.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ ⊥ < (↑x : EReal)⁻¹

Tactic:
exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
bot : LT.lt (α := EReal) ⊥ ⊥⁻¹
top : LT.lt (α := EReal) ⊥ ⊤⁻¹
coe : ∀ (x : ℝ), ⊥ < (↑x : EReal)⁻¹
⊢ ⊥ < x⁻¹

Tactic:
cases x with
  | bot => exact inv_bot ▸ bot_lt_zero
  | top => exact EReal.inv_top ▸ bot_lt_zero
  | coe x => exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊥⁻¹ ⊤

Tactic:
inv_bot ▸ zero_lt_top

Premises used: Eq.rec, EReal.inv_bot, EReal.zero_lt_top, Eq.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊥⁻¹ ⊤

Tactic:
exact inv_bot ▸ zero_lt_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊤⁻¹ ⊤

Tactic:
EReal.inv_top ▸ zero_lt_top

Premises used: Eq.rec, EReal.inv_top, EReal.zero_lt_top, Eq.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
⊢ LT.lt (α := EReal) ⊤⁻¹ ⊤

Tactic:
exact EReal.inv_top ▸ zero_lt_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ (↑x : EReal)⁻¹ < ⊤

Tactic:
(coe_inv x).symm ▸ coe_lt_top (x⁻¹)

Premises used: Eq.rec, Inv.inv, EReal.coe_inv, Eq.symm, EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : ℝ
⊢ (↑x : EReal)⁻¹ < ⊤

Tactic:
exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)
-- Module: Mathlib.Data.EReal.Inv
Goal:
x : EReal
bot : LT.lt (α := EReal) ⊥⁻¹ ⊤
top : LT.lt (α := EReal) ⊤⁻¹ ⊤
coe : ∀ (x : ℝ), (↑x : EReal)⁻¹ < ⊤
⊢ x⁻¹ < ⊤

Tactic:
cases x with
  | bot => exact inv_bot ▸ zero_lt_top
  | top => exact EReal.inv_top ▸ zero_lt_top
  | coe x => exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)
-- Module: Mathlib.Data.EReal.Inv
Goal:
h : LE.le (α := EReal) 0 ⊥
⊢ LE.le (α := EReal) 0 ⊥⁻¹

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

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : 0 ≤ (↑a : EReal)
coe : 0 ≤ a
⊢ 0 ≤ (↑a : EReal)⁻¹

Tactic:
rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]

Premises used: EReal.coe_nonneg, inv_nonneg, EReal.coe_inv
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : 0 ≤ (↑a : EReal)
⊢ 0 ≤ a

Tactic:
EReal.coe_nonneg.1 h

Premises used: EReal.coe_nonneg, Iff.mp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : 0 ≤ (↑a : EReal)
⊢ 0 ≤ a

Tactic:
exact EReal.coe_nonneg.1 h

Premises used: EReal.coe_nonneg, Iff.mp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : 0 ≤ a
bot : ∀ (h : LE.le (α := EReal) 0 ⊥), LE.le (α := EReal) 0 ⊥⁻¹
top : ∀ (h : LE.le (α := EReal) 0 ⊤), LE.le (α := EReal) 0 ⊤⁻¹
coe : ∀ (a : ℝ) (h : 0 ≤ (↑a : EReal)), 0 ≤ (↑a : EReal)⁻¹
⊢ 0 ≤ a⁻¹

Tactic:
cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h

Premises used: EReal.coe_nonneg, inv_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h

Premises used: EReal.coe_nonneg, inv_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
h : LE.le (α := EReal) ⊥ 0
⊢ LE.le (α := EReal) ⊥⁻¹ 0

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

Tactic:
simp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : (↑a : EReal) ≤ 0
coe : a ≤ 0
⊢ (↑a : EReal)⁻¹ ≤ 0

Tactic:
rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]

Premises used: EReal.coe_nonpos, EReal.coe_inv, inv_nonpos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : (↑a : EReal) ≤ 0
⊢ a ≤ 0

Tactic:
EReal.coe_nonpos.1 h

Premises used: EReal.coe_nonpos, Iff.mp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : (↑a : EReal) ≤ 0
⊢ a ≤ 0

Tactic:
exact EReal.coe_nonpos.1 h

Premises used: EReal.coe_nonpos, Iff.mp
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : a ≤ 0
bot : ∀ (h : LE.le (α := EReal) ⊥ 0), LE.le (α := EReal) ⊥⁻¹ 0
top : ∀ (h : LE.le (α := EReal) ⊤ 0), LE.le (α := EReal) ⊤⁻¹ 0
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≤ 0), (↑a : EReal)⁻¹ ≤ 0
⊢ a⁻¹ ≤ 0

Tactic:
cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h

Premises used: EReal.coe_nonpos, inv_nonpos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : a ≤ 0
⊢ a⁻¹ ≤ 0

Tactic:
cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h

Premises used: EReal.coe_nonpos, inv_nonpos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : 0 < a
h' : a ≠ ⊤
⊢ a ≠ ⊤ ∧ a ≠ ⊥

Tactic:
⟨h', ne_bot_of_gt h⟩

Premises used: And.intro, ne_bot_of_gt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : 0 < a
h' : a ≠ ⊤
lift : ∀ (a : ℝ) (h : 0 < (↑a : EReal)) (h' : (↑a : EReal) ≠ ⊤), 0 < (↑a : EReal)⁻¹
⊢ 0 < a⁻¹

Tactic:
lift a to ℝ using ⟨h', ne_bot_of_gt h⟩
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : 0 < (↑a : EReal)
h' : (↑a : EReal) ≠ ⊤
norm_cast : ∀ (h : 0 < a), 0 < a⁻¹
⊢ 0 < (↑a⁻¹ : EReal)

Tactic:
norm_cast at *
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h' : ¬(↑a : EReal) = ⊤
h : 0 < a
⊢ 0 < a⁻¹

Tactic:
inv_pos_of_pos h

Premises used: inv_pos_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h' : ¬(↑a : EReal) = ⊤
h : 0 < a
⊢ 0 < a⁻¹

Tactic:
exact inv_pos_of_pos h

Premises used: inv_pos_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : a < 0
h' : a ≠ ⊥
⊢ a ≠ ⊤ ∧ a ≠ ⊥

Tactic:
⟨ne_top_of_lt h, h'⟩

Premises used: And.intro, ne_top_of_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : a < 0
h' : a ≠ ⊥
lift : ∀ (a : ℝ) (h : (↑a : EReal) < 0) (h' : (↑a : EReal) ≠ ⊥), (↑a : EReal)⁻¹ < 0
⊢ a⁻¹ < 0

Tactic:
lift a to ℝ using ⟨ne_top_of_lt h, h'⟩
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h : (↑a : EReal) < 0
h' : (↑a : EReal) ≠ ⊥
norm_cast : ∀ (h : a < 0), a⁻¹ < 0
⊢ (↑a⁻¹ : EReal) < 0

Tactic:
norm_cast at *
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h' : ¬(↑a : EReal) = ⊥
h : a < 0
⊢ a⁻¹ < 0

Tactic:
inv_lt_zero.2 h

Premises used: Iff.mpr, inv_lt_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : ℝ
h' : ¬(↑a : EReal) = ⊥
h : a < 0
⊢ a⁻¹ < 0

Tactic:
exact inv_lt_zero.2 h

Premises used: Iff.mpr, inv_lt_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
a_0 : Membership.mem (γ := Set EReal) (Ioi 0) a
b : EReal
b_0 : Membership.mem (γ := Set EReal) (Ioi 0) b
a_b : a < b
⊢ 0 < b

Tactic:
push _ ∈ _ at *
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
a_0 : Membership.mem (γ := Set EReal) (Ioi 0) a
b : EReal
b_0 : Membership.mem (γ := Set EReal) (Ioi 0) b
a_b : a < b
b_0₁ : 0 < b
⊢ 0 < a

Tactic:
push _ ∈ _ at *
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
a_b : a < b
b_0 : 0 < b
a_0 : 0 < a
⊢ a ≠ ⊤ ∧ a ≠ ⊥

Tactic:
⟨ne_top_of_lt a_b, ne_bot_of_gt a_0⟩

Premises used: And.intro, ne_top_of_lt, ne_bot_of_gt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
a_b : a < b
b_0 : 0 < b
a_0 : 0 < a
lift : ∀ (a : ℝ) (a_b : (↑a : EReal) < b) (a_0 : 0 < (↑a : EReal)), b⁻¹ < (↑a : EReal)⁻¹
⊢ b⁻¹ < a⁻¹

Tactic:
lift a to ℝ using ⟨ne_top_of_lt a_b, ne_bot_of_gt a_0⟩
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b_0 : LT.lt (α := EReal) 0 ⊤
a_b : (↑a : EReal) < ⊤
⊢ ⊤⁻¹ < (↑a : EReal)⁻¹

Tactic:
inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)

Premises used: Eq.rec, EReal.inv_top, EReal.coe_ne_top, Eq.symm, EReal.inv_pos_of_pos_ne_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b_0 : LT.lt (α := EReal) 0 ⊤
a_b : (↑a : EReal) < ⊤
⊢ ⊤⁻¹ < (↑a : EReal)⁻¹

Tactic:
exact inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b_0 : LT.lt (α := EReal) 0 ⊥
a_b : (↑a : EReal) < ⊥
⊢ ⊥⁻¹ < (↑a : EReal)⁻¹

Tactic:
(not_lt_bot b_0).rec

Premises used: not_lt_bot, Bot.bot, Inv.inv, LT.lt, False.rec, Real.toEReal
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b_0 : LT.lt (α := EReal) 0 ⊥
a_b : (↑a : EReal) < ⊥
⊢ ⊥⁻¹ < (↑a : EReal)⁻¹

Tactic:
exact (not_lt_bot b_0).rec
-- Module: Mathlib.Data.EReal.Inv
Goal:
b_1 : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b : ℝ
b_0 : 0 < (↑b : EReal)
a_b : (↑a : EReal) < (↑b : EReal)
rw : b⁻¹ < a⁻¹
⊢ (↑b : EReal)⁻¹ < (↑a : EReal)⁻¹

Tactic:
rw [← coe_inv a, ← coe_inv b, EReal.coe_lt_coe_iff]

Premises used: EReal.coe_inv, EReal.coe_lt_coe_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
b_1 : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b : ℝ
b_0 : 0 < (↑b : EReal)
a_b : (↑a : EReal) < (↑b : EReal)
⊢ b⁻¹ < a⁻¹

Tactic:
_root_.inv_strictAntiOn (EReal.coe_pos.1 a_0) (EReal.coe_pos.1 b_0)
      (EReal.coe_lt_coe_iff.1 a_b)

Premises used: inv_strictAntiOn, EReal.coe_pos, Iff.mp, EReal.coe_lt_coe_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
b_1 : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b : ℝ
b_0 : 0 < (↑b : EReal)
a_b : (↑a : EReal) < (↑b : EReal)
⊢ b⁻¹ < a⁻¹

Tactic:
exact _root_.inv_strictAntiOn (EReal.coe_pos.1 a_0) (EReal.coe_pos.1 b_0)
      (EReal.coe_lt_coe_iff.1 a_b)

Premises used: inv_strictAntiOn, Iff.mp, EReal.coe_lt_coe_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
b_0 : 0 < b
a : ℝ
a_b : (↑a : EReal) < b
a_0 : 0 < (↑a : EReal)
⊢ b⁻¹ < (↑a : EReal)⁻¹

Tactic:
match b with
  | ⊤ => exact inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)
  | ⊥ => exact (not_lt_bot b_0).rec
  | (b : ℝ) =>
    rw [← coe_inv a, ← coe_inv b, EReal.coe_lt_coe_iff]
    exact _root_.inv_strictAntiOn (EReal.coe_pos.1 a_0) (EReal.coe_pos.1 b_0)
      (EReal.coe_lt_coe_iff.1 a_b)
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
⊢ a / b = b⁻¹ * a

Tactic:
EReal.mul_comm a b⁻¹

Premises used: DivInvMonoid.div', Inv.inv, EReal.mul_comm, EReal.mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : ℝ
⊢ (↑(a / b) : EReal) = (↑a : EReal) / (↑b : EReal)

Tactic:
rfl

Premises used: WithBot.some, DivInvMonoid.div', EReal.mul, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Inv
Goal:
m n : ℕ
rw : (↑(m / n) : ℝ) ≤ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
⊢ (↑(m / n) : EReal) ≤ HDiv.hDiv (α := EReal) (↑m : EReal) (↑n : EReal)

Tactic:
rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_div,
    EReal.coe_le_coe_iff]

Premises used: EReal.coe_le_coe_iff, EReal.coe_coe_eq_natCast, EReal.coe_div
-- Module: Mathlib.Data.EReal.Inv
Goal:
m n : ℕ
⊢ (↑(m / n) : ℝ) ≤ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
Nat.cast_div_le

Premises used: Nat.cast_div_le
-- Module: Mathlib.Data.EReal.Inv
Goal:
m n : ℕ
⊢ (↑(m / n) : ℝ) ≤ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
exact Nat.cast_div_le

Premises used: Nat.cast_div_le
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
⊢ a / ⊥ = 0

Tactic:
inv_bot ▸ mul_zero a

Premises used: Eq.rec, MulZeroClass.mul_zero, EReal.inv_bot
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
⊢ a / ⊤ = 0

Tactic:
inv_top ▸ mul_zero a

Premises used: Eq.rec, MulZeroClass.mul_zero, EReal.inv_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
change : a * 0⁻¹ = 0
⊢ a / 0 = 0

Tactic:
change a * 0⁻¹ = 0
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
rw : a * 0 = 0
rw₁ rw₂ : Eq (α := EReal) 0 0
⊢ a * 0⁻¹ = 0

Tactic:
rw [inv_zero, mul_zero a]

Premises used: MulZeroClass.mul_zero, EReal.inv_zero
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
⊢ 0 / a = 0

Tactic:
zero_mul a⁻¹

Premises used: MulZeroClass.zero_mul, DivInvMonoid.div', Inv.inv, EReal.mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : 0 < a
h' : a ≠ ⊤
⊢ ⊤ / a = ⊤

Tactic:
top_mul_of_pos (inv_pos_of_pos_ne_top h h')

Premises used: EReal.top_mul_of_pos, DivInvMonoid.div', EReal.mul, EReal.inv_pos_of_pos_ne_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : a < 0
h' : a ≠ ⊥
⊢ ⊤ / a = ⊥

Tactic:
top_mul_of_neg (inv_neg_of_neg_ne_bot h h')

Premises used: DivInvMonoid.div', EReal.top_mul_of_neg, EReal.mul, EReal.inv_neg_of_neg_ne_bot
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : 0 < a
h' : a ≠ ⊤
⊢ ⊥ / a = ⊥

Tactic:
bot_mul_of_pos (inv_pos_of_pos_ne_top h h')

Premises used: DivInvMonoid.div', EReal.bot_mul_of_pos, EReal.mul, EReal.inv_pos_of_pos_ne_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h : a < 0
h' : a ≠ ⊥
⊢ ⊥ / a = ⊤

Tactic:
bot_mul_of_neg (inv_neg_of_neg_ne_bot h h')

Premises used: DivInvMonoid.div', EReal.mul, EReal.inv_neg_of_neg_ne_bot, EReal.bot_mul_of_neg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : a ≠ 0
rw : ∀ (h₃ : (↑a.toReal : EReal) ≠ 0), (↑a.toReal : EReal) / (↑a.toReal : EReal) = 1
⊢ a / a = 1

Tactic:
rw [← coe_toReal h₂ h₁] at h₃ ⊢

Premises used: EReal.coe_toReal
-- Module: Mathlib.Data.EReal.Inv
Goal:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : (↑a.toReal : EReal) ≠ 0
rw : (↑(a.toReal / a.toReal) : EReal) = 1
rw₁ : (↑1 : EReal) = 1
rw₂ rw₃ : Eq (α := EReal) 1 1
⊢ (↑a.toReal : EReal) / (↑a.toReal : EReal) = 1

Tactic:
rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]

Premises used: EReal.coe_ne_zero, Iff.mp, EReal.coe_one, EReal.coe_div, div_self
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
change : a * (b * c⁻¹) = a * b * c⁻¹
⊢ a * (b / c) = a * b / c

Tactic:
change a * (b * c⁻¹) = (a * b) * c⁻¹

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
rw rw₁ : a * (b * c⁻¹) = a * (b * c⁻¹)
⊢ a * (b * c⁻¹) = a * b * c⁻¹

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
rw : c * (a / b) = a * c / b
rw₁ : c * a / b = a * c / b
rw₂ rw₃ : a * c / b = a * c / b
⊢ a / b * c = a * c / b

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

Premises used: EReal.mul_div, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
rw : a * b / c = b * (a / c)
rw₁ : b * a / c = b * (a / c)
rw₂ rw₃ : b * (a / c) = b * (a / c)
⊢ a * (b / c) = b * (a / c)

Tactic:
rw [mul_div a b c, mul_comm a b, ← mul_div b a c]

Premises used: EReal.mul_div, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
change : a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹
⊢ a / b / c = a / (b * c)

Tactic:
change (a * b⁻¹) * c⁻¹ = a * (b * c)⁻¹

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
rw : a * (b⁻¹ * c⁻¹) = a * (b * c)⁻¹
rw₁ rw₂ : a * (b⁻¹ * c⁻¹) = a * (b⁻¹ * c⁻¹)
⊢ a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹

Tactic:
rw [mul_assoc a b⁻¹, mul_inv]

Premises used: mul_assoc, Inv.inv, EReal.mul_inv
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c d : EReal
rw : a / b * (c / d) = a * (c / (b * d))
rw₁ : a / b * (c / d) = a * (c / (d * b))
rw₂ : a / b * (c / d) = a * (c / d / b)
rw₃ : a / b * (c / d) = c / d * (a / b)
rw₄ rw₅ : c / d * (a / b) = c / d * (a / b)
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]

Premises used: HDiv.hDiv, EReal.mul_div, mul_comm, EReal.mul_div_left_comm, EReal.div_div
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
rw : b * (a / b) = a
rw₁ : a * (b / b) = a
rw₂ : a * 1 = a
rw₃ rw₄ : a = a
⊢ a / b * b = a

Tactic:
rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]

Premises used: HDiv.hDiv, EReal.div_self, mul_comm, EReal.mul_div_left_comm, mul_one
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
rw : a / b * b = a
rw₁ rw₂ : a = a
⊢ b * (a / b) = a

Tactic:
rw [mul_comm, div_mul_cancel h₁ h₂ h₃]

Premises used: mul_comm, EReal.div_mul_cancel
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
rw : a / (b * c) * c = a / b
rw₁ : a / b / c * c = a / b
rw₂ rw₃ : a / b = a / b
⊢ a * c / (b * c) = a / b

Tactic:
rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]

Premises used: HMul.hMul, EReal.div_mul_cancel, EReal.mul_div_right, EReal.div_div
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
⊢ c / b = a ↔ c = a * b

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
refine_1 : ∀ (h : c / b = a), c = a * b
refine_2 : ∀ (h : c = a * b), c / b = a
⊢ c / b = a ↔ c = a * b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩