awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Div α
s : ι → Set α
t : Set α
⊢ (⋂ (i : ι), s i) / t ⊆ ⋂ (i : ι), s i / t

Tactic:
image2_iInter_subset_left ..

Premises used: Set.image2_iInter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Div α
s : Set α
t : ι → Set α
⊢ s / ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s / t i

Tactic:
image2_iInter_subset_right ..

Premises used: Set.image2_iInter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Div α
S : Set (Set α)
t : Set α
⊢ ⋂₀ S / t ⊆ ⋂ s ∈ S, s / t

Tactic:
image2_sInter_subset_left ..

Premises used: Set.image2_sInter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Div α
s : Set α
T : Set (Set α)
⊢ s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t

Tactic:
image2_sInter_subset_right ..

Premises used: Set.image2_sInter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Div α
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ (i : ι), ⋂ (j : κ i), s i j) / t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j / t

Tactic:
image2_iInter₂_subset_left ..

Premises used: Set.image2_iInter₂_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Div α
s : Set α
t : (i : ι) → κ i → Set α
⊢ s / ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s / t i j

Tactic:
image2_iInter₂_subset_right ..

Premises used: Set.image2_iInter₂_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ ⋃ a ∈ s, a • t = s • t

Tactic:
iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ ⋃ a ∈ t, (fun (x : α) ↦ x • a) '' s = s • t

Tactic:
iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : SMul α β
s : ι → Set α
t : Set β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Set α) (⋃ (i : ι), s i) t = ⋃ (i : ι), s i • t

Tactic:
image2_iUnion_left ..

Premises used: Set.image2_iUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : SMul α β
s : Set α
t : ι → Set β
⊢ HSMul.hSMul (β := Set β) s (⋃ (i : ι), t i) = ⋃ (i : ι), s • t i

Tactic:
image2_iUnion_right ..

Premises used: Set.image2_iUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
S : Set (Set α)
t : Set β
⊢ ⋃₀ S • t = ⋃ s ∈ S, s • t

Tactic:
image2_sUnion_left ..

Premises used: Set.image2_sUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
T : Set (Set β)
⊢ s • ⋃₀ T = ⋃ t ∈ T, s • t

Tactic:
image2_sUnion_right ..

Premises used: Set.image2_sUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SMul α β
s : (i : ι) → κ i → Set α
t : Set β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Set α) (⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), s i j • t

Tactic:
image2_iUnion₂_left ..

Premises used: Set.image2_iUnion₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SMul α β
s : Set α
t : (i : ι) → κ i → Set β
⊢ HSMul.hSMul (β := Set β) s (⋃ (i : ι), ⋃ (j : κ i), t i j) = ⋃ (i : ι), ⋃ (j : κ i), s • t i j

Tactic:
image2_iUnion₂_right ..

Premises used: Set.image2_iUnion₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : SMul α β
s : ι → Set α
t : Set β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Set α) (⋂ (i : ι), s i) t ⊆ ⋂ (i : ι), s i • t

Tactic:
image2_iInter_subset_left ..

Premises used: Set.image2_iInter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : SMul α β
s : Set α
t : ι → Set β
⊢ HSMul.hSMul (β := Set β) s (⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s • t i

Tactic:
image2_iInter_subset_right ..

Premises used: Set.image2_iInter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
S : Set (Set α)
t : Set β
⊢ ⋂₀ S • t ⊆ ⋂ s ∈ S, s • t

Tactic:
image2_sInter_left_subset S t (fun a x => a • x)

Premises used: HSMul.hSMul, Set.image2_sInter_left_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
T : Set (Set β)
⊢ s • ⋂₀ T ⊆ ⋂ t ∈ T, s • t

Tactic:
image2_sInter_right_subset s T (fun a x => a • x)

Premises used: Set.image2_sInter_right_subset, HSMul.hSMul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SMul α β
s : (i : ι) → κ i → Set α
t : Set β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Set α) (⋂ (i : ι), ⋂ (j : κ i), s i j) t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j • t

Tactic:
image2_iInter₂_subset_left ..

Premises used: Set.image2_iInter₂_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SMul α β
s : Set α
t : (i : ι) → κ i → Set β
⊢ HSMul.hSMul (β := Set β) s (⋂ (i : ι), ⋂ (j : κ i), t i j) ⊆ ⋂ (i : ι), ⋂ (j : κ i), s • t i j

Tactic:
image2_iInter₂_subset_right ..

Premises used: Set.image2_iInter₂_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : SMul α β
a : α
s : ι → Set β
⊢ HSMul.hSMul (β := Set β) a (⋃ (i : ι), s i) = ⋃ (i : ι), a • s i

Tactic:
image_iUnion

Premises used: Set.image_iUnion
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SMul α β
a : α
s : (i : ι) → κ i → Set β
⊢ HSMul.hSMul (β := Set β) a (⋃ (i : ι), ⋃ (j : κ i), s i j) = ⋃ (i : ι), ⋃ (j : κ i), a • s i j

Tactic:
image_iUnion₂ ..

Premises used: Set.image_iUnion₂
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
S : Set (Set β)
rw : HSMul.hSMul (β := Set β) a (⋃ i ∈ S, i) = ⋃ s ∈ S, a • s
rw₁ rw₂ : Eq.{u_3 + 1} (α := Set β) (⋃ i ∈ S, a • i) (⋃ s ∈ S, a • s)
⊢ a • ⋃₀ S = ⋃ s ∈ S, a • s

Tactic:
rw [sUnion_eq_biUnion, smul_set_iUnion₂]

Premises used: Set.smul_set_iUnion₂, Set.sUnion_eq_biUnion
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : SMul α β
a : α
t : ι → Set β
⊢ HSMul.hSMul (β := Set β) a (⋂ (i : ι), t i) ⊆ ⋂ (i : ι), a • t i

Tactic:
image_iInter_subset ..

Premises used: Set.image_iInter_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋂₀ S ⊆ ⋂ s ∈ S, a • s

Tactic:
image_sInter_subset ..

Premises used: Set.image_sInter_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SMul α β
a : α
t : (i : ι) → κ i → Set β
⊢ HSMul.hSMul (β := Set β) a (⋂ (i : ι), ⋂ (j : κ i), t i j) ⊆ ⋂ (i : ι), ⋂ (j : κ i), a • t i j

Tactic:
image_iInter₂_subset ..

Premises used: Set.image_iInter₂_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
⊢ ⋃ a ∈ s, (fun (x : β) ↦ a -ᵥ x) '' t = s -ᵥ t

Tactic:
iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
⊢ ⋃ a ∈ t, (fun (x : β) ↦ x -ᵥ a) '' s = s -ᵥ t

Tactic:
iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : VSub α β
s : ι → Set β
t : Set β
⊢ (⋃ (i : ι), s i) -ᵥ t = ⋃ (i : ι), s i -ᵥ t

Tactic:
image2_iUnion_left ..

Premises used: Set.image2_iUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : VSub α β
s : Set β
t : ι → Set β
⊢ s -ᵥ ⋃ (i : ι), t i = ⋃ (i : ι), s -ᵥ t i

Tactic:
image2_iUnion_right ..

Premises used: Set.image2_iUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
S : Set (Set β)
t : Set β
⊢ ⋃₀ S -ᵥ t = ⋃ s ∈ S, s -ᵥ t

Tactic:
image2_sUnion_left ..

Premises used: Set.image2_sUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s : Set β
T : Set (Set β)
⊢ s -ᵥ ⋃₀ T = ⋃ t ∈ T, s -ᵥ t

Tactic:
image2_sUnion_right ..

Premises used: Set.image2_sUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : VSub α β
s : (i : ι) → κ i → Set β
t : Set β
⊢ (⋃ (i : ι), ⋃ (j : κ i), s i j) -ᵥ t = ⋃ (i : ι), ⋃ (j : κ i), s i j -ᵥ t

Tactic:
image2_iUnion₂_left ..

Premises used: Set.image2_iUnion₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : VSub α β
s : Set β
t : (i : ι) → κ i → Set β
⊢ s -ᵥ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s -ᵥ t i j

Tactic:
image2_iUnion₂_right ..

Premises used: Set.image2_iUnion₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : VSub α β
s : ι → Set β
t : Set β
⊢ (⋂ (i : ι), s i) -ᵥ t ⊆ ⋂ (i : ι), s i -ᵥ t

Tactic:
image2_iInter_subset_left ..

Premises used: Set.image2_iInter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
inst : VSub α β
s : Set β
t : ι → Set β
⊢ s -ᵥ ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s -ᵥ t i

Tactic:
image2_iInter_subset_right ..

Premises used: Set.image2_iInter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
S : Set (Set β)
t : Set β
⊢ ⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t

Tactic:
image2_sInter_subset_left ..

Premises used: Set.image2_sInter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s : Set β
T : Set (Set β)
⊢ s -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t

Tactic:
image2_sInter_subset_right ..

Premises used: Set.image2_sInter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : VSub α β
s : (i : ι) → κ i → Set β
t : Set β
⊢ (⋂ (i : ι), ⋂ (j : κ i), s i j) -ᵥ t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j -ᵥ t

Tactic:
image2_iInter₂_subset_left ..

Premises used: Set.image2_iInter₂_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
β : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : VSub α β
s : Set β
t : (i : ι) → κ i → Set β
⊢ s -ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s -ᵥ t i j

Tactic:
image2_iInter₂_subset_right ..

Premises used: Set.image2_iInter₂_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
zero : Membership.mem (γ := Set α) (List.prod []) a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod [] = a
zero₁ : Membership.mem (γ := Set α) 1 a ↔ ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), 1 = a
zero₂ : Membership.mem (γ := Set α) 1 a ↔ 1 = a
zero₃ : Membership.mem (γ := Set α) 1 a ↔ a = 1
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a

Tactic:
simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]

Premises used: Set.mem_one, Fin.exists_fin_zero_pi, eq_comm, List.ofFn_zero, List.prod_nil
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
a : α
s : Fin n → Set α
zero :
  ∀ {a : α} {s : Fin 0 → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin 0) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (↑(f i) : α)) = a
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {a : α} {s : Fin n → Set α},
        a ∈ (List.ofFn s).prod ↔
          ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a)
    {a : α} {s : Fin (n + 1) → Set α},
    a ∈ (List.ofFn s).prod ↔
      ∃ (f : (i : Fin (n + 1)) → (↑(s i) : Type u_1)),
        List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (↑(f i) : α)) = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin n) → (↑(s i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a

Tactic:
induction n generalizing a with
  | zero => simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
  | succ n ih =>
    simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]

Premises used: Fin.cons_succ, Set.mem_one, Fin.exists_fin_succ_pi, Fin.exists_fin_zero_pi, SetCoe.exists, exists_prop, eq_comm, List.ofFn_zero, exists_exists_eq_and, List.prod_nil, List.prod_cons, List.ofFn_succ, Set.mem_mul, Fin.cons_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
l : List (Set α)
a : α
h :
  ∀ (n : ℕ) (f : Fin n → Set α),
    a ∈ (List.ofFn f).prod ↔
      ∃ (l' : List ((s : Set α) × (↑s : Type u_1))),
        List.prod
              (List.map
                (fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α))
                l') =
            a ∧
          List.map (Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1))) l' = List.ofFn f
⊢ a ∈ l.prod ↔
    ∃ (l' : List ((s : Set α) × (↑s : Type u_1))),
      List.prod
            (List.map
              (fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) l') =
          a ∧
        List.map (Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1))) l' = l

Tactic:
induction l using List.ofFnRec with | _ n f
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
a : α
n : ℕ
f : Fin n → Set α
h :
  (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) ↔
    ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
      List.prod
            (List.ofFn
              ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘
                x)) =
          a ∧
        Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f
⊢ a ∈ (List.ofFn f).prod ↔
    ∃ (l' : List ((s : Set α) × (↑s : Type u_1))),
      List.prod
            (List.map
              (fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) l') =
          a ∧
        List.map (Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1))) l' = List.ofFn f

Tactic:
simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, List.ofFn_inj',
    Sigma.mk.inj_iff, and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]

Premises used: Set.mem_prod_list_ofFn, heq_eq_eq, exists_and_left, and_left_comm, exists_eq_left, List.map_ofFn, List.exists_iff_exists_tuple, List.ofFn_inj', Sigma.mk.inj_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
a : α
n : ℕ
f : Fin n → Set α
h :
  (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) →
    ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
      List.prod
            (List.ofFn
              ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘
                x)) =
          a ∧
        Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f
h₁ :
  (∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
      List.prod
            (List.ofFn
              ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘
                x)) =
          a ∧
        Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f) →
    ∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a
⊢ (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) ↔
    ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
      List.prod
            (List.ofFn
              ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘
                x)) =
          a ∧
        Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → (↑(f i) : Type u_1)
⊢ ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
    Eq (α := α)
        (List.prod
          (List.ofFn
            ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘ x)))
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(fi i) : α))) ∧
      Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f

Tactic:
⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩

Premises used: And.intro, Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → (↑(f i) : Type u_1)
⊢ ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
    Eq (α := α)
        (List.prod
          (List.ofFn
            ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘ x)))
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(fi i) : α))) ∧
      Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f

Tactic:
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
fi : Fin n → (s : Set α) × (↑s : Type u_1)
⊢ ∃ (f : (i : Fin n) → (↑((Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ fi) i) : Type u_1)),
    Eq (α := α) (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)))
      (List.prod
        (List.ofFn
          ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘ fi)))

Tactic:
⟨fun i ↦ _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
n : ℕ
fi : Fin n → (s : Set α) × (↑s : Type u_1)
⊢ ∃ (f : (i : Fin n) → (↑((Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ fi) i) : Type u_1)),
    Eq (α := α) (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)))
      (List.prod
        (List.ofFn
          ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘ fi)))

Tactic:
exact ⟨fun i ↦ _, rfl⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Goal:
α : Type u_1
inst : Monoid α
s : Set α
a : α
n : ℕ
rw : a ∈ s ^ n ↔ Membership.mem (γ := Set α) (List.prod (List.ofFn (n := n) fun (a : Fin n) ↦ s)) a
rw₁ : a ∈ s ^ n ↔ a ∈ (List.replicate n s).prod
rw₂ rw₃ : a ∈ s ^ n ↔ a ∈ s ^ n
⊢ a ∈ s ^ n ↔ ∃ (f : Fin n → (↑s : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a

Tactic:
rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]

Premises used: Set.mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ image2 (fun (x1 : α) (x2 : β) ↦ x1 • x2) s t = s • t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ (fun (x : α × β) ↦ x.1 • x.2) '' s ×ˢ t = s • t

Tactic:
image_prod _

Premises used: Set.image_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
b : β
⊢ b ∈ s • t ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : β), y ∈ t ∧ x • y = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
a : α
b : β
⊢ a ∈ s → b ∈ t → a • b ∈ s • t

Tactic:
mem_image2_of_mem

Premises used: Set.Mem, Set.mem_image2_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
t : Set β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Set α) ∅ t = ∅

Tactic:
image2_empty_left

Premises used: Set.image2_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
⊢ HSMul.hSMul (β := Set β) s ∅ = ∅

Tactic:
image2_empty_right

Premises used: Set.image2_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ s • t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image2_eq_empty_iff

Premises used: Set.image2_eq_empty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image2_nonempty_iff

Premises used: Set.image2_nonempty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ s.Nonempty → t.Nonempty → (s • t).Nonempty

Tactic:
.image2

Premises used: Set.Nonempty.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ (s • t).Nonempty → s.Nonempty

Tactic:
.of_image2_left

Premises used: Set.Nonempty.of_image2_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ (s • t).Nonempty → t.Nonempty

Tactic:
.of_image2_right

Premises used: Set.Nonempty.of_image2_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
b : β
⊢ HSMul.hSMul (β := Set β) s {b} = (fun (x : α) ↦ x • b) '' s

Tactic:
image2_singleton_right

Premises used: Set.image2_singleton_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
t : Set β
a : α
⊢ HSMul.hSMul (α := Set α) {a} t = a • t

Tactic:
image2_singleton_left

Premises used: Set.image2_singleton_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
b : β
⊢ HSMul.hSMul (α := Set α) (β := Set β) {a} {b} = {a • b}

Tactic:
image2_singleton

Premises used: Set.image2_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂

Tactic:
image2_subset

Premises used: Set.image2_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t₁ t₂ : Set β
⊢ t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂

Tactic:
image2_subset_left

Premises used: Set.image2_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s₁ s₂ : Set α
t : Set β
⊢ s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t

Tactic:
image2_subset_right

Premises used: Set.image2_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t u : Set β
⊢ s • t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → a • b ∈ u

Tactic:
image2_subset_iff

Premises used: Set.image2_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t

Tactic:
image2_union_left

Premises used: Set.image2_union_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t₁ t₂ : Set β
⊢ s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂

Tactic:
image2_union_right

Premises used: Set.image2_union_right