case zero
F : Type ?u.41
α : Type u_1
β : Type ?u.47
γ : Type ?u.50
inst✝ : Monoid α
s✝¹ t : Set α
a✝¹ : α
m n : ℕ
a✝ : α
s✝ : Fin n → Set α
a : α
s : Fin Nat.zero → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a

case succ
F : Type ?u.41
α : Type u_1
β : Type ?u.47
γ : Type ?u.50
inst✝ : Monoid α
s✝¹ t : Set α
a✝¹ : α
m n✝ : ℕ
a✝ : α
s✝ : Fin n✝ → Set α
n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
a : α
s : Fin (Nat.succ n) → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
F : Type ?u.41
α : Type u_1
β : Type ?u.47
γ : Type ?u.50
inst✝ : Monoid α
s✝ t : Set α
a✝ : α
m n : ℕ
a : α
s : Fin n → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
induction' n with n ih generalizing a
no goals
case zero
F : Type ?u.41
α : Type u_1
β : Type ?u.47
γ : Type ?u.50
inst✝ : Monoid α
s✝¹ t : Set α
a✝¹ : α
m n : ℕ
a✝ : α
s✝ : Fin n → Set α
a : α
s : Fin Nat.zero → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
no goals
case succ
F : Type ?u.41
α : Type u_1
β : Type ?u.47
γ : Type ?u.50
inst✝ : Monoid α
s✝¹ t : Set α
a✝¹ : α
m n✝ : ℕ
a✝ : α
s✝ : Fin n✝ → Set α
n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
a : α
s : Fin (Nat.succ n) → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
  mem_mul, @ih, exists_and_left, exists_exists_eq_and, SetCoe.exists, exists_prop]