Theorem: ENNReal.sub_right_eq_self (ForML/LpHoelder.lean)

State before:
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a ↔ b = 0
Tactic:
refine Iff.intro ?_ ?_
State after:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a → b = 0

case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a

State before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a → b = 0

case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Tactic:
. intro h
  suffices hba : b ≤ a
  . simpa [← ENNReal.sub_right_inj ha' hba]
  have hba : 0 < a - b
  . simpa [h, zero_lt_iff]
  simp at hba
  exact hba.le
State after:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a

State before:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Tactic:
. intro h
  simp [h]
State after:
no goals

State before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a → b = 0
Tactic:
intro h
State after:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b = 0

State before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b = 0
Tactic:
suffices hba : b ≤ a
State after:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b ≤ a
⊢ b = 0

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a

State before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b ≤ a
⊢ b = 0

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a
Tactic:
. simpa [← ENNReal.sub_right_inj ha' hba]
State after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a

State before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a
Tactic:
have hba : 0 < a - b
State after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ 0 < a - b

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a

State before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ 0 < a - b

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a
Tactic:
. simpa [h, zero_lt_iff]
State after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a

State before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a
Tactic:
simp at hba
State after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b < a
⊢ b ≤ a

State before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b < a
⊢ b ≤ a
Tactic:
exact hba.le
State after:
no goals

State before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b ≤ a
⊢ b = 0
Tactic:
simpa [← ENNReal.sub_right_inj ha' hba]
State after:
no goals

State before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ 0 < a - b
Tactic:
simpa [h, zero_lt_iff]
State after:
no goals

State before:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Tactic:
intro h
State after:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : b = 0
⊢ a - b = a

State before:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : b = 0
⊢ a - b = a
Tactic:
simp [h]
State after:
no goals