Theorem: GGPR.Vars.finsupp_eq_ext (FormalSnarksProject/SNARKs/GGPR.lean)

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

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

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

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

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

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

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

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