awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
h₁ : ((∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i) → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₂ h₃ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
h₄ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₅ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₆ h₇ h₈ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₉ h₁₀ h₁₁ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₁₂ h₁₃ h₁₄ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₁₅ h₁₆ h₁₇ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₁₈ h₁₉ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₂₀ h₂₁ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₂₂ h₂₃ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₂₄ :
  ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (b : β), (w ∈ s ∧ b ∈ t) ∧ fst ∈ f w ∧ snd ∈ g b
h₂₅ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₂₆ :
  ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (b : β), (w ∈ s ∧ b ∈ t) ∧ fst ∈ f w ∧ snd ∈ g b
h₂₇ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₂₈ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → (w ∈ s ∧ w_1 ∈ t) ∧ fst ∈ f w ∧ snd ∈ g w_1
h₂₉ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₃₀ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₃₁ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → (w ∈ s ∧ w_1 ∈ t) ∧ fst ∈ f w ∧ snd ∈ g w_1
h₃₂ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₃₃ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
⊢ (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) ↔ (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
have h₃₄ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → w ∈ s ∧ w_1 ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
h₁ : ((∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i) → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₂ h₃ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
h₄ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₅ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₆ h₇ h₈ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₉ h₁₀ h₁₁ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₁₂ h₁₃ h₁₄ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₁₅ h₁₆ h₁₇ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₁₈ h₁₉ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₂₀ h₂₁ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₂₂ h₂₃ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₂₄ :
  ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (b : β), (w ∈ s ∧ b ∈ t) ∧ fst ∈ f w ∧ snd ∈ g b
h₂₅ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₂₆ :
  ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (b : β), (w ∈ s ∧ b ∈ t) ∧ fst ∈ f w ∧ snd ∈ g b
h₂₇ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₂₈ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → (w ∈ s ∧ w_1 ∈ t) ∧ fst ∈ f w ∧ snd ∈ g w_1
h₂₉ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₃₀ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₃₁ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → (w ∈ s ∧ w_1 ∈ t) ∧ fst ∈ f w ∧ snd ∈ g w_1
h₃₂ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₃₃ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₃₄ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → w ∈ s ∧ w_1 ∈ t
⊢ (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) ↔ (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
have h₃₅ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → fst ∈ f w ∧ snd ∈ g w_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hS : S.Nonempty
hT : T.Nonempty
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
have obtain : ∀ (s₁ : Set α) (h₁ : s₁ ∈ S), ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
Tactic: obtain ⟨s₁, h₁⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hT : T.Nonempty
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
have obtain : ∀ (s₂ : Set β) (h₂ : s₂ ∈ T), ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
Tactic: obtain ⟨s₂, h₂⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
have refine : ∀ (x : α × β) (hx : Membership.mem (γ := Set (α × β)) (⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2) x), x ∈ ⋂₀ S ×ˢ ⋂₀ T
Tactic: refine Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (hypothesis)
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
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
have hx₁ : ∀ (i : Prod.{u_1, u_2} (Set α) (Set β)) (j : i ∈ S ×ˢ T), x ∈ i.1 ×ˢ i.2
Tactic: rw [mem_iInter₂] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t
have rw : Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (β := Set (Set β)) S {t}, r.1 ×ˢ r.2) (⋂ s ∈ S, s ×ˢ t)
Tactic: rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (β := Set (Set β)) S {t}, r.1 ×ˢ r.2) (⋂ s ∈ S, s ×ˢ t)
have 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)
Tactic: simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (β := Set (Set β)) S {t}, r.1 ×ˢ r.2) (⋂ s ∈ S, s ×ˢ t)
have 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)
Tactic: simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (β := Set (Set β)) S {t}, r.1 ×ˢ r.2) (⋂ s ∈ S, s ×ˢ t)
have 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)
Tactic: simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (β := Set (Set β)) S {t}, r.1 ×ˢ r.2) (⋂ s ∈ S, s ×ˢ t)
have 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)
Tactic: simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t
have rw : Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (α := Set (Set α)) {s} T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)
Tactic: rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (α := Set (Set α)) {s} T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)
have simp_rw : Eq (α := Set (α × β)) (⋂ r ∈ Prod.mk 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]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (α := Set (Set α)) {s} T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)
have 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)
Tactic: simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (α := Set (Set α)) {s} T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)
have 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)
Tactic: simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ Eq (α := Set (α × β)) (⋂ r ∈ SProd.sprod (α := Set (Set α)) {s} T, r.1 ×ˢ r.2) (⋂ t ∈ T, s ×ˢ t)
have 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)
Tactic: simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
⊢ SProd.sprod (β := Set β) s (⋂ (i : ι), t i) = ⋂ (i : ι), s ×ˢ t i
have h : ∀ (x : α × β),
  x ∈ SProd.sprod (β := Set β) s (⋂ (i : ι), t i) ↔ Membership.mem (γ := Set (α × β)) (⋂ (i : ι), s ×ˢ t i) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ x ∈ SProd.sprod (β := Set β) s (⋂ (i : ι), t i) ↔ Membership.mem (γ := Set (α × β)) (⋂ (i : ι), s ×ˢ t i) x
have h : (x.1 ∈ s ∧ ∀ (i : ι), x.2 ∈ t i) ↔ ∀ (i : ι), x.1 ∈ s ∧ x.2 ∈ t i
Tactic: simp only [mem_prod, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
have h : ∀ (x : γ), x ∈ image2 f s t ↔ Membership.mem (γ := Set γ) (⋃ i ∈ s, ⋃ j ∈ t, {f i j}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ b ∈ t, (fun (x : α) ↦ f x b) '' s = image2 f s t
have rw : Eq.{u_3 + 1} (α := Set γ) (⋃ b ∈ t, (fun (x : α) ↦ f x b) '' s) (image2 (fun (a : β) (b : α) ↦ f b a) t s)
Tactic: rw [image2_swap, iUnion_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ ⋃ b ∈ t, (fun (x : α) ↦ f x b) '' s = image2 f s t
have rw₁ : Eq.{u_3 + 1} (α := Set γ) (image2 (fun (b : β) (x : α) ↦ f x b) t s) (image2 (fun (a : β) (b : α) ↦ f b a) t s)
Tactic: rw [image2_swap, iUnion_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
have simp_rw : ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t
Tactic: simp_rw [image2_subset_iff, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
have simp_rw : ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)
Tactic: simp_rw [image2_subset_iff, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
have 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
Tactic: simp_rw [image2_subset_iff, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
have 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)
Tactic: simp_rw [image2_subset_iff, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
have rw : image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t
Tactic: rw [sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
have rw : image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t
Tactic: rw [sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ a ∈ s, (fun (b : β) ↦ (a, b)) '' t
have rw : s ×ˢ t = image2 (fun (a : α) (b : β) ↦ (a, b)) s t
Tactic: rw [iUnion_image_left, image2_mk_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : s ×ˢ t = image2 (fun (a : α) (b : β) ↦ (a, b)) s t
⊢ s ×ˢ t = ⋃ a ∈ s, (fun (b : β) ↦ (a, b)) '' t
have rw₁ : s ×ˢ t = s ×ˢ t
Tactic: rw [iUnion_image_left, image2_mk_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ b ∈ t, (fun (a : α) ↦ (a, b)) '' s
have rw : s ×ˢ t = image2 Prod.mk s t
Tactic: rw [iUnion_image_right, image2_mk_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : s ×ˢ t = image2 Prod.mk s t
⊢ s ×ˢ t = ⋃ b ∈ t, (fun (a : α) ↦ (a, b)) '' s
have rw₁ : s ×ˢ t = s ×ˢ t
Tactic: rw [iUnion_image_right, image2_mk_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ s.seq t = ⋃ f ∈ s, f '' t
have rw : Eq.{u_2 + 1} (α := Set β) (image2 (fun (f : α → β) (a : α) ↦ f a) s t) (⋃ f ∈ s, f '' t)
Tactic: rw [seq_eq_image2, iUnion_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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)
⊢ s.seq t = ⋃ f ∈ s, f '' t
have rw₁ : Eq.{u_2 + 1} (α := Set β) (image2 (fun (f : α → β) (a : α) ↦ f a) s t) (image2 (fun (f : α → β) ↦ f) s t)
Tactic: rw [seq_eq_image2, iUnion_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ s.seq (t.seq u) = seq (seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' s) t) u
have 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)
Tactic: simp only [seq_eq_image2, image2_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = seq (Prod.mk '' s) t
have rw : s ×ˢ t = image2 (fun (f : β → α × β) (a : β) ↦ f a) (Prod.mk '' s) t
Tactic: rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : s ×ˢ t = image2 (fun (f : β → α × β) (a : β) ↦ f a) (Prod.mk '' s) t
⊢ s ×ˢ t = seq (Prod.mk '' s) t
have rw₁ : s ×ˢ t = image2 (fun (a : α) (b : β) ↦ (a, b)) s t
Tactic: rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
⊢ s ×ˢ t = seq (Prod.mk '' s) t
have rw₂ : s ×ˢ t = s ×ˢ t
Tactic: rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ seq (Prod.mk '' s) t = seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) s
have rw : Eq (α := Set (α × β)) (seq ((fun (x : α → β × α) ↦ Prod.swap ∘ x) ∘ Prod.mk '' t) s)
  (seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) s)
Tactic: rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = (f '' s).seq t
have rw : image2 f s t = image2 (fun (f : β → γ) (a : β) ↦ f a) (f '' s) t
Tactic: rw [seq_eq_image2, image2_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
rw : image2 f s t = image2 (fun (f : β → γ) (a : β) ↦ f a) (f '' s) t
⊢ image2 f s t = (f '' s).seq t
have rw₁ : image2 f s t = image2 (fun (a : α) (b : β) ↦ f a b) s t
Tactic: rw [seq_eq_image2, image2_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
Goal:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ t, s i) ⊤
x : β
⊢ ∃ i ∈ t, x ∈ s i
have p : Membership.mem (γ := Set β) ⊤ x
Tactic: have p : x ∈ ⊤ := Set.mem_univ x
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
Goal:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ t, s i) ⊤
x : β
p : Membership.mem (γ := Set β) ⊤ x
⊢ ∃ i ∈ t, x ∈ s i
have p₁ : ∃ (i : ι), Membership.mem (γ := Set β) (⋃ (_ : i ∈ t), s i) x
Tactic: rw [← w, Set.mem_iUnion] at p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, s i) ⊤
⊢ t.Nonempty
have obtain : ∀ (x : ι) (m : x ∈ t), t.Nonempty
Tactic: obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
h_Union : Set.Nonempty.{u_1} (α := α) (⋃ (i : ι), s i)
⊢ Nonempty ι
have obtain : ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x), Nonempty ι
Tactic: obtain ⟨x, hx⟩ := h_Union
Cleared hypotheses: h_Union
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), {x : α | P i x}) {x : α | ∃ (i : ι), P i x}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (⋃ (i : ι), {x : α | P i x}) x ↔ Membership.mem (γ := Set α) {x : α | ∃ (i : ι), P i x} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), {x : α | P i x}) {x : α | ∀ (i : ι), P i x}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (⋂ (i : ι), {x : α | P i x}) x ↔ Membership.mem (γ := Set α) {x : α | ∀ (i : ι), P i x} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
x : β
t : ι → Set β
⊢ Eq (α := Set β) (insert x (⋃ (i : ι), t i)) (⋃ (i : ι), insert x (t i))
have simp_rw : Eq (α := Set β) ((⋃ (i : ι), t i) ∪ {x}) (⋃ (i : ι), t i ∪ {x})
Tactic: simp_rw [← union_singleton, iUnion_union]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ Eq (α := Set β) (insert x (⋂ (i : ι), t i)) (⋂ (i : ι), insert x (t i))
have simp_rw : Eq (α := Set β) ((⋂ (i : ι), t i) ∪ {x}) (⋂ (i : ι), t i ∪ {x})
Tactic: simp_rw [← union_singleton, iInter_union]