Theorem: Groth16TypeI.Vars.finsupp_eq_ext (FormalSnarksProject/SNARKs/Groth16.lean)

State before:
f g : Vars →₀ ℕ
⊢ f = g ↔ f α = g α ∧ 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 β ∧ f γ = g γ ∧ f δ = g δ

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

case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β ∧ 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 β ∧ 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 β ∧ f γ = g γ ∧ f δ = g δ

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

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

State before:
case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β ∧ 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 β ∧ f γ = g γ ∧ f δ = g δ
x : Vars
⊢ f x = g x

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