awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Sigma
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)))
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
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.Data.Set.Sigma
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
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)
⊢ 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:
simp only [mem_preimage, mem_pi, mem_sigma_iff, and_imp]

Premises used: and_imp, Set.mem_sigma_iff, Set.mem_pi, Set.mem_preimage
-- Module: Mathlib.Data.Set.Sigma
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
⊢ (∀ (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:
⟨fun h i hi j hj ↦ h ⟨i, j⟩ hi hj, fun h p hp1 hp2 ↦ h p.1 hp1 p.2 hp2⟩

Premises used: Sigma.fst, Iff.intro, Sigma.mk, Sigma.snd
-- Module: Mathlib.Data.Set.Sigma
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
⊢ (∀ (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:
exact ⟨fun h i hi j hj ↦ h ⟨i, j⟩ hi hj, fun h p hp1 hp2 ↦ h p.1 hp1 p.2 hp2⟩
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A B : Set α
h : A ⊆ B
rw :
  ∀ (a : α) (b : a ∈ A), Membership.mem (γ := Set (↑A : Type u_2)) (A ↓∩ B) (Subtype.mk (p := fun (a : α) ↦ a ∈ A) a b)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ B) univ

Tactic:
rw [eq_univ_iff_forall, Subtype.forall]

Premises used: Set.eq_univ_iff_forall, Subtype.forall
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A B : Set α
h : A ⊆ B
⊢ ∀ (a : α) (b : a ∈ A), Membership.mem (γ := Set (↑A : Type u_2)) (A ↓∩ B) (Subtype.mk (p := fun (a : α) ↦ a ∈ A) a b)

Tactic:
h

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A B : Set α
h : A ⊆ B
⊢ ∀ (a : α) (b : a ∈ A), Membership.mem (γ := Set (↑A : Type u_2)) (A ↓∩ B) (Subtype.mk (p := fun (a : α) ↦ a ∈ A) a b)

Tactic:
exact h
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
rw : Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋃₀ S) (⋃ a ∈ S, A ↓∩ a)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋃₀ S) (⋃₀ {x : Set (↑A : Type u_2) | ∃ B ∈ S, A ↓∩ B = x})

Tactic:
rw [← Set.image, sUnion_image]

Premises used: Set.sUnion_image, Set.image
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
simp_rw : Eq.{u_2 + 1} (α := Set (↑A : Type u_2)) (A ↓∩ ⋃ i ∈ S, i) (⋃ a ∈ S, A ↓∩ a)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋃₀ S) (⋃ a ∈ S, A ↓∩ a)

Tactic:
simp_rw [sUnion_eq_biUnion, preimage_iUnion]

Premises used: Set.sUnion_eq_biUnion, Set.preimage_iUnion
-- Module: Mathlib.Data.Set.Subset
Goal:
ι : Sort u_1
α : Type u_2
A : Set α
s : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set (↑A : Type u_2)) (A ↓∩ ⋂ (i : ι), s i) (⋂ (i : ι), A ↓∩ s i)

Tactic:
preimage_iInter

Premises used: Set.preimage_iInter
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
rw : Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋂₀ S) (⋂ a ∈ S, A ↓∩ a)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋂₀ S) (⋂₀ {x : Set (↑A : Type u_2) | ∃ B ∈ S, A ↓∩ B = x})

Tactic:
rw [← Set.image, sInter_image]

Premises used: Set.sInter_image, Set.image
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
simp_rw : Eq.{u_2 + 1} (α := Set (↑A : Type u_2)) (A ↓∩ ⋂ i ∈ S, i) (⋂ a ∈ S, A ↓∩ a)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋂₀ S) (⋂ a ∈ S, A ↓∩ a)

Tactic:
simp_rw [sInter_eq_biInter, preimage_iInter]

Premises used: Set.sInter_eq_biInter, Set.preimage_iInter
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ Eq (α := Set (↑A : Type u_2)) (A ↓∩ ⋂₀ S) (⋂₀ ((fun (x : Set α) ↦ A ↓∩ x) '' S))

Tactic:
simp only [preimage_sInter, sInter_image]

Premises used: Set.preimage_sInter, Set.sInter_image
-- Module: Mathlib.Data.Set.Subset
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)
⊢ A ∩ B = B

Tactic:
simp only [← inter_eq_right] at hB hC

Premises used: Set.inter_eq_right
-- Module: Mathlib.Data.Set.Subset
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
⊢ A ∩ C = C

Tactic:
simp only [← inter_eq_right] at hB hC

Premises used: Set.inter_eq_right
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A B C : Set α
h : Eq (α := Set (↑A : Type u_2)) (A ↓∩ B) (A ↓∩ C)
hB : A ∩ B = B
hC : A ∩ C = C
⊢ B = C

Tactic:
simp only [Subtype.preimage_val_eq_preimage_val_iff, hB, hC] at h

Premises used: Subtype.preimage_val_eq_preimage_val_iff
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A B C : Set α
hB : A ∩ B = B
hC : A ∩ C = C
h : B = C
⊢ B = C

Tactic:
h
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A B C : Set α
hB : A ∩ B = B
hC : A ∩ C = C
h : B = C
⊢ B = C

Tactic:
exact h
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (D ∪ E) =
    Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D ∪ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E

Tactic:
image_union _ _ _

Premises used: Set.image_union
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (D ∩ E) =
    Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D ∩ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E

Tactic:
image_inter Subtype.val_injective

Premises used: Subtype.val_injective, Set.image_inter
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' (D \ E) =
    Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D \ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E

Tactic:
image_diff Subtype.val_injective _ _

Premises used: Subtype.val_injective, Set.image_diff
-- Module: Mathlib.Data.Set.Subset
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
rw₄ rw₅ : 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

Tactic:
rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]

Premises used: Set.image_univ, Subtype.range_coe_subtype, Set.setOf_mem_eq, Set.compl_eq_univ_diff, Set.image_val_diff
-- Module: Mathlib.Data.Set.Subset
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}
rw₁ 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})
⊢ 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]

Premises used: Set.image_sUnion, Set.image
-- Module: Mathlib.Data.Set.Subset
Goal:
ι : Sort u_1
α : Type u_2
A : Set α
t : ι → Set (↑A : Type u_2)
⊢ Eq.{u_2 + 1} (α := Set α) (image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) (⋃ (i : ι), t i))
    (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ A) '' t i)

Tactic:
image_iUnion

Premises used: Set.image_iUnion
-- Module: Mathlib.Data.Set.Subset
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)
rw₃ 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)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' ⋂₀ T =
    ⋂₀ {x : Set α | ∃ B ∈ T, Subtype.val (p := fun (x : α) ↦ x ∈ A) '' B = x}

Tactic:
rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]

Premises used: Subtype.val_injective, Function.Injective.injOn, Set.sInter_eq_biInter, Set.sInter_image, Set.image, Set.InjOn.image_biInter_eq
-- Module: Mathlib.Data.Set.Subset
Goal:
ι : Sort u_1
α : Type u_2
A : Set α
t : ι → Set (↑A : Type u_2)
inst : Nonempty ι
⊢ Eq.{u_2 + 1} (α := Set α) (image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) (⋂ (i : ι), t i))
    (⋂ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ A) '' t i)

Tactic:
Subtype.val_injective.injOn.image_iInter_eq

Premises used: Subtype.val_injective, Function.Injective.injOn, Set.InjOn.image_iInter_eq
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
⊢ A ∪ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D = A

Tactic:
union_eq_left.2 image_val_subset

Premises used: Iff.mpr, Set.union_eq_left, Set.image_val_subset
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D ∪ A = A

Tactic:
union_eq_right.2 image_val_subset

Premises used: Iff.mpr, Set.image_val_subset, Set.union_eq_right
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
⊢ A ∩ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D = Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D

Tactic:
inter_eq_right.2 image_val_subset

Premises used: Iff.mpr, Set.inter_eq_right, Set.image_val_subset
-- Module: Mathlib.Data.Set.Subset
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

Tactic:
inter_eq_left.2 image_val_subset

Premises used: Set.inter_eq_left, Iff.mpr, Set.image_val_subset
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
rw rw₁ : D ⊆ E ↔ D ⊆ E
⊢ D ⊆ A ↓∩ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E ↔ D ⊆ E

Tactic:
rw [preimage_image_eq _ Subtype.val_injective]

Premises used: Subtype.val_injective, Set.preimage_image_eq
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D = Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E ↔ D = E

Tactic:
Subtype.val_injective.image_injective.eq_iff

Premises used: Subtype.val_injective, Function.Injective.eq_iff, Function.Injective.image_injective
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Set { x : α // x ∈ A }) (image (Subtype.val (p := fun (x : α) ↦ x ∈ A)))

Tactic:
Subtype.val_injective.image_injective

Premises used: Subtype.val_injective, Function.Injective.image_injective
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
h : Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E
⊢ D ⊆ E

Tactic:
(image_subset_image_iff Subtype.val_injective).1 h

Premises used: Subtype.val_injective, Set.image_subset_image_iff, Iff.mp
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D E : Set (↑A : Type u_2)
h : D ⊆ E
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' E

Tactic:
(image_subset_image_iff Subtype.val_injective).2 h

Premises used: Iff.mpr, Subtype.val_injective, Set.image_subset_image_iff
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A B : Set α
⊢ image (α := { x : α // x ∈ A }) (Subtype.val (p := fun (x : α) ↦ x ∈ A)) (A ↓∩ B) ⊆ B

Tactic:
image_preimage_subset _ _

Premises used: Set.image_preimage_subset
-- Module: Mathlib.Data.Set.Subset
Goal:
α : Type u_2
A : Set α
D : Set (↑A : Type u_2)
⊢ A ↓∩ Subtype.val (p := fun (x : α) ↦ x ∈ A) '' D = D

Tactic:
Function.Injective.preimage_image Subtype.val_injective _

Premises used: Subtype.val_injective, Function.Injective.preimage_image
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s t : Set α
ht : t.Subsingleton
hst : s ⊆ t
⊢ s.Subsingleton

Tactic:
fun _ hx _ hy =>
  ht (hst hx) (hst hy)

Premises used: Set.Subsingleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Subsingleton
x : α
hx : x ∈ s
⊢ s = {x}

Tactic:
ext fun _ => ⟨fun hy => hs hx hy ▸ mem_singleton _, fun hy => (eq_of_mem_singleton hy).symm ▸ hx⟩

Premises used: Set.ext, Set.mem_singleton, Set.eq_of_mem_singleton, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
⊢ Set.Subsingleton.{u} (α := α) ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, Set.Subsingleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
⊢ Set.Subsingleton (α := α) {a}

Tactic:
fun _ hx _ hy =>
  (eq_of_mem_singleton hx).symm ▸ (eq_of_mem_singleton hy).symm ▸ rfl

Premises used: Set.eq_of_mem_singleton, Eq.rec, Set.Subsingleton, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s : Set α
h : s ⊆ {a}
⊢ s.Subsingleton

Tactic:
subsingleton_singleton.anti h

Premises used: Set.subsingleton_singleton, Set.Subsingleton.anti
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
a : α
h : ∀ (b : α), b ∈ s → b = a
⊢ s.Subsingleton

Tactic:
fun _ hb _ hc =>
  (h _ hb).trans (h _ hc).symm

Premises used: Set.Subsingleton, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hx : x ∈ s
⊢ s.Subsingleton ↔ s = {x}

Tactic:
⟨fun h => h.eq_singleton_of_mem hx, fun h => h.symm ▸ subsingleton_singleton⟩

Premises used: Eq.rec, Set.subsingleton_singleton, Set.Subsingleton.eq_singleton_of_mem, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Subsingleton
⊢ s = ∅ ∨ ∃ (x : α), s = {x}

Tactic:
s.eq_empty_or_nonempty.elim Or.inl fun ⟨x, hx⟩ => Or.inr ⟨x, hs.eq_singleton_of_mem hx⟩

Premises used: Exists, _private.0.Set.Subsingleton.eq_empty_or_singleton.match_1, Set.Subsingleton.eq_singleton_of_mem, Set.eq_empty_or_nonempty, Exists.intro, Or.inl, Or, EmptyCollection.emptyCollection, Or.elim, Singleton.singleton, Eq, Or.inr
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
h : s = ∅
⊢ s.Subsingleton

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
w : α
⊢ Set.Subsingleton (α := α) {w}

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
p : Set α → Prop
hs : s.Subsingleton
he : p ∅
h₁ : ∀ (x : α), p {x}
inl : ∀ (hs : Set.Subsingleton.{u} (α := α) ∅), p ∅
inr : ∀ (x : α) (hs : Set.Subsingleton (α := α) {x}), p {x}
⊢ p s

Tactic:
rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
hs : Set.Subsingleton.{u} (α := α) ∅
⊢ p ∅

Tactic:
he
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
x : α
hs : Set.Subsingleton (α := α) {x}
⊢ p {x}

Tactic:
h₁ _
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
hs : Set.Subsingleton.{u} (α := α) ∅
⊢ p ∅

Tactic:
exacts [he, h₁ _]
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : Subsingleton α
⊢ Set.Subsingleton.{u} (α := α) univ

Tactic:
fun x _ y _ =>
  Subsingleton.elim x y

Premises used: Set.Subsingleton, Subsingleton.elim
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
h : Set.Subsingleton.{u} (α := α) univ
⊢ Subsingleton α

Tactic:
⟨fun a b => h (mem_univ a) (mem_univ b)⟩

Premises used: Subsingleton.intro, Set.mem_univ
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
⊢ Set.Subsingleton.{u} (α := α) univ ↔ Subsingleton α

Tactic:
⟨subsingleton_of_univ_subsingleton, fun h => @subsingleton_univ _ h⟩

Premises used: Set.subsingleton_univ, Set.subsingleton_of_univ_subsingleton, Iff.intro
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s : Set α
⊢ (s ∩ {a}).Subsingleton

Tactic:
Set.subsingleton_of_subset_singleton Set.inter_subset_right

Premises used: Set.subsingleton_of_subset_singleton, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s : Set α
⊢ ({a} ∩ s).Subsingleton

Tactic:
Set.subsingleton_of_subset_singleton Set.inter_subset_left

Premises used: Set.inter_subset_left, Set.subsingleton_of_subset_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s t : Set α
h : (s ∪ t).Subsingleton
⊢ s.Subsingleton

Tactic:
fun _ h₁ _ h₂ ↦ h (.inl h₁) (.inl h₂)

Premises used: Set.Subsingleton, Or.inl
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s t : Set α
h : (s ∪ t).Subsingleton
⊢ t.Subsingleton

Tactic:
fun _ h₁ _ h₂ ↦ h (.inr h₁) (.inr h₂)

Premises used: Set.Subsingleton, Or.inr
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : Subsingleton α
s : Set α
⊢ s.Subsingleton

Tactic:
subsingleton_univ.anti (subset_univ s)

Premises used: Set.subsingleton_univ, Set.subset_univ, Set.Subsingleton.anti
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Set.Subsingleton.{u_1} (α := α) {x : α | IsTop x}

Tactic:
fun x hx _ hy => hx.isMax.eq_of_le (hy x)

Premises used: IsTop.isMax, IsMax.eq_of_le, Set.Subsingleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ (∃ (a : α), s = {a}) ↔ s.Nonempty ∧ s.Subsingleton

Tactic:
⟨?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
refine_1 : (∃ (a : α), s = {a}) → s.Nonempty ∧ s.Subsingleton
refine_2 : ∀ (h : s.Nonempty ∧ s.Subsingleton), ∃ (a : α), s = {a}
⊢ (∃ (a : α), s = {a}) ↔ s.Nonempty ∧ s.Subsingleton

Tactic:
refine ⟨?_, fun h => ?_⟩
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
⊢ Set.Nonempty (α := α) {a} ∧ Set.Subsingleton (α := α) {a}

Tactic:
⟨singleton_nonempty a, subsingleton_singleton⟩

Premises used: Set.singleton_nonempty, Set.subsingleton_singleton, And.intro
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
⊢ Set.Nonempty (α := α) {a} ∧ Set.Subsingleton (α := α) {a}

Tactic:
exact ⟨singleton_nonempty a, subsingleton_singleton⟩
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ (a : α), s = {a}

Tactic:
h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

Premises used: Set.Nonempty.ne_empty, Or.resolve_left, And.right, And.left, Set.Subsingleton.eq_empty_or_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ (a : α), s = {a}

Tactic:
exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

Premises used: Set.Nonempty.ne_empty, Or.resolve_left, And.right, And.left, Set.Subsingleton.eq_empty_or_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : Subsingleton α
s : Set α
⊢ s = ∅ ∨ ∃ (a : α), s = {a}

Tactic:
subsingleton_of_subsingleton.eq_empty_or_singleton

Premises used: Set.subsingleton_of_subsingleton, Set.Subsingleton.eq_empty_or_singleton