Theorem: BabySNARK.Vars.finsupp_eq_ext (FormalSnarksProject/SNARKs/BabySnark.lean)

State before:
f g : Vars →₀ ℕ
⊢ f = g ↔ f β = g β ∧ f γ = g γ
Tactic:
rw [DFunLike.ext_iff]
State after:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f β = g β ∧ f γ = g γ

State before:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f β = g β ∧ f γ = g γ
Tactic:
constructor
State after:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f β = g β ∧ f γ = g γ

case mpr
f g : Vars →₀ ℕ
⊢ f β = g β ∧ f γ = g γ → ∀ (x : Vars), f x = g x

State before:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f β = g β ∧ f γ = g γ
Tactic:
intro h
State after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f β = g β ∧ f γ = g γ

State before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f β = g β ∧ f γ = g γ
Tactic:
simp_rw [h]
State after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True

State before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True
Tactic:
simp only [and_self]
State after:
no goals

State before:
case mpr
f g : Vars →₀ ℕ
⊢ f β = g β ∧ f γ = g γ → ∀ (x : Vars), f x = g x
Tactic:
intro h x
State after:
case mpr
f g : Vars →₀ ℕ
h : f β = g β ∧ f γ = g γ
x : Vars
⊢ f x = g x

State before:
case mpr
f g : Vars →₀ ℕ
h : f β = g β ∧ f γ = g γ
x : Vars
⊢ f x = g x
Tactic:
cases x <;> tauto
State after:
no goals