Theorem: Nat.f_inj (PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean)

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
⊢ a = b
Tactic:
obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab
State after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a = b

State before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a = b
Tactic:
have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2 := by
  rw [finMulAntidiagonal_three a ha, hfab1, finMulAntidiagonal_three b hb]
State after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a = b

State before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a = b
Tactic:
have hab2 : a 2 = b 2 := by
  rw [← mul_right_inj' $ mul_ne_zero (ne_zero_of_mem_finMulAntidiagonal ha 0)
    (ne_zero_of_mem_finMulAntidiagonal ha 1)]
  exact hprods
State after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a = b

State before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a = b
Tactic:
have hab0 : a 0 = b 0 := by
  rw [hab2] at hfab2
  exact (mul_left_inj' $ ne_zero_of_mem_finMulAntidiagonal hb 2).mp hfab2;
State after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a = b

State before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a = b
Tactic:
have hab1 : a 1 = b 1 := by
  rw [hab0] at hfab1
  exact (mul_right_inj' $ ne_zero_of_mem_finMulAntidiagonal hb 0).mp hfab1;
State after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a = b

State before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a = b
Tactic:
funext i
State after:
case intro.h
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
⊢ a i = b i

State before:
case intro.h
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
⊢ a i = b i
Tactic:
fin_cases i <;> assumption
State after:
no goals

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
Tactic:
rw [finMulAntidiagonal_three a ha, hfab1, finMulAntidiagonal_three b hb]
State after:
no goals

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a 2 = b 2
Tactic:
rw [← mul_right_inj' $ mul_ne_zero (ne_zero_of_mem_finMulAntidiagonal ha 0)
  (ne_zero_of_mem_finMulAntidiagonal ha 1)]
State after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
Tactic:
exact hprods
State after:
no goals

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a 0 = b 0
Tactic:
rw [hab2] at hfab2
State after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * b 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a 0 = b 0

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * b 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a 0 = b 0
Tactic:
exact (mul_left_inj' $ ne_zero_of_mem_finMulAntidiagonal hb 2).mp hfab2
State after:
no goals

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a 1 = b 1
Tactic:
rw [hab0] at hfab1
State after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : b 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a 1 = b 1

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : b 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a 1 = b 1
Tactic:
exact (mul_right_inj' $ ne_zero_of_mem_finMulAntidiagonal hb 0).mp hfab1
State after:
no goals