case intro
y : PartENat
n x : ℕ
h : ↑x + y = ↑n
⊢ ↑x = ↑(n - Part.get y (_ : y.Dom))
x y : PartENat
n : ℕ
h : x + y = ↑n
⊢ x = ↑(n - Part.get y (_ : y.Dom))
lift x to ℕ using dom_of_le_natCast ((le_add_right le_rfl).trans_eq h)
case intro.intro
n x y : ℕ
h : ↑x + ↑y = ↑n
⊢ ↑x = ↑(n - Part.get ↑y (_ : (↑y).Dom))
case intro
y : PartENat
n x : ℕ
h : ↑x + y = ↑n
⊢ ↑x = ↑(n - Part.get y (_ : y.Dom))
lift y to ℕ using dom_of_le_natCast ((le_add_left le_rfl).trans_eq h)
case intro.intro
n x y : ℕ
h✝ : ↑x + ↑y = ↑n
h : x + y = n
⊢ ↑x = ↑(n - Part.get ↑y (_ : (↑y).Dom))
case intro.intro
n x y : ℕ
h : ↑x + ↑y = ↑n
⊢ ↑x = ↑(n - Part.get ↑y (_ : (↑y).Dom))
rw [← Nat.cast_add, natCast_inj] at h
no goals
case intro.intro
n x y : ℕ
h✝ : ↑x + ↑y = ↑n
h : x + y = n
⊢ ↑x = ↑(n - Part.get ↑y (_ : (↑y).Dom))
rw [get_natCast, natCast_inj, eq_tsub_of_add_eq h]