awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
x : (b : ι) → α b
⊢ Membership.mem (γ := Set ((b : ι) → α b))
      (preimage (β := (a : ι') → α ((f : (a : ι') → ι) a))
        (⇑(piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a))
        (s.pi (α := fun (a : ι') ↦ α ((f : (a : ι') → ι) a)) fun (i' : ι') ↦ t ((f : (a : ι') → ι) i')))
      x ↔
    x ∈ pi (α := α) ((⇑f : (a : ι') → ι) '' s) t

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ preimage (β := (a : ι') → α ((f : (a : ι') → ι) a))
      (⇑(piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a))
      (pi (α := fun (a : ι') ↦ α ((f : (a : ι') → ι) a)) univ fun (i' : ι') ↦ t ((f : (a : ι') → ι) i')) =
    pi (α := α) univ t

Tactic:
simpa [f.surjective.range_eq] using piCongrLeft_symm_preimage_pi f univ t

Premises used: Set.univ, Equiv.piCongrLeft_symm_preimage_pi, Function.Surjective.range_eq, Equiv.surjective
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
h :
  ∀ (x : (a : ι') → α ((f : (a : ι') → ι) a)),
    Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
        x ↔
      Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i)) x
⊢ Eq (α := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
    ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
      pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
    (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i))

Tactic:
apply Set.ext

Premises used: Set.ext
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
h :
  ∀ (a : (b : ι) → α b),
    Membership.mem (α := (a : ι') → α ((f : (a : ι') → ι) a)) (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
        (((piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a)) a :
          (a : ι') → α ((f : (a : ι') → ι) a)) ↔
      Membership.mem (α := (a : ι') → α ((f : (a : ι') → ι) a)) (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i))
        (((piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a)) a :
          (a : ι') → α ((f : (a : ι') → ι) a))
⊢ ∀ (x : (a : ι') → α ((f : (a : ι') → ι) a)),
    Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
        x ↔
      Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i)) x

Tactic:
rw [← (f.piCongrLeft α).symm.forall_congr_right]

Premises used: Equiv.piCongrLeft, Equiv.symm, Equiv.forall_congr_right
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (a : (b : ι) → α b),
    Membership.mem (α := (a : ι') → α ((f : (a : ι') → ι) a)) (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
        (((piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a)) a :
          (a : ι') → α ((f : (a : ι') → ι) a)) ↔
      Membership.mem (α := (a : ι') → α ((f : (a : ι') → ι) a)) (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i))
        (((piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a)) a :
          (a : ι') → α ((f : (a : ι') → ι) a))

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ Eq (α := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
    ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹' pi (α := α) univ t)
    (pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) univ fun (i : ι') ↦ t ((f : (a : ι') → ι) i))

Tactic:
simpa [f.surjective.range_eq] using piCongrLeft_preimage_pi f univ t

Premises used: Set.univ, Equiv.piCongrLeft_preimage_pi, Function.Surjective.range_eq, Equiv.surjective
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
h :
  ∀ (x : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))),
    Membership.mem (γ := Set (((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))))
        ((⇑(sumPiEquivProdPi π).symm :
            (a : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) → (i : ι ⊕ ι') → π i) ⁻¹'
          pi (α := π) univ t)
        x ↔
      x ∈
        SProd.sprod (α := Set ((i : ι) → π (Sum.inl i))) (β := Set ((i : ι') → π (Sum.inr i)))
          (pi (α := fun (i : ι) ↦ π (Sum.inl i)) univ fun (i : ι) ↦ t (Sum.inl i))
          (pi (α := fun (i : ι') ↦ π (Sum.inr i)) univ fun (i : ι') ↦ t (Sum.inr i))
⊢ (⇑(sumPiEquivProdPi π).symm : (a : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) → (i : ι ⊕ ι') → π i) ⁻¹'
      pi (α := π) univ t =
    SProd.sprod (α := Set ((i : ι) → π (Sum.inl i))) (β := Set ((i : ι') → π (Sum.inr i)))
      (pi (α := fun (i : ι) ↦ π (Sum.inl i)) univ fun (i : ι) ↦ t (Sum.inl i))
      (pi (α := fun (i : ι') ↦ π (Sum.inr i)) univ fun (i : ι') ↦ t (Sum.inr i))

Tactic:
ext
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ Membership.mem (γ := Set (((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))))
      ((⇑(sumPiEquivProdPi π).symm :
          (a : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) → (i : ι ⊕ ι') → π i) ⁻¹'
        pi (α := π) univ t)
      x ↔
    x ∈
      SProd.sprod (α := Set ((i : ι) → π (Sum.inl i))) (β := Set ((i : ι') → π (Sum.inr i)))
        (pi (α := fun (i : ι) ↦ π (Sum.inl i)) univ fun (i : ι) ↦ t (Sum.inl i))
        (pi (α := fun (i : ι') ↦ π (Sum.inr i)) univ fun (i : ι') ↦ t (Sum.inr i))

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : α × β
⊢ x ∈ graphOn f s ↔ x.1 ∈ s ∧ f x.1 = x.2

Tactic:
aesop (add simp graphOn)

Premises used: Set.graphOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ graphOn f ∅ = ∅

Tactic:
image_empty _

Premises used: Set.graphOn, Set.image_empty
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ graphOn f s = ∅ ↔ s = ∅

Tactic:
image_eq_empty

Premises used: Set.image_eq_empty, Set.graphOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ (graphOn f s).Nonempty ↔ s.Nonempty

Tactic:
image_nonempty

Premises used: Set.image_nonempty, Set.graphOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ graphOn f (s ∪ t) = graphOn f s ∪ graphOn f t

Tactic:
image_union ..

Premises used: Set.graphOn, Set.image_union
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ graphOn f {x} = {(x, f x)}

Tactic:
image_singleton ..

Premises used: Set.image_singleton, Set.graphOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
s : Set α
⊢ graphOn f (insert x s) = insert (x, f x) (graphOn f s)

Tactic:
image_insert_eq ..

Premises used: Set.graphOn, Set.image_insert_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Prod.fst '' graphOn f s = s

Tactic:
simp [graphOn, image_image]

Premises used: Set.image_image, Set.graphOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : ∀ (x : β), x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s
⊢ Prod.snd '' graphOn f s = f '' s

Tactic:
ext x
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : β
⊢ x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ InjOn Prod.fst (graphOn f s)

Tactic:
aesop (add simp InjOn)

Premises used: Set.InjOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
⊢ graphOn (g ∘ f) s = (fun (x : α × β) ↦ (x.1, g x.2)) '' graphOn f s

Tactic:
simpa using image_comp (fun x ↦ (x.1, g x.2)) (fun x ↦ (x, f x)) _

Premises used: Prod.mk, Set.image_comp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ graphOn f univ = range fun (x : α) ↦ (x, f x)

Tactic:
image_univ

Premises used: Set.image_univ, Set.graphOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
⊢ graphOn f s = graphOn g s ↔ EqOn f g s

Tactic:
simp [Set.ext_iff, forall_comm, EqOn]

Premises used: forall_comm, Set.EqOn, Set.ext_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn f s ×ˢ graphOn g t =
    (⇑(Equiv.prodProdProdComm α γ β δ) : (a : (α × γ) × β × δ) → (α × β) × γ × δ) ⁻¹' graphOn (Prod.map f g) (s ×ˢ t)

Tactic:
aesop
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn (Prod.map f g) (s ×ˢ t) =
    (⇑(Equiv.prodProdProdComm α β γ δ) : (a : (α × β) × γ × δ) → (α × γ) × β × δ) ⁻¹' graphOn f s ×ˢ graphOn g t

Tactic:
aesop
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ (f' : β → γ), range f = graphOn f' univ

Tactic:
⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩

Premises used: Exists.intro, Exists.choose, Prod.snd
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
refine : range f = graphOn (fun (h : β) ↦ (f (⋯.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ
⊢ ∃ (f' : β → γ), range f = graphOn f' univ

Tactic:
refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
h :
  ∀ (x : β × γ),
    x ∈ range f ↔
      Membership.mem (γ := Set (β × γ))
        (graphOn (fun (h : β) ↦ (f (⋯.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ) x
⊢ range f = graphOn (fun (h : β) ↦ (f (⋯.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ

Tactic:
ext x
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
h : (∃ (y : α), f y = x) ↔ (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = x.1) ⋯)).2 = x.2
⊢ x ∈ range f ↔
    Membership.mem (γ := Set (β × γ))
      (graphOn (fun (h : β) ↦ (f (⋯.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ) x

Tactic:
simp only [mem_range, comp_apply, mem_graphOn, mem_univ, true_and]

Premises used: Set.mem_range, Set.mem_graphOn, Set.mem_univ, Function.comp_apply, true_and
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ (y : α), f y = x) ↔ (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = x.1) ⋯)).2 = x.2

Tactic:
⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩

Premises used: Exists.choose_spec, Prod.fst, Prod.ext, Iff.intro, Exists.intro, Exists.choose
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
h : (∃ (y : α), f y = x) → (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = x.1) ⋯)).2 = x.2
⊢ (∃ (y : α), f y = x) ↔ (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = x.1) ⋯)).2 = x.2

Tactic:
refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
g : α
⊢ (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = (f g).1) ⋯)).2 = (f g).2

Tactic:
hf _ _ (hf₁ (f g).1).choose_spec

Premises used: Exists.choose_spec, Prod.fst
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
g : α
⊢ (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = (f g).1) ⋯)).2 = (f g).2

Tactic:
exact hf _ _ (hf₁ (f g).1).choose_spec

Premises used: Exists.choose_spec, Prod.fst
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
obtain : ∀ (e₁ : β → γ) (he₁ : range f = graphOn e₁ univ), ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ
⊢ ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ

Tactic:
obtain ⟨e₁, he₁⟩ := exists_range_eq_graphOn_univ hf₁ fun _ _ ↦ (hf _ _).1

Premises used: Set.exists_range_eq_graphOn_univ, Iff.mp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ Surjective.{u_1 + 1, u_3 + 1} (β := γ)
    (comp (β := γ × β) Prod.fst ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f))

Tactic:
simpa
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ ∀ (g₁ g₂ : α),
    Eq.{u_3 + 1} (α := γ) (((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) g₁).1
        (((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) g₂).1 →
      Eq.{u_2 + 1} (α := β) (((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) g₁).2
        (((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) g₂).2

Tactic:
simp [hf]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
obtain :
  ∀ (e₂ : γ → β) (he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ),
    ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ
⊢ ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ

Tactic:
obtain ⟨e₂, he₂⟩ := exists_range_eq_graphOn_univ (f := Equiv.prodComm _ _ ∘ f) (by simpa) <|
    by simp [hf]

Premises used: Set.exists_range_eq_graphOn_univ
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
h : β
i : γ
rw :
  ∀ (he₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ) (e₂ : γ → β)
    (he₂ :
      ∀ (x : γ × β),
        Membership.mem (γ := Set (γ × β)) (range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f)) x ↔
          x ∈ graphOn e₂ univ)
    (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
rw [Set.ext_iff] at he₁ he₂

Premises used: Set.ext_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ
e₂ : γ → β
he₂ :
  ∀ (x : γ × β),
    Membership.mem (γ := Set (γ × β)) (range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f)) x ↔
      x ∈ graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
aesop (add simp [Prod.swap_eq_iff_eq_swap])

Premises used: Prod.swap_eq_iff_eq_swap
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
⊢ ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h

Tactic:
have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [Set.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
h : β
rw rw₁ : e₁ h = e₁ h
⊢ e₂ (e₁ h) = h

Tactic:
rw [← he₁₂]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
i : γ
rw rw₁ : e₂ i = e₂ i
⊢ e₁ (e₂ i) = i

Tactic:
rw [he₁₂]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
⊢ ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ

Tactic:
exact ⟨
  { toFun := e₁
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
β : Type u_2
γ : Type u_3
s : Set (β × γ)
hs₁ : Bijective (α := { x : β × γ // x ∈ s }) (Prod.fst ∘ Subtype.val (p := fun (x : β × γ) ↦ x ∈ s))
⊢ ∃ (f : β → γ), s = graphOn f univ

Tactic:
simpa using exists_range_eq_graphOn_univ hs₁.surjective
    fun a b h ↦ congr_arg (Prod.snd ∘ (Subtype.val : s → β × γ)) (hs₁.injective h)

Premises used: Function.comp, Function.Bijective.injective, congr_arg, Set.exists_range_eq_graphOn_univ, Function.Bijective.surjective, Subtype.val, Prod.snd
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
π : α → Type u_6
s : Set α
⊢ Eq (α := (f : (a : α) → π a) → (a : (↑s : Type u_1)) → π (↑a : α)) (s.restrict (π := π))
    fun (f : (a : α) → π a) (x : (↑s : Type u_1)) ↦ f (↑x : α)

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ s.restrict (π := fun (a : α) ↦ β) f = f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
s : Set α
⊢ s.restrict (π := fun (a : α) ↦ α) id = Subtype.val (p := fun (x : α) ↦ x ∈ s)

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
π : α → Type u_6
f : (a : α) → π a
s : Set α
x : (↑s : Type u_1)
⊢ s.restrict (π := π) f x = f (↑x : α)

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
π : α → Type u_6
f : (a : α) → π a
s : Set α
g : (a : (↑s : Type u_1)) → π (↑a : α)
⊢ s.restrict (π := π) f = g ↔ ∀ (a : α) (ha : a ∈ s), f a = g (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha)

Tactic:
funext_iff.trans Subtype.forall

Premises used: funext_iff, Subtype.forall, Iff.trans
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
π : α → Type u_6
s : Set α
f : (a : (↑s : Type u_1)) → π (↑a : α)
g : (a : α) → π a
⊢ f = s.restrict (π := π) g ↔ ∀ (a : α) (ha : a ∈ s), f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = g a

Tactic:
funext_iff.trans Subtype.forall

Premises used: funext_iff, Subtype.forall, Iff.trans
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ range (s.restrict (π := fun (a : α) ↦ β) f) = f '' s

Tactic:
(range_comp _ _).trans <| congr_arg (f '' ·) Subtype.range_coe

Premises used: Set.range_comp, Subtype.range_coe, congr_arg, Set.image, Set.restrict, Eq.trans
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
rw :
  image (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    f '' (t ∩ s)
rw₁ :
  f ''
      image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    f '' (t ∩ s)
rw₂ : f '' (t ∩ range (ι := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = f '' (t ∩ s)
rw₃ rw₄ : f '' (t ∩ s) = f '' (t ∩ s)
⊢ s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t = f '' (t ∩ s)

Tactic:
rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]

Premises used: Subtype.range_coe, Set.image_preimage_eq_inter_range, Set.restrict_eq, Set.image_comp
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (x : α) → Decidable (x ∈ s)
f : (a : α) → a ∈ s → β
g : (a : α) → ¬a ∈ s → β
⊢ Eq (α := (a : (↑s : Type u_1)) → β)
    (s.restrict (π := fun (a : α) ↦ β) fun (a : α) ↦ if h : a ∈ s then f a h else g a h : (a : (↑s : Type u_1)) → β)
    fun (a : (↑s : Type u_1)) ↦ f (↑a : α) ⋯

Tactic:
funext fun a => dif_pos a.2

Premises used: dif_pos, funext, Subtype.property
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (x : α) → Decidable (x ∈ s)
f : (a : α) → a ∈ s → β
g : (a : α) → ¬a ∈ s → β
⊢ Eq (α := (a : (↑sᶜ : Type u_1)) → β)
    (sᶜ.restrict (π := fun (a : α) ↦ β) fun (a : α) ↦ if h : a ∈ s then f a h else g a h : (a : (↑sᶜ : Type u_1)) → β)
    fun (a : (↑sᶜ : Type u_1)) ↦ g (↑a : α) ⋯

Tactic:
funext fun a => dif_neg a.2

Premises used: dif_neg, funext, Subtype.property
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
inst : (x : α) → Decidable (x ∈ s)
⊢ (s.restrict (π := fun (a : α) ↦ β) fun (a : α) ↦ if a ∈ s then f a else g a) = s.restrict (π := fun (a : α) ↦ β) f

Tactic:
restrict_dite _ _

Premises used: Set.restrict_dite, Set.restrict, ite
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
inst : (x : α) → Decidable (x ∈ s)
⊢ (sᶜ.restrict (π := fun (a : α) ↦ β) fun (a : α) ↦ if a ∈ s then f a else g a) = sᶜ.restrict (π := fun (a : α) ↦ β) g

Tactic:
restrict_dite_compl _ _

Premises used: Set.restrict_dite_compl, Set.restrict, ite
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
inst : (x : α) → Decidable (x ∈ s)
⊢ s.restrict (π := fun (i : α) ↦ β) (s.piecewise (β := fun (i : α) ↦ β) f g) = s.restrict (π := fun (a : α) ↦ β) f

Tactic:
restrict_ite _ _ _

Premises used: Set.restrict_ite, Set.piecewise