Theorem: mergeBitRes_Fin_inj (Controlbits/BitResiduum.lean)

State before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
⊢ p₁ = p₂
Tactic:
have h₂ := (congrArg (getRes i) h)
State after:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : getRes i (mergeBitRes i b₁ p₁) = getRes i (mergeBitRes i b₂ p₂)
⊢ p₁ = p₂

State before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : getRes i (mergeBitRes i b₁ p₁) = getRes i (mergeBitRes i b₂ p₂)
⊢ p₁ = p₂
Tactic:
simp_rw [getRes_mergeBitRes] at h₂
State after:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : p₁ = p₂
⊢ p₁ = p₂

State before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : p₁ = p₂
⊢ p₁ = p₂
Tactic:
exact h₂
State after:
no goals