σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : n = 0
⊢ ↑(coeff R 0) (φ * invOfUnit φ u) = ↑(coeff R 0) 1
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : n = 0
⊢ ↑(coeff R n) (φ * invOfUnit φ u) = ↑(coeff R n) 1
rw [H]
no goals
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : n = 0
⊢ ↑(coeff R 0) (φ * invOfUnit φ u) = ↑(coeff R 0) 1
simp [coeff_mul, support_single_ne_zero, h]
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ↑(coeff R n) (φ * invOfUnit φ u) = ↑(coeff R n) 1
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
⊢ ↑(coeff R n) (φ * invOfUnit φ u) = ↑(coeff R n) 1
have : ((0 : σ →₀ ℕ), n) ∈ n.antidiagonal := by rw [Finsupp.mem_antidiagonal, zero_add]
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
    x ∈ Finset.erase (antidiagonal n) (0, n) →
      ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (invOfUnit φ u) =
        if x.snd < (0, n).snd then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (invOfUnit φ u) else 0
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ↑(coeff R n) (φ * invOfUnit φ u) = ↑(coeff R n) 1
rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this,
  Finset.sum_insert (Finset.not_mem_erase _ _), coeff_zero_eq_constantCoeff_apply, h,
  coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ←
  Finset.insert_erase this, Finset.sum_insert (Finset.not_mem_erase _ _),
  Finset.insert_erase this, if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ←
  sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl]
case mk
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.erase (antidiagonal n) (0, n)
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, n).snd then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) else 0
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
    x ∈ Finset.erase (antidiagonal n) (0, n) →
      ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (invOfUnit φ u) =
        if x.snd < (0, n).snd then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (invOfUnit φ u) else 0
rintro ⟨i, j⟩ hij
case mk
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ≠ (0, n) ∧ (i, j).fst + (i, j).snd = n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, n).snd then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) else 0
case mk
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.erase (antidiagonal n) (0, n)
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, n).snd then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) else 0
rw [Finset.mem_erase, Finsupp.mem_antidiagonal] at hij
case mk.intro
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
h₁ : (i, j) ≠ (0, n)
h₂ : (i, j).fst + (i, j).snd = n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, n).snd then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) else 0
case mk
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ≠ (0, n) ∧ (i, j).fst + (i, j).snd = n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, n).snd then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) else 0
cases' hij with h₁ h₂
case mk.intro
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, (i, j).fst + (i, j).snd).snd then
      ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u)
    else 0
case mk.intro
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
h₁ : (i, j) ≠ (0, n)
h₂ : (i, j).fst + (i, j).snd = n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, n).snd then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) else 0
subst n
case mk.intro.hc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ (i, j).snd < (0, (i, j).fst + (i, j).snd).snd
case mk.intro
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u) =
    if (i, j).snd < (0, (i, j).fst + (i, j).snd).snd then
      ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (invOfUnit φ u)
    else 0
rw [if_pos]
case mk.intro.hc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ 0 + j < i + j
case mk.intro.hc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ (i, j).snd < (0, (i, j).fst + (i, j).snd).snd
suffices (0 : _) + j < i + j by simpa
case mk.intro.hc.bc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ 0 < i
case mk.intro.hc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ 0 + j < i + j
apply add_lt_add_right
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑0 i_1) (↑i i_1)

case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ ¬∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
case mk.intro.hc.bc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ 0 < i
constructor
no goals
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
H : ¬n = 0
⊢ (0, n) ∈ antidiagonal n
rw [Finsupp.mem_antidiagonal, zero_add]
no goals
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this✝ : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
this : 0 + j < i + j
⊢ (i, j).snd < (0, (i, j).fst + (i, j).snd).snd
simpa
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
s : σ
⊢ PartialOrder.toPreorder.1.1 (↑0 s) (↑i s)
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑0 i_1) (↑i i_1)
intro s
no goals
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
s : σ
⊢ PartialOrder.toPreorder.1.1 (↑0 s) (↑i s)
exact Nat.zero_le _
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
⊢ False
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
⊢ ¬∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
intro H
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
⊢ (i, j) = (0, (i, j).fst + (i, j).snd)
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
⊢ False
apply h₁
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
⊢ i = 0
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
⊢ (i, j) = (0, (i, j).fst + (i, j).snd)
suffices i = 0 by simp [this]
case mk.intro.hc.bc.right.h
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
s : σ
⊢ ↑i s = ↑0 s
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
⊢ i = 0
ext1 s
no goals
case mk.intro.hc.bc.right.h
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
s : σ
⊢ ↑i s = ↑0 s
exact Nat.eq_zero_of_le_zero (H s)
no goals
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑(constantCoeff σ R) φ = ↑u
i j : σ →₀ ℕ
H✝ : ¬(i, j).fst + (i, j).snd = 0
this✝ : (0, (i, j).fst + (i, j).snd) ∈ antidiagonal ((i, j).fst + (i, j).snd)
h₁ : (i, j) ≠ (0, (i, j).fst + (i, j).snd)
H : ∀ (i_1 : σ), PartialOrder.toPreorder.1.1 (↑i i_1) (↑0 i_1)
this : i = 0
⊢ (i, j) = (0, (i, j).fst + (i, j).snd)
simp [this]