[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
induction' n with n ih generalizing a
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
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
[PROOFSTEP]
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]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n : ℕ
l : List (Set α)
a : α
⊢ a ∈ List.prod l ↔ ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = l
[PROOFSTEP]
induction' l using List.ofFnRec with n f
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ List.prod (List.ofFn f) ↔
    ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = List.ofFn f
[PROOFSTEP]
simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, Function.comp, List.ofFn_inj',
  Sigma.mk.inj_iff, and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) ↔
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f
[PROOFSTEP]
constructor
[GOAL]
case h.mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) →
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f
[PROOFSTEP]
rintro ⟨fi, rfl⟩
[GOAL]
case h.mp.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → ↑(f i)
⊢ ∃ x,
    List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = List.prod (List.ofFn fun i => ↑(fi i)) ∧
      (fun x_1 => (x x_1).fst) = f
[PROOFSTEP]
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩
[GOAL]
case h.mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f) →
    ∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a
[PROOFSTEP]
rintro ⟨fi, rfl, rfl⟩
[GOAL]
case h.mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = List.prod (List.ofFn fun x => ↑(fi x).snd)
[PROOFSTEP]
exact ⟨fun i ↦ _, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]
