Theorem: Weight.pair_w1 (Weights/Degree1.lean)

State before:
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
⊢ pair (w1 n) ↑a = if a = tw n 1 0 then 0 else 1
Tactic:
obtain ⟨k, ha⟩ := (testvecs1 n).2 a
State after:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ pair (w1 n) ↑a = if a = tw n 1 0 then 0 else 1

State before:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ pair (w1 n) ↑a = if a = tw n 1 0 then 0 else 1
Tactic:
rw [ha.symm, pair_tw, Nat.sub_self, zero_mul, zero_add, w1_apply]
State after:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1

State before:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
by_cases hk : k = 0
State after:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1

case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1

State before:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
simp only [hk, eq_self_iff_true]
State after:
no goals

State before:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
simp only [hk, if_false]
State after:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ 1 = if tw n 1 k = tw n 1 0 then 0 else 1

State before:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ 1 = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
split_ifs with h'
State after:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
⊢ False

case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : ¬tw n 1 k = tw n 1 0
⊢ 1 = 1

State before:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
⊢ False
Tactic:
have t := hk (tw_inj n 1 h')
State after:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
t : False
⊢ False

State before:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
t : False
⊢ False
Tactic:
tauto
State after:
no goals

State before:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : ¬tw n 1 k = tw n 1 0
⊢ 1 = 1
Tactic:
rfl
State after:
no goals