Theorem: Lipmaa.Vars.finsupp_eq_ext (FormalSnarksProject/SNARKs/Lipmaa/Defs.lean)

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

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

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

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

State before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f y = g y
Tactic:
simp_rw [h]
State after:
no goals

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

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