Theorem: ToySnark.Vars.finsupp_eq_ext (FormalSnarksProject/SNARKs/ToySnark.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