awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk (β := α) i '' g i ⁻¹' s = Sigma.map (β₁ := α) (β₂ := β) f g ⁻¹' Sigma.mk (β := β) (f i) '' s
have refine : Sigma.map (β₁ := α) (β₂ := β) f g ⁻¹' Sigma.mk (β := β) (f i) '' s ⊆ Sigma.mk (β := α) i '' g i ⁻¹' s
Tactic: refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : Sigma.mk (β := β) (f i) y = Sigma.map (β₁ := α) (β₂ := β) f g (Sigma.mk (β := α) j x)
⊢ Sigma.mk (β := α) j x ∈ Sigma.mk (β := α) i '' g i ⁻¹' s
have hxy₁ : i = j ∧ y ≍ g j x
Tactic: simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
have pos : ∀ (h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁),
  x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
Tactic: by_cases h₁ : x.1 ∈ s₁
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
pos :
  ∀ (h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
have neg : ∀ (h₁ : x.fst (β := fun (i : ι) ↦ α i) ∉ s₁),
  x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
Tactic: by_cases h₁ : x.1 ∈ s₁
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
have pos : ∀
  (h₂ :
    Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
      (x.snd (β := fun (i : ι) ↦ α i))),
  x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
Tactic: by_cases h₂ : x.2 ∈ t₁ x.1
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁
pos :
  ∀
    (h₂ :
      Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
        (x.snd (β := fun (i : ι) ↦ α i))),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
have neg : ∀ (h₂ : x.snd (β := fun (i : ι) ↦ α i) ∉ t₁ (x.fst (β := fun (i : ι) ↦ α i))),
  x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
Tactic: by_cases h₂ : x.2 ∈ t₁ x.1
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∉ s₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
have pos : ∀
  (h₂ :
    Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
      (x.snd (β := fun (i : ι) ↦ α i))),
  x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
Tactic: by_cases h₂ : x.2 ∈ t₁ x.1
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∉ s₁
pos :
  ∀
    (h₂ :
      Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
        (x.snd (β := fun (i : ι) ↦ α i))),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
have neg : ∀ (h₂ : x.snd (β := fun (i : ι) ↦ α i) ∉ t₁ (x.fst (β := fun (i : ι) ↦ α i))),
  x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
Tactic: by_cases h₂ : x.2 ∈ t₁ x.1
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
β : (i : ι) → α i → Type u_7
s : Set ι
t : (i : ι) → Set (α i)
u : (p : (i : ι) × α i) → Set (β (p.fst (β := fun (i : ι) ↦ α i)) (p.snd (β := fun (i : ι) ↦ α i)))
⊢ Sigma.uncurry (β := fun (i : ι) ↦ α i) (γ := β) ⁻¹'
      (s.sigma (α := α) t).pi (α := fun (x : (i : ι) × α i) ↦
        β (x.fst (β := fun (i : ι) ↦ α i)) (x.snd (β := fun (i : ι) ↦ α i))) u =
    s.pi (α := fun (i : ι) ↦
      (i_1 : α i) →
        β ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).fst (β := fun (i : ι) ↦ α i))
          ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).snd (β := fun (i : ι) ↦ α i)))
      fun (i : ι) ↦
      (t i).pi (α := fun (j : α i) ↦
        β ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
          ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)))
        fun (j : α i) ↦ u (Sigma.mk (β := fun (i : ι) ↦ α i) i j)
have h : ∀ (x : (x : ι) → (y : α x) → β x y),
  x ∈
      Sigma.uncurry (β := fun (i : ι) ↦ α i) (γ := β) ⁻¹'
        (s.sigma (α := α) t).pi (α := fun (x : (i : ι) × α i) ↦
          β (x.fst (β := fun (i : ι) ↦ α i)) (x.snd (β := fun (i : ι) ↦ α i))) u ↔
    Membership.mem (γ := Set ((x : ι) → (y : α x) → β x y))
      (s.pi (α := fun (i : ι) ↦
        (i_1 : α i) →
          β ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).fst (β := fun (i : ι) ↦ α i))
            ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).snd (β := fun (i : ι) ↦ α i)))
        fun (i : ι) ↦
        (t i).pi (α := fun (j : α i) ↦
          β ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
            ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)))
          fun (j : α i) ↦ u (Sigma.mk (β := fun (i : ι) ↦ α i) i j))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
β : (i : ι) → α i → Type u_7
s : Set ι
t : (i : ι) → Set (α i)
u : (p : (i : ι) × α i) → Set (β (p.fst (β := fun (i : ι) ↦ α i)) (p.snd (β := fun (i : ι) ↦ α i)))
x : (x : ι) → (y : α x) → β x y
⊢ x ∈
      Sigma.uncurry (β := fun (i : ι) ↦ α i) (γ := β) ⁻¹'
        (s.sigma (α := α) t).pi (α := fun (x : (i : ι) × α i) ↦
          β (x.fst (β := fun (i : ι) ↦ α i)) (x.snd (β := fun (i : ι) ↦ α i))) u ↔
    Membership.mem (γ := Set ((x : ι) → (y : α x) → β x y))
      (s.pi (α := fun (i : ι) ↦
        (i_1 : α i) →
          β ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).fst (β := fun (i : ι) ↦ α i))
            ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).snd (β := fun (i : ι) ↦ α i)))
        fun (i : ι) ↦
        (t i).pi (α := fun (j : α i) ↦
          β ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
            ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)))
          fun (j : α i) ↦ u (Sigma.mk (β := fun (i : ι) ↦ α i) i j))
      x
have h : (∀ (i : (i : ι) × α i),
    i.fst (β := fun (i : ι) ↦ α i) ∈ s →
      Membership.mem (γ := Set (α (i.fst (β := fun (i : ι) ↦ α i)))) (t (i.fst (β := fun (i : ι) ↦ α i)))
          (i.snd (β := fun (i : ι) ↦ α i)) →
        Sigma.uncurry (β := fun (i : ι) ↦ α i) (γ := β) x i ∈ u i) ↔
  ∀ i ∈ s,
    ∀ i_1 ∈ t i,
      Membership.mem (γ := Set (β i i_1))
        (u (Sigma.mk (β := fun (i : ι) ↦ α i) i i_1) :
          Set
            (β ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).fst (β := fun (i : ι) ↦ α i))
              ((Sigma.mk (β := fun (i : ι) ↦ α i) i i_1).snd (β := fun (i : ι) ↦ α i))))
        (x i i_1)
Tactic: simp only [mem_preimage, mem_pi, mem_sigma_iff, and_imp]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A B : Set α
h : A ⊆ B
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ B) univ
have rw : ∀ (a : α) (b : a ∈ A), Membership.mem (γ := Set (↑A : Type u_2)) (A ↓∩ B) (Subtype.mk (p := fun (a : α) ↦ a ∈ A) a b)
Tactic: rw [eq_univ_iff_forall, Subtype.forall]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋃₀ S) (⋃₀ {x : Set (↑A : Type u_2) | ∃ B ∈ S, A ↓∩ B = x})
have rw : Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋃₀ S) (⋃ a ∈ S, A ↓∩ a)
Tactic: rw [← Set.image, sUnion_image]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋃₀ S) (⋃ a ∈ S, A ↓∩ a)
have simp_rw : Eq.{u_2 + 1} (α := Set (↑A : Type u_2)) (A ↓∩ ⋃ i ∈ S, i) (⋃ a ∈ S, A ↓∩ a)
Tactic: simp_rw [sUnion_eq_biUnion, preimage_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋂₀ S) (⋂₀ {x : Set (↑A : Type u_2) | ∃ B ∈ S, A ↓∩ B = x})
have rw : Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋂₀ S) (⋂ a ∈ S, A ↓∩ a)
Tactic: rw [← Set.image, sInter_image]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋂₀ S) (⋂ a ∈ S, A ↓∩ a)
have simp_rw : Eq.{u_2 + 1} (α := Set (↑A : Type u_2)) (A ↓∩ ⋂ i ∈ S, i) (⋂ a ∈ S, A ↓∩ a)
Tactic: simp_rw [sInter_eq_biInter, preimage_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (hypothesis)
Goal:
α : Type u_2
A B C : Set α
hB : B ⊆ A
hC : C ⊆ A
h : Eq (α := Set (↑A : Type u_2)) (A ↓∩ B) (A ↓∩ C)
⊢ B = C
have hB₁ : A ∩ B = B
Tactic: simp only [← inter_eq_right] at hB hC
Cleared hypotheses: hB, hC
-- Lean 4 proof step from Mathlib.Data.Set.Subset (hypothesis)
Goal:
α : Type u_2
A B C : Set α
hB : B ⊆ A
hC : C ⊆ A
h : Eq (α := Set (↑A : Type u_2)) (A ↓∩ B) (A ↓∩ C)
hB₁ : A ∩ B = B
⊢ B = C
have hC₁ : A ∩ C = C
Tactic: simp only [← inter_eq_right] at hB hC
Cleared hypotheses: hB, hC
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' Dᶜ = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
have rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (univ \ D) = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
Tactic: rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (univ \ D) = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' Dᶜ = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
have rw₁ : image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) univ \
    Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D =
  A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
Tactic: rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (univ \ D) = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
rw₁ :
  image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) univ \
      Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D =
    A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' Dᶜ = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
have rw₂ : range (ι := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D =
  A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
Tactic: rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (univ \ D) = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
rw₁ :
  image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) univ \
      Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D =
    A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
rw₂ :
  range (ι := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) \
      Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D =
    A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' Dᶜ = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
have rw₃ : {x : α | x ∈ A} \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
Tactic: rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (univ \ D) = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
rw₁ :
  image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) univ \
      Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D =
    A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
rw₂ :
  range (ι := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) \
      Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D =
    A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
rw₃ : {x : α | x ∈ A} \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' Dᶜ = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
have rw₄ : A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D = A \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D
Tactic: rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
T : Set (Set (↑A : Type u_2))
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋃₀ T =
    ⋃₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
have rw : ⋃₀ (image (Subtype.val (p := fun (x : α) ↦ x ∈ A)) '' T) =
  ⋃₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
Tactic: rw [image_sUnion, image]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
T : Set (Set (↑A : Type u_2))
rw :
  ⋃₀ (image (Subtype.val (p := fun (x : α) ↦ x ∈ A)) '' T) =
    ⋃₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋃₀ T =
    ⋃₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
have rw₁ : Eq.{u_2 + 1} (α := Set α) (⋃₀ {x : Set α | ∃ a ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' a = x})
  (⋃₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x})
Tactic: rw [image_sUnion, image]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
T : Set (Set (↑A : Type u_2))
hT : T.Nonempty
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T =
    ⋂₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
have rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T = ⋂₀ (image (Subtype.val (p := fun (x : α) ↦ x ∈ A)) '' T)
Tactic: rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
T : Set (Set (↑A : Type u_2))
hT : T.Nonempty
rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T = ⋂₀ (image (Subtype.val (p := fun (x : α) ↦ x ∈ A)) '' T)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T =
    ⋂₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
have rw₁ : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T = ⋂ a ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' a
Tactic: rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
T : Set (Set (↑A : Type u_2))
hT : T.Nonempty
rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T = ⋂₀ (image (Subtype.val (p := fun (x : α) ↦ x ∈ A)) '' T)
rw₁ : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T = ⋂ a ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' a
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T =
    ⋂₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
have rw₂ : Eq.{u_2 + 1} (α := Set α) (image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) (⋂ i ∈ T, i))
  (⋂ a ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' a)
Tactic: rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
T : Set (Set (↑A : Type u_2))
hT : T.Nonempty
rw : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T = ⋂₀ (image (Subtype.val (p := fun (x : α) ↦ x ∈ A)) '' T)
rw₁ : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T = ⋂ a ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' a
rw₂ :
  Eq.{u_2 + 1} (α := Set α) (image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) (⋂ i ∈ T, i))
    (⋂ a ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' a)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T =
    ⋂₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}
have rw₃ : Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' i)
  (⋂ a ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' a)
Tactic: rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]
-- Lean 4 proof step from Mathlib.Data.Set.Subset (goal)
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
⊢ D ⊆ A ↓∩ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E ↔ D ⊆ E
have rw : D ⊆ E ↔ D ⊆ E
Tactic: rw [preimage_image_eq _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
p : Set α → Prop
hs : s.Subsingleton
he : p ∅
h₁ : ∀ (x : α), p {x}
⊢ p s
have inl : ∀ (hs : Set.Subsingleton.{u} (α := α) ∅), p ∅
Tactic: rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
p : Set α → Prop
hs : s.Subsingleton
he : p ∅
h₁ : ∀ (x : α), p {x}
inl : ∀ (hs : Set.Subsingleton.{u} (α := α) ∅), p ∅
⊢ p s
have inr : ∀ (x : α) (hs : Set.Subsingleton (α := α) {x}), p {x}
Tactic: rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
⊢ (∃ (a : α), s = {a}) ↔ s.Nonempty ∧ s.Subsingleton
have refine_1 : (∃ (a : α), s = {a}) → s.Nonempty ∧ s.Subsingleton
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
refine_1 : (∃ (a : α), s = {a}) → s.Nonempty ∧ s.Subsingleton
⊢ (∃ (a : α), s = {a}) ↔ s.Nonempty ∧ s.Subsingleton
have refine_2 : ∀ (h : s.Nonempty ∧ s.Subsingleton), ∃ (a : α), s = {a}
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
⊢ Subsingleton.{u + 1} (↑s : Type u) ↔ s.Subsingleton
have mp : Subsingleton.{u + 1} (↑s : Type u) → s.Subsingleton
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
mp : Subsingleton.{u + 1} (↑s : Type u) → s.Subsingleton
⊢ Subsingleton.{u + 1} (↑s : Type u) ↔ s.Subsingleton
have mpr : s.Subsingleton → Subsingleton.{u + 1} (↑s : Type u)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
⊢ Subsingleton.{u + 1} (↑s : Type u) → s.Subsingleton
have mp : ∀ (h : Subsingleton.{u + 1} (↑s : Type u)) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s), a = b
Tactic: refine fun h => fun a ha b hb => ?_
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
a : α
s_1 t : Set α
inst : Subsingleton α
s : Set α
⊢ Subsingleton.{u + 1} (↑s : Type u)
have rw : s.Subsingleton
Tactic: rw [s.subsingleton_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
⊢ ∃ (x : α), x ∈ s ∧ x ≠ z
have by_contra! : ∀ (H : ∀ (x : α) (_ : x ∈ s), x = z), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
H : ∀ (x : α) (_ : x ∈ s), x = z
⊢ False
have rcases : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), False
Tactic: rcases hs with ⟨x, hx, y, hy, hxy⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (hypothesis)
Goal:
α : Type u
s : Set α
z : α
H : ∀ (x : α) (_ : x ∈ s), x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ False
have hxy₁ : z ≠ z
Tactic: rw [H x hx, H y hy] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (hypothesis)
Goal:
α : Type u
x : α
H : Set.Nontrivial (α := α) {x}
⊢ False
have H₁ : ∃ (y : α), Membership.mem (γ := Set α) {x} y ∧ y ≠ x
Tactic: rw [nontrivial_iff_exists_ne (mem_singleton x)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
x : α
H : ∃ (y : α), Membership.mem (γ := Set α) {x} y ∧ y ≠ x
⊢ False
have let : ∀ (y : α) (hy : Membership.mem (γ := Set α) {x} y) (hya : y ≠ x), False
Tactic: let ⟨y, hy, hya⟩ := H
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (hypothesis)
Goal:
α : Type u
s : Set α
x : α
hs : s.Nontrivial
H : s = {x}
⊢ False
have hs₁ : Set.Nontrivial (α := α) {x}
Tactic: rw [H] at hs
Cleared hypotheses: hs, H
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
⊢ ¬s.Subsingleton ↔ s.Nontrivial
have simp_rw : (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ s.Nontrivial
Tactic: simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
simp_rw : (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ s.Nontrivial
⊢ ¬s.Subsingleton ↔ s.Nontrivial
have simp_rw₁ : (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x ≠ y
Tactic: simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
s : Set α
simp_rw : (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ s.Nontrivial
simp_rw₁ : (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x ≠ y
⊢ ¬s.Subsingleton ↔ s.Nontrivial
have simp_rw₂ : (∃ (x : α), ∃ (h : x ∈ s), ∃ (x_1 : α), ∃ (x_2 : x_1 ∈ s), ¬x = x_1) ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x ≠ y
Tactic: simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial
have rw : s.Subsingleton ∨ s.Nontrivial
Tactic: rw [← subsingleton_iff_singleton ha]
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
⊢ Eq (α := Set (Set α)) univ {∅} ↔ IsEmpty α
have refine : ∀ (h : Eq (α := Set (Set α)) univ {∅}), IsEmpty α
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ by simp⟩
-- Lean 4 proof step from Mathlib.Data.Set.Subsingleton (goal)
Goal:
α : Type u
h : Eq (α := Set (Set α)) univ {∅}
⊢ IsEmpty α
have suffices : Membership.mem (γ := Set (Set α)) univ univ
Tactic: suffices @univ α ∈ univ by aesop