Theorem: mergeBitRes_Bool_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₂
⊢ b₁ = b₂
Tactic:
have h₂ := (congrArg (getBit 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₂ : getBit i (mergeBitRes i b₁ p₁) = getBit i (mergeBitRes i b₂ p₂)
⊢ b₁ = b₂

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₂ : getBit i (mergeBitRes i b₁ p₁) = getBit i (mergeBitRes i b₂ p₂)
⊢ b₁ = b₂
Tactic:
simp only [getBit_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₂ : b₁ = b₂
⊢ b₁ = b₂

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₂ : b₁ = b₂
⊢ b₁ = b₂
Tactic:
exact h₂
State after:
no goals