awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
have coe₉ : (↑(- -a) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
have coe₁₀ : (↑a : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
a_pos : 0 < a
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
have coe : (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
Tactic: rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
a_pos : 0 < a
⊢ (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
have coe : (↑|a| : EReal)⁻¹ = (↑a : EReal)⁻¹
Tactic: simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
a_pos : 0 < a
⊢ (↑|a| : EReal)⁻¹ = (↑a : EReal)⁻¹
have coe : |a| = a
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs : EReal)⁻¹ = a⁻¹
have bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥) : EReal)⁻¹ = ⊥⁻¹
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥) : EReal)⁻¹ = ⊥⁻¹
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs : EReal)⁻¹ = a⁻¹
have top : (↑((sign : (a : EReal) → SignType) ⊤) : EReal) * (↑(EReal.abs ⊤) : EReal)⁻¹ = ⊤⁻¹
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥) : EReal)⁻¹ = ⊥⁻¹
top : (↑((sign : (a : EReal) → SignType) ⊤) : EReal) * (↑(EReal.abs ⊤) : EReal)⁻¹ = ⊤⁻¹
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs : EReal)⁻¹ = a⁻¹
have coe : ∀ (a : ℝ), (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs : EReal)⁻¹ = (↑a : EReal)⁻¹
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe : ∀ (a_neg : a < 0),
  (↑((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)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
coe :
  ∀ (a_neg : a < 0),
    (↑((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)⁻¹
have coe₁ : (↑((sign : (a : EReal) → SignType) (↑0 : EReal)) : EReal) * (↑(↑0 : EReal).abs⁻¹ : EReal) = (↑0 : EReal)⁻¹
Tactic: rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₂ : ∀ (a_pos : 0 < a),
  (↑((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)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
a_neg : a < 0
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe : (↑((sign : (a : ℝ) → SignType) a) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
a_neg : a < 0
coe : (↑((sign : (a : ℝ) → SignType) a) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₁ : (↑(-1) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₂ : -1 * (↑(↑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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₃ : -(↑(↑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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₄ : -(↑(ENNReal.ofReal |a|)⁻¹ : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₅ : -(↑(ENNReal.ofReal |a|⁻¹) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₆ : -(↑(max |a|⁻¹ 0) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₇ : -(↑|a|⁻¹ : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₈ : (↑(-|a|⁻¹) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₉ : (↑(-|a|⁻¹) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₁₀ : (↑(-(-a)⁻¹) : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₁₁ : (↑(- -a)⁻¹ : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe₁₂ : (↑a⁻¹ : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
a_pos : 0 < a
⊢ (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
have coe : (↑|a|⁻¹ : 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]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
a_pos : 0 < a
⊢ (↑|a|⁻¹ : EReal) = (↑a⁻¹ : EReal)
have coe : |a| = a
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs⁻¹ : EReal) = a⁻¹
have bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥)⁻¹ : EReal) = ⊥⁻¹
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥)⁻¹ : EReal) = ⊥⁻¹
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs⁻¹ : EReal) = a⁻¹
have top : (↑((sign : (a : EReal) → SignType) ⊤) : EReal) * (↑(EReal.abs ⊤)⁻¹ : EReal) = ⊤⁻¹
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
bot : (↑((sign : (a : EReal) → SignType) ⊥) : EReal) * (↑(EReal.abs ⊥)⁻¹ : EReal) = ⊥⁻¹
top : (↑((sign : (a : EReal) → SignType) ⊤) : EReal) * (↑(EReal.abs ⊤)⁻¹ : EReal) = ⊤⁻¹
⊢ (↑((sign : (a : EReal) → SignType) a) : EReal) * (↑a.abs⁻¹ : EReal) = a⁻¹
have coe : ∀ (a : ℝ), (↑((sign : (a : EReal) → SignType) (↑a : EReal)) : EReal) * (↑(↑a : EReal).abs⁻¹ : EReal) = (↑a : EReal)⁻¹
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
⊢ ⊥ < x⁻¹
have bot : LT.lt (α := EReal) ⊥ ⊥⁻¹
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⁻¹)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
bot : LT.lt (α := EReal) ⊥ ⊥⁻¹
⊢ ⊥ < x⁻¹
have top : LT.lt (α := EReal) ⊥ ⊤⁻¹
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⁻¹)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
bot : LT.lt (α := EReal) ⊥ ⊥⁻¹
top : LT.lt (α := EReal) ⊥ ⊤⁻¹
⊢ ⊥ < x⁻¹
have coe : ∀ (x : ℝ), ⊥ < (↑x : EReal)⁻¹
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⁻¹)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
⊢ x⁻¹ < ⊤
have bot : LT.lt (α := EReal) ⊥⁻¹ ⊤
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⁻¹)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
bot : LT.lt (α := EReal) ⊥⁻¹ ⊤
⊢ x⁻¹ < ⊤
have top : LT.lt (α := EReal) ⊤⁻¹ ⊤
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⁻¹)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : EReal
bot : LT.lt (α := EReal) ⊥⁻¹ ⊤
top : LT.lt (α := EReal) ⊤⁻¹ ⊤
⊢ x⁻¹ < ⊤
have coe : ∀ (x : ℝ), (↑x : EReal)⁻¹ < ⊤
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⁻¹)
Cleared hypotheses: x