awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ι), f i) ∩ ⋃ (j : κ), g j) (⋃ (i : ι), ⋃ (j : κ), f i ∩ g j)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), f i ∩ ⋃ (j : κ), g j) (⋃ (i : ι), ⋃ (j : κ), f i ∩ g j)
Tactic: simp_rw [iUnion_inter, inter_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) ((⋂ (i : ι), f i) ∪ ⋂ (j : κ), g j) (⋂ (i : ι), ⋂ (j : κ), f i ∪ g j)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), f i ∪ ⋂ (j : κ), g j) (⋂ (i : ι), ⋂ (j : κ), f i ∪ g j)
Tactic: simp_rw [iInter_union, union_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) ((⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), f i₁ i₂) ∩ ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), g j₁ j₂)
    (⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), f i₁ i₂ ∩ g j₁ j₂)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι₁), ⋃ (i_1 : ι₂ i), f i i_1 ∩ ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), g j₁ j₂)
  (⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), f i₁ i₂ ∩ g j₁ j₂)
Tactic: simp_rw [iUnion_inter, inter_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) ((⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), f i₁ i₂) ∪ ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), g j₁ j₂)
    (⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), f i₁ i₂ ∪ g j₁ j₂)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι₁), ⋂ (i_1 : ι₂ i), f i i_1 ∪ ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), g j₁ j₂)
  (⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), f i₁ i₂ ∪ g j₁ j₂)
Tactic: simp_rw [iInter_union, union_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
⊢ f '' ⋃₀ s = ⋃₀ (image f '' s)
have h : ∀ (x : β), x ∈ f '' ⋃₀ s ↔ x ∈ ⋃₀ (image f '' s)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
x : β
⊢ x ∈ f '' ⋃₀ s ↔ x ∈ ⋃₀ (image f '' s)
have h : x ∈ f '' ⋃₀ s ↔ ∃ (i : Set α) (_ : i ∈ s), x ∈ f '' i
Tactic: simp only [Set.mem_iUnion, Set.sUnion_image]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t
have rw : f ⁻¹' ⋃ i ∈ s, i = ⋃ t ∈ s, f ⁻¹' t
Tactic: rw [sUnion_eq_biUnion, preimage_iUnion₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
rw : f ⁻¹' ⋃ i ∈ s, i = ⋃ t ∈ s, f ⁻¹' t
⊢ f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t
have rw₁ : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, f ⁻¹' i) (⋃ t ∈ s, f ⁻¹' t)
Tactic: rw [sUnion_eq_biUnion, preimage_iUnion₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ f ⁻¹' ⋂ (i : ι), s i = ⋂ (i : ι), f ⁻¹' s i
have h : ∀ (x : α), x ∈ f ⁻¹' ⋂ (i : ι), s i ↔ Membership.mem (γ := Set α) (⋂ (i : ι), f ⁻¹' s i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t
have rw : f ⁻¹' ⋂ i ∈ s, i = ⋂ t ∈ s, f ⁻¹' t
Tactic: rw [sInter_eq_biInter, preimage_iInter₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
rw : f ⁻¹' ⋂ i ∈ s, i = ⋂ t ∈ s, f ⁻¹' t
⊢ f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t
have rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ s, f ⁻¹' i) (⋂ t ∈ s, f ⁻¹' t)
Tactic: rw [sInter_eq_biInter, preimage_iInter₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s
have rw : f ⁻¹' ⋃ i ∈ s, {i} = f ⁻¹' s
Tactic: rw [← preimage_iUnion₂, biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f ⁻¹' ⋃ i ∈ s, {i} = f ⁻¹' s
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s
have rw₁ : f ⁻¹' s = f ⁻¹' s
Tactic: rw [← preimage_iUnion₂, biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ y ∈ range f, f ⁻¹' {y}) univ
have rw : f ⁻¹' range f = univ
Tactic: rw [biUnion_preimage_singleton, preimage_range]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : f ⁻¹' range f = univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ y ∈ range f, f ⁻¹' {y}) univ
have rw₁ : Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [biUnion_preimage_singleton, preimage_range]
-- 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 β
⊢ 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
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun (t : Set β) ↦ s ×ˢ t) '' C)
have simp_rw : SProd.sprod (β := Set β) s (⋃ i ∈ C, i) =
  ⋃ (i : Set (α × β)), ⋃ (_ : Membership.mem (γ := Set (Set (α × β))) ((fun (t : Set β) ↦ s ×ˢ t) '' C) i), i
Tactic: simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
simp_rw :
  SProd.sprod (β := Set β) s (⋃ i ∈ C, i) =
    ⋃ (i : Set (α × β)), ⋃ (_ : Membership.mem (γ := Set (Set (α × β))) ((fun (t : Set β) ↦ s ×ˢ t) '' C) i), i
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun (t : Set β) ↦ s ×ˢ t) '' C)
have simp_rw₁ : SProd.sprod (β := Set β) s (⋃ i ∈ C, i) = ⋃ y ∈ C, s ×ˢ y
Tactic: simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]
-- 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 β
⊢ SProd.sprod (α := Set α) (⋃ (i : ι), s i) t = ⋃ (i : ι), s i ×ˢ t
have h : ∀ (x : α × β),
  x ∈ SProd.sprod (α := Set α) (⋃ (i : ι), s i) t ↔ Membership.mem (γ := Set (α × β)) (⋃ (i : ι), s i ×ˢ t) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
⊢ ⋃ (x : ι × ι'), s x.1 ×ˢ t x.2 = SProd.sprod (α := Set α) (β := Set β) (⋃ (i : ι), s i) (⋃ (i : ι'), t i)
have h : ∀ (x : α × β),
  Membership.mem (γ := Set (α × β)) (⋃ (x : ι × ι'), s x.1 ×ˢ t x.2) x ↔
    x ∈ SProd.sprod (α := Set α) (β := Set β) (⋃ (i : ι), s i) (⋃ (i : ι'), t i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
⊢ ⋃ (x : α), s x ×ˢ t x = SProd.sprod (α := Set β) (β := Set γ) (⋃ (x : α), s x) (⋃ (x : α), t x)
have h : ∀ (z : β) (w : γ),
  Membership.mem (γ := Set (β × γ)) (⋃ (x : α), s x ×ˢ t x) (z, w) ↔
    (z, w) ∈ SProd.sprod (α := Set β) (β := Set γ) (⋃ (x : α), s x) (⋃ (x : α), t x)
Tactic: ext ⟨z, w⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ Membership.mem (γ := Set (β × γ)) (⋃ (x : α), s x ×ˢ t x) (z, w) ↔
    (z, w) ∈ SProd.sprod (α := Set β) (β := Set γ) (⋃ (x : α), s x) (⋃ (x : α), t x)
have h : (∀ (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: simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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 : α), 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
have h : ∀ (x : α), z ∈ s x → w ∈ t x → (∃ (i : α), z ∈ s i) ∧ ∃ (i : α), w ∈ t i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
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
⊢ (∀ (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
have h₁ : ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ (i : α), z ∈ s i ∧ w ∈ t i
Tactic: constructor
-- 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 δ
⊢ ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = SProd.sprod (α := Set γ) (β := Set δ) (⋃ x ∈ s, f x) (⋃ x ∈ t, g x)
have 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)
Tactic: ext ⟨_, _⟩
-- 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 : δ
⊢ 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)
have h : (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) ↔ (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
Tactic: simp only [mem_iUnion, mem_prod, exists_prop, Prod.exists]
-- 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 : δ
⊢ (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) ↔ (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
have h : (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) → (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
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
⊢ (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) ↔ (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
have h₁ : ((∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i) → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
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
⊢ (∃ (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 → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
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
⊢ (∃ (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 → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
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
⊢ (∃ (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 → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
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
⊢ (∃ (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 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
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
⊢ (∃ (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 → ∃ (b : β), (w ∈ s ∧ b ∈ t) ∧ fst ∈ f w ∧ snd ∈ g b
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
⊢ (∃ (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 → α
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 → α
⊢ (∃ (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) ∧ fst ∈ f w ∧ snd ∈ g w_1
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
⊢ (∃ (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 → β
Tactic: tauto