awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
hf : EqOn f f' s
hg : EqOn g g' t
⊢ EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)

Tactic:
grind [EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f f' : α → γ
g g' : β → δ
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t) ↔ EqOn f f' s ∧ EqOn g g' t

Tactic:
⟨fun h ↦ ⟨h.left_of_eqOn_prodMap ht, h.right_of_eqOn_prodMap hs⟩, fun ⟨h, h'⟩ ↦ h.prodMap h'⟩

Premises used: Set.EqOn.prodMap, SProd.sprod, Set.EqOn.right_of_eqOn_prodMap, Prod.map, Set.EqOn.left_of_eqOn_prodMap, Set.EqOn, And.intro, Iff.intro, _private.0.Set.eqOn_prodMap_iff.match_1
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
inst : Nonempty α
⊢ (diagonal α).Nonempty

Tactic:
Nonempty.elim ‹_› fun x => ⟨_, mem_diagonal x⟩

Premises used: Nonempty.elim, Prod.mk, Exists.intro, Set.mem_diagonal
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
h :
  ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s),
    Membership.mem (γ := Set ((↑s : Type u_1) × (↑s : Type u_1)))
        ((Prod.map (fun (x : (↑s : Type u_1)) ↦ (↑x : α)) fun (x : (↑s : Type u_1)) ↦ (↑x : α)) ⁻¹' diagonal α)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx, Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy) ↔
      Membership.mem (γ := Set ((↑s : Type u_1) × (↑s : Type u_1))) (diagonal (↑s : Type u_1))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx, Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
⊢ Eq (α := Set ((↑s : Type u_1) × (↑s : Type u_1)))
    ((Prod.map (fun (x : (↑s : Type u_1)) ↦ (↑x : α)) fun (x : (↑s : Type u_1)) ↦ (↑x : α)) ⁻¹' diagonal α)
    (diagonal (↑s : Type u_1))

Tactic:
ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ Membership.mem (γ := Set ((↑s : Type u_1) × (↑s : Type u_1)))
      ((Prod.map (fun (x : (↑s : Type u_1)) ↦ (↑x : α)) fun (x : (↑s : Type u_1)) ↦ (↑x : α)) ⁻¹' diagonal α)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx, Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy) ↔
    Membership.mem (γ := Set ((↑s : Type u_1) × (↑s : Type u_1))) (diagonal (↑s : Type u_1))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx, Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)

Tactic:
simp [Set.diagonal]

Premises used: Set.diagonal
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
h : ∀ (x y : α), Membership.mem (γ := Set (α × α)) (range fun (x : α) ↦ (x, x)) (x, y) ↔ (x, y) ∈ diagonal α
⊢ (range fun (x : α) ↦ (x, x)) = diagonal α

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
x y : α
⊢ Membership.mem (γ := Set (α × α)) (range fun (x : α) ↦ (x, x)) (x, y) ↔ (x, y) ∈ diagonal α

Tactic:
simp [diagonal, eq_comm]

Premises used: eq_comm, Set.diagonal
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set (α × α)
rw : (range fun (x : α) ↦ (x, x)) ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
rw₁ rw₂ : (∀ (y : α), (y, y) ∈ s) ↔ ∀ (x : α), (x, x) ∈ s
⊢ diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s

Tactic:
rw [← range_diag, range_subset_iff]

Premises used: Set.range_diag, Set.range_subset_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
⊢ s ×ˢ t ⊆ (diagonal α)ᶜ ↔ Disjoint s t

Tactic:
prod_subset_iff.trans disjoint_iff_forall_ne.symm

Premises used: Set.prod_subset_iff, Set.disjoint_iff_forall_ne, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
⊢ (fun (x : α) ↦ (x, x)) ⁻¹' s ×ˢ t = s ∩ t

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.inter, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
⊢ (fun (x : α) ↦ (x, x)) ⁻¹' s ×ˢ s = s

Tactic:
inter_self s

Premises used: Set.Mem, Set.inter_self, setOf, Set.prod, Set.inter, Set.preimage
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
rw : (fun (x : α) ↦ (x, x)) '' s = (range fun (x : α) ↦ (x, x)) ∩ s ×ˢ s
rw₁ : Eq (α := Set (α × α)) ((fun (x : α) ↦ (x, x)) '' s) ((fun (x : α) ↦ (x, x)) '' (fun (x : α) ↦ (x, x)) ⁻¹' s ×ˢ s)
rw₂ rw₃ : Eq (α := Set (α × α)) ((fun (x : α) ↦ (x, x)) '' s) ((fun (x : α) ↦ (x, x)) '' s)
⊢ (fun (x : α) ↦ (x, x)) '' s = diagonal α ∩ s ×ˢ s

Tactic:
rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]

Premises used: Set.image_preimage_eq_range_inter, Set.range_diag, Set.diag_preimage_prod_self
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
⊢ diagonal α = univ ↔ Subsingleton α

Tactic:
simp only [subsingleton_iff, eq_univ_iff_forall, Prod.forall, mem_diagonal_iff]

Premises used: subsingleton_iff, Set.eq_univ_iff_forall, Set.mem_diagonal_iff, Prod.forall
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
inst : Subsingleton α
⊢ diagonal α = univ

Tactic:
diagonal_eq_univ_iff.2 ‹_›

Premises used: Iff.mpr, Set.diagonal_eq_univ_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
⊢ Eq (α := Set (α → β)) (range (const α)) {f : α → β | ∀ (x y : α), f x = f y}

Tactic:
(range_eq_iff _ _).mpr ⟨fun _ _ _ ↦ rfl, fun f hf ↦ ?_⟩

Premises used: Iff.mpr, And.intro, rfl, Set.range_eq_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
refine :
  ∀ (f : α → β) (hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f),
    ∃ (a : β), const α a = f
⊢ Eq (α := Set (α → β)) (range (const α)) {f : α → β | ∀ (x y : α), f x = f y}

Tactic:
refine (range_eq_iff _ _).mpr ⟨fun _ _ _ ↦ rfl, fun f hf ↦ ?_⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f
inl : ∀ (h : IsEmpty α), ∃ (a : β), const α a = f
inr : ∀ (a : α), ∃ (a : β), const α a = f
⊢ ∃ (a : β), const α a = f

Tactic:
rcases isEmpty_or_nonempty α with h | ⟨⟨a⟩⟩

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f
h : IsEmpty α
⊢ ∃ (a : β), const α a = f

Tactic:
hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩

Premises used: Nonempty.elim, Exists.intro, Function.const, Subsingleton.elim
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f
h : IsEmpty α
⊢ ∃ (a : β), const α a = f

Tactic:
exact hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩

Premises used: Nonempty.elim
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f
a : α
⊢ ∃ (a : β), const α a = f

Tactic:
⟨f a, funext fun x ↦ hf _ _⟩

Premises used: funext, Exists.intro
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f
a : α
⊢ ∃ (a : β), const α a = f

Tactic:
exact ⟨f a, funext fun x ↦ hf _ _⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
⊢ Eq (α := Pullback f g → Y) (f ∘ fst) (g ∘ snd)

Tactic:
funext fun p ↦ p.2

Premises used: funext, Subtype.property
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
h :
  ∀ (p₁ p₂ : Pullback f g) (he : (p₁, p₂).1.snd = (p₁, p₂).2.snd),
    Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' pullbackDiagonal f)
        (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
      Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (pullbackDiagonal snd)
        (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)
⊢ Eq (α := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' pullbackDiagonal f) (pullbackDiagonal snd)

Tactic:
ext ⟨⟨p₁, p₂⟩, he⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
h :
  Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' {p : Pullback f f | p.fst = p.snd})
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
    (↑(fst (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).1 =
        (↑(snd (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).1 ∧
      (↑(fst (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).2 =
        (↑(snd (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).2
⊢ Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' pullbackDiagonal f)
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
    Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (pullbackDiagonal snd)
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)

Tactic:
simp_rw [pullbackDiagonal, mem_setOf, Subtype.ext_iff, Prod.ext_iff]

Premises used: Prod.ext_iff, Set.mem_setOf, Subtype.ext_iff, Function.pullbackDiagonal
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' {p : Pullback f f | p.fst = p.snd})
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
    (↑(fst (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).1 =
        (↑(snd (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).1 ∧
      (↑(fst (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).2 =
        (↑(snd (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).2

Tactic:
(and_iff_left he).symm

Premises used: Set.Mem, setOf, and_iff_left, Function.Pullback.fst, Function.Pullback.snd, Set.preimage, Iff.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' {p : Pullback f f | p.fst = p.snd})
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
    (↑(fst (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).1 =
        (↑(snd (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).1 ∧
      (↑(fst (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).2 =
        (↑(snd (Y := Z) (f := snd) (g := snd)
                (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
            X × Z).2

Tactic:
exact (and_iff_left he).symm

Premises used: and_iff_left, Iff.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → X
inj : Injective g
⊢ f ∘ g = id ∘ f ∘ g

Tactic:
rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → X
inj : Injective g
⊢ mapPullback g id g ⋯ ⋯ ⁻¹' pullbackDiagonal f = pullbackDiagonal (f ∘ g)

Tactic:
ext fun _ ↦ inj.eq_iff

Premises used: Set.ext, Function.Injective.eq_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
h :
  ∀ (x : Pullback f f),
    x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
⊢ toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s

Tactic:
ext x
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
h : x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
h₁ : x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s
⊢ x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s

Tactic:
constructor
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
hx : x ∈ s
⊢ toPullbackDiag f x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s

Tactic:
⟨rfl, hx, hx⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
hx : x ∈ s
⊢ toPullbackDiag f x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s

Tactic:
exact ⟨rfl, hx, hx⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
h :
  ∀ (x y : X) (h : f (x, y).1 = f (x, y).2),
    Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, y) h ∈
        pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s →
      Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, y) h ∈ toPullbackDiag f '' s
⊢ x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s

Tactic:
obtain ⟨⟨x, y⟩, h⟩ := x
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
h : f (x, x).1 = f (x, x).2
h2x :
  Membership.mem (γ := Set (Pullback f f)) (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s)
    (Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, x) h)
⊢ Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, x) h ∈ toPullbackDiag f '' s

Tactic:
mem_image_of_mem _ h2x.1

Premises used: Set.Mem, toPullbackDiag, And.left, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
h : f (x, x).1 = f (x, x).2
h2x :
  Membership.mem (γ := Set (Pullback f f)) (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s)
    (Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, x) h)
⊢ Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, x) h ∈ toPullbackDiag f '' s

Tactic:
exact mem_image_of_mem _ h2x.1

Premises used: And.left, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
rw : toPullbackDiag f '' univ = pullbackDiagonal f
rw₁ :
  pullbackDiagonal f ∩
      Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' SProd.sprod (α := Set X) (β := Set X) univ univ =
    pullbackDiagonal f
rw₂ : pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' univ = pullbackDiagonal f
rw₃ : pullbackDiagonal f ∩ univ = pullbackDiagonal f
rw₄ rw₅ : pullbackDiagonal f = pullbackDiagonal f
⊢ range (toPullbackDiag f) = pullbackDiagonal f

Tactic:
rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]

Premises used: Set.image_univ, Set.inter_univ, Set.univ_prod_univ, Set.preimage_univ, image_toPullbackDiag
-- Module: Mathlib.Data.Set.Prod
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
⊢ Injective (toPullbackDiag f)

Tactic:
fun _ _ h ↦ congr_arg Prod.fst (congr_arg Subtype.val h)

Premises used: Prod.fst, congr_arg, Function.Injective, Subtype.val
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Set α) offDiag

Tactic:
fun _ _ h _ =>
  And.imp (@h _) <| And.imp_left <| @h _

Premises used: And.imp, Set.Mem, Monotone, setOf, Set.offDiag, And.imp_left, Set.Subset
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
⊢ s.offDiag.Nonempty ↔ s.Nontrivial

Tactic:
simp [offDiag, Set.Nonempty, Set.Nontrivial]

Premises used: Set.offDiag, Set.Nonempty, Set.Nontrivial
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
rw : ¬s.offDiag.Nonempty ↔ s.Subsingleton
rw₁ : ¬s.offDiag.Nonempty ↔ ¬s.Nontrivial
rw₂ rw₃ : ¬s.Nontrivial ↔ ¬s.Nontrivial
⊢ s.offDiag = ∅ ↔ s.Subsingleton

Tactic:
rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]

Premises used: Set.offDiag_nonempty, Set.not_nonempty_iff_eq_empty, Iff.not, Set.not_nontrivial_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
⊢ s.offDiag ⊆ s ×ˢ s

Tactic:
fun _ hx => ⟨hx.1, hx.2.1⟩

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
⊢ s.offDiag = {x : α × α | x ∈ s ×ˢ s ∧ x.1 ≠ x.2}

Tactic:
ext fun _ => and_assoc.symm

Premises used: Set.ext, and_assoc, Iff.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (α × α)) (offDiag ∅) ∅

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set (α × α)) (offDiag {a}) ∅

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
⊢ ∀ (x : α × α), Membership.mem (γ := Set (α × α)) (offDiag univ) x ↔ x ∈ (diagonal α)ᶜ

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
⊢ s ×ˢ s \ diagonal α = s.offDiag

Tactic:
ext fun _ => and_assoc

Premises used: Set.ext, and_assoc
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
⊢ Disjoint (diagonal α) s.offDiag

Tactic:
disjoint_left.mpr fun _ hd ho => ho.2.2 hd

Premises used: Iff.mpr, Set.disjoint_left, And.right
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
mp₈ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mpr₁ mpr₂ :
  x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mpr₃ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ s
mpr₄ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ t
mpr₅ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.2 ∈ s
mpr₆ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.2 ∈ t
mpr₇ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ≠ x.2
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2

Tactic:
tauto
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
h₁ : ∀ (x : α × α), x ∈ (s ∪ t).offDiag ↔ x ∈ s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
⊢ (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Tactic:
ext x
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h₁ :
  (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
h₂ :
  ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
constructor
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ s
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
simp [*, h.ne_of_mem, Ne.symm]

Premises used: Ne.symm, Disjoint.ne_of_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ t
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
simp [*, h.ne_of_mem, Ne.symm]

Premises used: Ne.symm, Disjoint.ne_of_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
simp [*, h.ne_of_mem, Ne.symm]

Premises used: Ne.symm, Disjoint.ne_of_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
simp [*, h.ne_of_mem, Ne.symm]

Premises used: Ne.symm, Disjoint.ne_of_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s : Set α
a : α
ha : ¬a ∈ s
⊢ (insert a s).offDiag = s.offDiag ∪ SProd.sprod (α := Set α) {a} s ∪ SProd.sprod (β := Set α) s {a}

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
⊢ pi (α := α) ∅ s = univ

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), (t i).Subsingleton
⊢ (pi (α := α) univ t).Subsingleton

Tactic:
fun _f hf _g hg ↦ funext fun i ↦
  (ht i) (hf _ <| mem_univ _) (hg _ <| mem_univ _)

Premises used: funext, Set.Subsingleton, Set.mem_univ
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
⊢ Eq (α := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ univ) univ

Tactic:
eq_univ_of_forall fun _ _ _ => mem_univ _

Premises used: Set.eq_univ_of_forall, Set.mem_univ
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst : DecidablePred fun (x : ι) ↦ x ∈ s
t : (i : ι) → Set (α i)
⊢ (pi (α := α) univ fun (i : ι) ↦ if i ∈ s then t i else univ) = s.pi (α := α) t

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : ∀ (i : ι), i ∈ s₂ → t₁ i ⊆ t₂ i
h' : s₂ ⊆ s₁
⊢ s₁.pi (α := α) t₁ ⊆ s₂.pi (α := α) t₂

Tactic:
fun _ hx i hi ↦ h i hi (hx i (h' hi))

Premises used: Set.Mem, setOf, Set.Subset, Set.pi