awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
have coe_coe₄ : (↑x : EReal)⁻¹ * (↑y⁻¹ : EReal) = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
Tactic: rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
have coe_coe₅ : (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
Tactic: rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
have neg_bot : ⊤⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
Tactic: rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
neg_bot : ⊤⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
have neg_bot₁ : 0 = (↑x : EReal)⁻¹ * ⊥⁻¹
Tactic: rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
neg_bot : ⊤⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
neg_bot₁ : 0 = (↑x : EReal)⁻¹ * ⊥⁻¹
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
have neg_bot₂ : 0 = (↑x : EReal)⁻¹ * 0
Tactic: rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
x : ℝ
x_neg : x < 0
neg_bot : ⊤⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
neg_bot₁ : 0 = (↑x : EReal)⁻¹ * ⊥⁻¹
neg_bot₂ : 0 = (↑x : EReal)⁻¹ * 0
⊢ ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
have neg_bot₃ : Eq (α := EReal) 0 0
Tactic: rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have top_top : (HMul.hMul (α := EReal) ⊤ ⊤)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊤⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
top_top : (HMul.hMul (α := EReal) ⊤ ⊤)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊤⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have top_zero : (HMul.hMul (α := EReal) ⊤ 0)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ 0⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
top_top : (HMul.hMul (α := EReal) ⊤ ⊤)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊤⁻¹
top_zero : (HMul.hMul (α := EReal) ⊤ 0)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ 0⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have top_bot : (HMul.hMul (α := EReal) ⊤ ⊥)⁻¹ = HMul.hMul (α := EReal) ⊤⁻¹ ⊥⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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) ⊤⁻¹ ⊥⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have zero_bot : (HMul.hMul (α := EReal) 0 ⊥)⁻¹ = HMul.hMul (α := EReal) 0⁻¹ ⊥⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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⁻¹ ⊥⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥)⁻¹ = HMul.hMul (α := EReal) ⊥⁻¹ ⊥⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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) ⊥⁻¹ ⊥⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have symm : ∀ {a b : EReal} (h : (a * b)⁻¹ = a⁻¹ * b⁻¹), (b * a)⁻¹ = b⁻¹ * a⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have top_pos : ∀ (x : ℝ) (x_pos : 0 < x), (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have top_neg : ∀ (x : ℝ) (x_neg : x < 0), (⊤ * (↑x : EReal))⁻¹ = ⊤⁻¹ * (↑x : EReal)⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have pos_bot : ∀ (x : ℝ) (x_pos : 0 < x), ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹ * ⊥⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal))⁻¹ = (↑x : EReal)⁻¹ * (↑y : EReal)⁻¹
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]
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
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)⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have neg_bot : ∀ (x : ℝ) (x_neg : x < 0), ((↑x : EReal) * ⊥)⁻¹ = (↑x : EReal)⁻¹ * ⊥⁻¹
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]
Cleared hypotheses: a, b
-- 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, ← 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)⁻¹
⊢ (↑((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, ← 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)⁻¹
⊢ (↑((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, ← 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)⁻¹
⊢ (↑((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, ← 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)⁻¹
⊢ (↑((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, ← 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)⁻¹
⊢ (↑((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, ← 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)⁻¹
⊢ (↑((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, ← 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)⁻¹
⊢ (↑((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)⁻¹
⊢ (↑((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]