awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
h : ∀ (x : α), z ∈ s x → w ∈ t x → (∃ (i : α), z ∈ s i) ∧ ∃ (i : α), w ∈ t i
h₁ : ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ (i : α), z ∈ s i ∧ w ∈ t i
⊢ (∀ (x : α), z ∈ s x → w ∈ t x → (∃ (i : α), z ∈ s i) ∧ ∃ (i : α), w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ (i : α), z ∈ s i ∧ w ∈ t i

Tactic:
constructor
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ (i : α), z ∈ s i) ∧ ∃ (i : α), w ∈ t i

Tactic:
⟨⟨x, hz⟩, x, hw⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ (i : α), z ∈ s i) ∧ ∃ (i : α), w ∈ t i

Tactic:
exact ⟨⟨x, hz⟩, x, hw⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
hw : w ∈ t x'
⊢ ∃ (i : α), z ∈ s i ∧ w ∈ t i

Tactic:
⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩

Premises used: le_sup_left, le_sup_right, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
hw : w ∈ t x'
⊢ ∃ (i : α), z ∈ s i ∧ w ∈ t i

Tactic:
exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
h :
  ∀ (fst : γ) (snd : δ),
    Membership.mem (γ := Set (γ × δ)) (⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2) (fst, snd) ↔
      (fst, snd) ∈ SProd.sprod (α := Set γ) (β := Set δ) (⋃ x ∈ s, f x) (⋃ x ∈ t, g x)
⊢ ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = SProd.sprod (α := Set γ) (β := Set δ) (⋃ x ∈ s, f x) (⋃ x ∈ t, g x)

Tactic:
ext ⟨_, _⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst : γ
snd : δ
h : (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) ↔ (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
⊢ Membership.mem (γ := Set (γ × δ)) (⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2) (fst, snd) ↔
    (fst, snd) ∈ SProd.sprod (α := Set γ) (β := Set δ) (⋃ x ∈ s, f x) (⋃ x ∈ t, g x)

Tactic:
simp only [mem_iUnion, mem_prod, exists_prop, Prod.exists]

Premises used: Set.mem_iUnion, exists_prop, Set.mem_prod, Prod.exists
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set β
t : Set γ
f : β × γ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ s ×ˢ t, f x) (⋃ i ∈ s, ⋃ j ∈ t, f (i, j))

Tactic:
biSup_prod

Premises used: biSup_prod, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
⊢ ⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
subset_iInter₂ fun x hx _ hy => ⟨hy.1 x.1 hx.1, hy.2 x.2 hx.2⟩

Premises used: Set.subset_iInter₂, Prod.fst, And.right, And.left, And.intro, Prod.snd
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hS : S.Nonempty
hT : T.Nonempty
obtain : ∀ (s₁ : Set α) (h₁ : s₁ ∈ S), ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
obtain ⟨s₁, h₁⟩ := hS
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hT : T.Nonempty
s₁ : Set α
h₁ : s₁ ∈ S
obtain : ∀ (s₂ : Set β) (h₂ : s₂ ∈ T), ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
obtain ⟨s₂, h₂⟩ := hT
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_

Premises used: Set.Subset.antisymm, Set.sInter_prod_sInter_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
refine : ∀ (x : α × β) (hx : Membership.mem (γ := Set (α × β)) (⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2) x), x ∈ ⋂₀ S ×ˢ ⋂₀ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
refine Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_

Premises used: Set.Subset.antisymm, Set.sInter_prod_sInter_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : Membership.mem (γ := Set (α × β)) (⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2) x
⊢ ∀ (i : Prod.{u_1, u_2} (Set α) (Set β)) (j : i ∈ S ×ˢ T), x ∈ i.1 ×ˢ i.2

Tactic:
rw [mem_iInter₂] at hx

Premises used: Set.mem_iInter₂
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ (i : Prod.{u_1, u_2} (Set α) (Set β)) (j : i ∈ S ×ˢ T), x ∈ i.1 ×ˢ i.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T

Tactic:
⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩

Premises used: Set.Mem, setOf, Set.prod, Prod.mk, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ (i : Prod.{u_1, u_2} (Set α) (Set β)) (j : i ∈ S ×ˢ T), x ∈ i.1 ×ˢ i.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T

Tactic:
exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
rw : Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (β := Set (Set β)) S {t}, r.1 ×ˢ r.2) (⋂ s ∈ S, s ×ˢ t)
⊢ ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t

Tactic:
rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]

Premises used: Set.singleton_nonempty, Set.sInter_prod_sInter, Set.sInter_singleton
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
simp_rw :
  Eq (α := Set (α × β))
    (⋂ (r : Prod.{u_1, u_2} (Set α) (Set β)),
      ⋂ (_ : Membership.mem (γ := Set (Prod.{u_1, u_2} (Set α) (Set β))) ((fun (a : Set α) ↦ (a, t)) '' S) r),
        r.1 ×ˢ r.2)
    (⋂ s ∈ S, s ×ˢ t)
simp_rw₁ :
  Eq (α := Set (α × β)) (⋂ (r : Prod.{u_1, u_2} (Set α) (Set β)), ⋂ (_ : ∃ x ∈ S, (x, t) = r), r.1 ×ˢ r.2)
    (⋂ s ∈ S, s ×ˢ t)
simp_rw₂ :
  Eq (α := Set (α × β)) (⋂ (r : Prod.{u_1, u_2} (Set α) (Set β)), ⋂ (i : Set α), ⋂ (_ : i ∈ S ∧ (i, t) = r), r.1 ×ˢ r.2)
    (⋂ s ∈ S, s ×ˢ t)
simp_rw₃ :
  Eq (α := Set (α × β)) (⋂ y ∈ S, ⋂ (x : Prod.{u_1, u_2} (Set α) (Set β)), ⋂ (_ : (y, t) = x), x.1 ×ˢ x.2)
    (⋂ s ∈ S, s ×ˢ t)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (β := Set (Set β)) S {t}, r.1 ×ˢ r.2) (⋂ s ∈ S, s ×ˢ t)

Tactic:
simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

Premises used: Set.iInter_iInter_eq_right, Set.mem_image, Set.prod_singleton, Set.iInter_exists, Set.biInter_and'
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
rw : Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (α := Set (Set α)) {s} T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)
⊢ s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t

Tactic:
rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]

Premises used: Set.singleton_nonempty, Set.sInter_prod_sInter, Set.sInter_singleton
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
simp_rw : Eq (α := Set (α × β)) (⋂ r ∈ Prod.mk s '' T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)
simp_rw₁ :
  Eq (α := Set (α × β)) (⋂ (r : Prod.{u_1, u_2} (Set α) (Set β)), ⋂ (_ : ∃ x ∈ T, (s, x) = r), r.1 ×ˢ r.2)
    (⋂ t ∈ T, s ×ˢ t)
simp_rw₂ :
  Eq (α := Set (α × β)) (⋂ (r : Prod.{u_1, u_2} (Set α) (Set β)), ⋂ (i : Set β), ⋂ (_ : i ∈ T ∧ (s, i) = r), r.1 ×ˢ r.2)
    (⋂ t ∈ T, s ×ˢ t)
simp_rw₃ :
  Eq (α := Set (α × β)) (⋂ y ∈ T, ⋂ (x : Prod.{u_1, u_2} (Set α) (Set β)), ⋂ (_ : (s, y) = x), x.1 ×ˢ x.2)
    (⋂ t ∈ T, s ×ˢ t)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (α := Set (Set α)) {s} T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)

Tactic:
simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

Premises used: Set.iInter_iInter_eq_right, Set.mem_image, Set.singleton_prod, Set.iInter_exists, Set.biInter_and'
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
h :
  ∀ (x : α × β),
    x ∈ SProd.sprod (β := Set β) s (⋂ (i : ι), t i) ↔ Membership.mem (γ := Set (α × β)) (⋂ (i : ι), s ×ˢ t i) x
⊢ SProd.sprod (β := Set β) s (⋂ (i : ι), t i) = ⋂ (i : ι), s ×ˢ t i

Tactic:
ext x
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
h : (x.1 ∈ s ∧ ∀ (i : ι), x.2 ∈ t i) ↔ ∀ (i : ι), x.1 ∈ s ∧ x.2 ∈ t i
⊢ x ∈ SProd.sprod (β := Set β) s (⋂ (i : ι), t i) ↔ Membership.mem (γ := Set (α × β)) (⋂ (i : ι), s ×ˢ t i) x

Tactic:
simp only [mem_prod, mem_iInter]

Premises used: Set.mem_iInter, Set.mem_prod
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ (x.1 ∈ s ∧ ∀ (i : ι), x.2 ∈ t i) ↔ ∀ (i : ι), x.1 ∈ s ∧ x.2 ∈ t i

Tactic:
⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩

Premises used: Nonempty.some, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ (x.1 ∈ s ∧ ∀ (i : ι), x.2 ∈ t i) ↔ ∀ (i : ι), x.1 ∈ s ∧ x.2 ∈ t i

Tactic:
exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
h : ∀ (x : γ), x ∈ image2 f s t ↔ Membership.mem (γ := Set γ) (⋃ i ∈ s, ⋃ j ∈ t, {f i j}) x
⊢ image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
x : γ
⊢ x ∈ image2 f s t ↔ Membership.mem (γ := Set γ) (⋃ i ∈ s, ⋃ j ∈ t, {f i j}) x

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ a ∈ s, f a '' t = image2 f s t

Tactic:
simp only [image2_eq_iUnion, image_eq_iUnion]

Premises used: Set.image_eq_iUnion, Set.image2_eq_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
rw : Eq.{u_3 + 1} (α := Set γ) (⋃ b ∈ t, (fun (x : α) ↦ f x b) '' s) (image2 (fun (a : β) (b : α) ↦ f b a) t s)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := Set γ) (image2 (fun (b : β) (x : α) ↦ f x b) t s) (image2 (fun (a : β) (b : α) ↦ f b a) t s)
⊢ ⋃ b ∈ t, (fun (x : α) ↦ f x b) '' s = image2 f s t

Tactic:
rw [image2_swap, iUnion_image_left]

Premises used: Set.iUnion_image_left, Set.image2_swap
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), image2 f (s i) t

Tactic:
simp only [← image_prod, iUnion_prod_const, image_iUnion]

Premises used: Set.image_prod, Set.iUnion_prod_const, Set.image_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), image2 f s (t i)

Tactic:
simp only [← image_prod, prod_iUnion, image_iUnion]

Premises used: Set.image_prod, Set.prod_iUnion, Set.image_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t

Tactic:
aesop
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t

Tactic:
aesop
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), image2 f (s i j) t

Tactic:
simp_rw [image2_iUnion_left]

Premises used: Set.image2_iUnion_left
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋃ (i : ι), ⋃ (j : κ i), t i j) = ⋃ (i : ι), ⋃ (j : κ i), image2 f s (t i j)

Tactic:
simp_rw [image2_iUnion_right]

Premises used: Set.image2_iUnion_right
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
simp_rw : ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t
⊢ image2 f (⋂ (i : ι), s i) t ⊆ ⋂ (i : ι), image2 f (s i) t

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Premises used: Set.mem_iInter, Set.image2_subset_iff
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t

Tactic:
fun x hx y hy i => mem_image2_of_mem (hx _) hy

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t

Tactic:
exact fun x hx y hy i => mem_image2_of_mem (hx _) hy

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
simp_rw : ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)
⊢ image2 f s (⋂ (i : ι), t i) ⊆ ⋂ (i : ι), image2 f s (t i)

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Premises used: Set.mem_iInter, Set.image2_subset_iff
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)

Tactic:
fun x hx y hy i => mem_image2_of_mem hx (hy _)

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)

Tactic:
exact fun x hx y hy i => mem_image2_of_mem hx (hy _)

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
simp_rw : ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t
⊢ image2 f (⋂ (i : ι), ⋂ (j : κ i), s i j) t ⊆ ⋂ (i : ι), ⋂ (j : κ i), image2 f (s i j) t

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Premises used: Set.mem_iInter, Set.image2_subset_iff
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t

Tactic:
fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t

Tactic:
exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
simp_rw : ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)
⊢ image2 f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ⊆ ⋂ (i : ι), ⋂ (j : κ i), image2 f s (t i j)

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Premises used: Set.mem_iInter, Set.image2_subset_iff
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)

Tactic:
fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)

Tactic:
exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
rw : image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
rw [sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
image2_iInter₂_subset_left ..

Premises used: Set.image2_iInter₂_subset_left
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
exact image2_iInter₂_subset_left ..

Premises used: Set.image2_iInter₂_subset_left
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
rw : image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t
⊢ image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
rw [sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
image2_iInter₂_subset_right ..

Premises used: Set.image2_iInter₂_subset_right
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
exact image2_iInter₂_subset_right ..

Premises used: Set.image2_iInter₂_subset_right
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : s ×ˢ t = image2 (fun (a : α) (b : β) ↦ (a, b)) s t
rw₁ rw₂ : s ×ˢ t = s ×ˢ t
⊢ s ×ˢ t = ⋃ a ∈ s, (fun (b : β) ↦ (a, b)) '' t

Tactic:
rw [iUnion_image_left, image2_mk_eq_prod]

Premises used: Set.image2_mk_eq_prod, Set.iUnion_image_left
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : s ×ˢ t = image2 Prod.mk s t
rw₁ rw₂ : s ×ˢ t = s ×ˢ t
⊢ s ×ˢ t = ⋃ b ∈ t, (fun (a : α) ↦ (a, b)) '' s

Tactic:
rw [iUnion_image_right, image2_mk_eq_prod]

Premises used: Set.iUnion_image_right, Set.image2_mk_eq_prod
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
rw : Eq.{u_2 + 1} (α := Set β) (image2 (fun (f : α → β) (a : α) ↦ f a) s t) (⋃ f ∈ s, f '' t)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set β) (image2 (fun (f : α → β) (a : α) ↦ f a) s t) (image2 (fun (f : α → β) ↦ f) s t)
⊢ s.seq t = ⋃ f ∈ s, f '' t

Tactic:
rw [seq_eq_image2, iUnion_image_left]

Premises used: Set.iUnion_image_left, Set.seq_eq_image2
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
u : Set β
⊢ s.seq t ⊆ u ↔ ∀ f ∈ s, ∀ a ∈ t, f a ∈ u

Tactic:
image2_subset_iff

Premises used: Set.image2_subset_iff, Set.seq
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s₀ s₁ : Set (α → β)
t₀ t₁ : Set α
hs : s₀ ⊆ s₁
ht : t₀ ⊆ t₁
⊢ s₀.seq t₀ ⊆ s₁.seq t₁

Tactic:
image2_subset hs ht

Premises used: Set.image2_subset, Set.seq
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : Set α
⊢ seq {f} t = f '' t

Tactic:
image2_singleton_left

Premises used: Set.image2_singleton_left, Set.seq
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set (α → β)
a : α
⊢ s.seq {a} = (fun (f : α → β) ↦ f a) '' s

Tactic:
image2_singleton_right

Premises used: Set.image2_singleton_right, Set.seq
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
simp :
  Eq.{u_3 + 1} (α := Set γ) (image2 (fun (f : β → γ) (a : β) ↦ f a) s (image2 (fun (f : α → β) (a : α) ↦ f a) t u))
    (image2 (fun (f : α → γ) (a : α) ↦ f a) (image2 (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) s t) u)
⊢ s.seq (t.seq u) = seq (seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' s) t) u

Tactic:
simp only [seq_eq_image2, image2_image_left]

Premises used: Set.image2_image_left, Set.seq_eq_image2
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ Eq.{u_3 + 1} (α := Set γ) (image2 (fun (f : β → γ) (a : β) ↦ f a) s (image2 (fun (f : α → β) (a : α) ↦ f a) t u))
    (image2 (fun (f : α → γ) (a : α) ↦ f a) (image2 (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) s t) u)

Tactic:
.symm <| image2_assoc fun _ _ _ ↦ rfl

Premises used: Set.image2_assoc, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ Eq.{u_3 + 1} (α := Set γ) (image2 (fun (f : β → γ) (a : β) ↦ f a) s (image2 (fun (f : α → β) (a : α) ↦ f a) t u))
    (image2 (fun (f : α → γ) (a : α) ↦ f a) (image2 (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) s t) u)

Tactic:
exact .symm <| image2_assoc fun _ _ _ ↦ rfl

Premises used: Set.image2_assoc, rfl
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
s : Set (α → β)
t : Set α
⊢ f '' s.seq t = seq ((fun (x : α → β) ↦ f ∘ x) '' s) t

Tactic:
simp only [seq, image_image2, image2_image_left, comp_apply]

Premises used: Set.image2_image_left, Set.image_image2, Function.comp_apply, Set.seq
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : s ×ˢ t = image2 (fun (f : β → α × β) (a : β) ↦ f a) (Prod.mk '' s) t
rw₁ : s ×ˢ t = image2 (fun (a : α) (b : β) ↦ (a, b)) s t
rw₂ rw₃ : s ×ˢ t = s ×ˢ t
⊢ s ×ˢ t = seq (Prod.mk '' s) t

Tactic:
rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]

Premises used: Set.image2_image_left, Set.image2_mk_eq_prod, Set.seq_eq_image2
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw :
  Eq (α := Set (α × β)) (seq ((fun (x : α → β × α) ↦ Prod.swap ∘ x) ∘ Prod.mk '' t) s)
    (seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) s)
⊢ seq (Prod.mk '' s) t = seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) s

Tactic:
rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]

Premises used: Set.image_swap_prod, Set.prod_eq_seq, Set.image_comp, Set.image_seq
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Eq (α := Set (α × β)) (seq ((fun (x : α → β × α) ↦ Prod.swap ∘ x) ∘ Prod.mk '' t) s)
    (seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) s)

Tactic:
rfl