Theorem: Weight.tw_inj (Weights/Weights.lean)

State before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
⊢ Function.Injective (tw n d)
Tactic:
intro j k h
State after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : tw n d j = tw n d k
⊢ j = k

State before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : tw n d j = tw n d k
⊢ j = k
Tactic:
simp only [tw, tw', ge_iff_le, nsmul_eq_mul, Pi.coe_nat, Nat.cast_tsub, Nat.cast_id,
  Nat.cast_one, Subtype.mk.injEq] at h
State after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1 =
    (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1
⊢ j = k

State before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1 =
    (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1
⊢ j = k
Tactic:
replace h := congr_fun h k
State after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1) k =
    ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1) k
⊢ j = k

State before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1) k =
    ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1) k
⊢ j = k
Tactic:
simp only [ge_iff_le, Pi.add_apply, Pi.mul_apply, ne_eq, Function.update_apply, zero_apply,
  mul_ite, mul_one, mul_zero, Function.update_same, add_right_inj, ite_eq_left_iff, if_true] at h
State after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : ¬k = j → False
⊢ j = k

State before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : ¬k = j → False
⊢ j = k
Tactic:
exact (of_not_not h).symm
State after:
no goals