awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a).get ⋯ = x) → C a) ((f a).get ⋯)
      (fun (b' : β) (e : (f a).get ⋯ = Sum.inl b') ↦
        have e := ⋯;
        hbase a ⋯)
      (fun (a'' : α) (e : (f a).get ⋯ = Sum.inr a'') ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun (x : α) (h' : Sum.inr x ∈ f a) ↦
              (fixInduction (C := fun (x : α) ↦ C x) ⋯
                  fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a'') ↦
                  Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → C a') ((f a').get ⋯)
                    (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
                      have e := ⋯;
                      hbase a' ⋯)
                    (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
                      have e := ⋯;
                      hind a' a'' ⋯ e (ih a'' e))
                    ⋯ :
                C x))
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction (C := fun (x : α) ↦ (fun (x : α) ↦ C x) x) h'
        fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → (fun (x : α) ↦ C x) a'') ↦
        Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → (fun (x : α) ↦ C x) a') ((f a').get ⋯)
          (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Tactic:
Eq.rec (motive := fun x e =>
      Sum.casesOn (motive := fun y => (f a).get (dom_of_mem_fix h) = y → C a) x ?_ ?_
      (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = _) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm

Premises used: Part.get_eq_of_mem, Eq.rec, Eq.symm, PFun.dom_of_mem_fix
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fun (x : β ⊕ α) (e : Sum.inr a' = x) ↦
      Sum.casesOn (motive := fun (y : β ⊕ α) ↦ (f a).get ⋯ = y → C a) x
          (fun (b' : β) (e : (f a).get ⋯ = Sum.inl b') ↦
            have e := ⋯;
            hbase a ⋯)
          (fun (a'' : α) (e : (f a).get ⋯ = Sum.inr a'') ↦
            have e := ⋯;
            hind a a'' ⋯ e
              ((fun (x : α) (h' : Sum.inr x ∈ f a) ↦
                  (fixInduction (C := fun (x : α) ↦ C x) ⋯
                      fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a'') ↦
                      Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → C a') ((f a').get ⋯)
                        (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
                          have e := ⋯;
                          hbase a' ⋯)
                        (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
                          have e := ⋯;
                          hind a' a'' ⋯ e (ih a'' e))
                        ⋯ :
                    C x))
                a'' e))
          ⋯ =
        hind a a' h' fa
          (fixInduction (C := fun (x : α) ↦ (fun (x : α) ↦ C x) x) h'
            fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → (fun (x : α) ↦ C x) a'') ↦
            Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → (fun (x : α) ↦ C x) a') ((f a').get ⋯)
              (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
                have e := ⋯;
                hbase a' ⋯)
              (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
                have e := ⋯;
                hind a' a'' ⋯ e (ih a'' e))
              ⋯))
    (Sum.inr a') ⋯

Tactic:
simp
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set α
⊢ f.image s = {y : β | ∃ (x : α), x ∈ s ∧ y ∈ f x}

Tactic:
rfl

Premises used: PFun.graph', Part.Mem, Set.Mem, setOf, PFun.image, SetRel.image, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
y : β
s : Set α
⊢ y ∈ f.image s ↔ ∃ (x : α), x ∈ s ∧ y ∈ f x

Tactic:
Iff.rfl

Premises used: PFun.graph', Part.Mem, Set.Mem, Iff.rfl, setOf, PFun.image, SetRel.image
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set α
h : s ⊆ t
⊢ f.image s ⊆ f.image t

Tactic:
SetRel.image_mono h

Premises used: PFun.image, SetRel.image_mono
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set α
⊢ f.image (s ∩ t) ⊆ f.image s ∩ f.image t

Tactic:
SetRel.image_inter_subset _

Premises used: PFun.image, SetRel.image_inter_subset
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set α
⊢ f.image (s ∪ t) = f.image s ∪ f.image t

Tactic:
SetRel.image_union _ s t

Premises used: PFun.image, SetRel.image_union
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.preimage s = {x : α | ∃ (y : β), y ∈ s ∧ y ∈ f x}

Tactic:
rfl

Premises used: PFun.graph', Part.Mem, Set.Mem, setOf, SetRel.preimage, rfl, PFun.preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : α
⊢ x ∈ f.preimage s ↔ ∃ (y : β), y ∈ s ∧ y ∈ f x

Tactic:
Iff.rfl

Premises used: PFun.graph', Part.Mem, Set.Mem, Iff.rfl, setOf, SetRel.preimage, PFun.preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.preimage s ⊆ f.Dom

Tactic:
fun _ ⟨y, _, fxy⟩ =>
  Part.dom_iff_mem.mpr ⟨y, fxy⟩

Premises used: Iff.mpr, Membership.mem, _private.0.PFun.preimage_subset_dom.match_1, Part.dom_iff_mem, Set.Subset, Exists.intro, PFun.Dom
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set β
h : s ⊆ t
⊢ f.preimage s ⊆ f.preimage t

Tactic:
SetRel.preimage_mono h

Premises used: SetRel.preimage_mono, PFun.preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set β
⊢ f.preimage (s ∩ t) ⊆ f.preimage s ∩ f.preimage t

Tactic:
SetRel.preimage_inter_subset _

Premises used: SetRel.preimage_inter_subset, PFun.preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set β
⊢ f.preimage (s ∪ t) = f.preimage s ∪ f.preimage t

Tactic:
SetRel.preimage_union _ s t

Premises used: SetRel.preimage_union, PFun.preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
h : ∀ (x : α), x ∈ f.preimage Set.univ ↔ x ∈ f.Dom
⊢ f.preimage Set.univ = f.Dom

Tactic:
ext
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
x : α
⊢ x ∈ f.preimage Set.univ ↔ x ∈ f.Dom

Tactic:
simp [mem_preimage, mem_dom]

Premises used: PFun.mem_dom, PFun.mem_preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), x ∈ (↑f : α →. β).preimage s ↔ x ∈ f ⁻¹' s
⊢ (↑f : α →. β).preimage s = f ⁻¹' s

Tactic:
ext
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x : α
⊢ x ∈ (↑f : α →. β).preimage s ↔ x ∈ f ⁻¹' s

Tactic:
simp
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = {x : α | ∀ (y : β), y ∈ f x → y ∈ s}

Tactic:
rfl

Premises used: PFun.graph', Part.Mem, Set.Mem, setOf, PFun.core, SetRel.core, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
x : α
s : Set β
⊢ x ∈ f.core s ↔ ∀ (y : β), y ∈ f x → y ∈ s

Tactic:
Iff.rfl

Premises used: PFun.graph', Part.Mem, Set.Mem, Iff.rfl, setOf, PFun.core, SetRel.core
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.Domᶜ ⊆ f.core s

Tactic:
fun x hx y fxy =>
  absurd ((mem_dom f x).mpr ⟨y, fxy⟩) hx

Premises used: Iff.mpr, Set.Mem, setOf, PFun.mem_dom, PFun.core, Set.Subset, SetRel.core, absurd, Exists.intro
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set β
h : s ⊆ t
⊢ f.core s ⊆ f.core t

Tactic:
SetRel.core_mono h

Premises used: SetRel.core_mono, PFun.core
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s t : Set β
⊢ f.core (s ∩ t) = f.core s ∩ f.core t

Tactic:
SetRel.core_inter _ s t

Premises used: PFun.core, SetRel.core_inter
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ s → f x ∈ t

Tactic:
simp [mem_core, mem_res]

Premises used: PFun.mem_core, PFun.mem_res
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : ∀ (x : α), x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t
⊢ (res f s).core t = sᶜ ∪ f ⁻¹' t

Tactic:
ext x
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h : x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
⊢ x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
rw [mem_core_res]

Premises used: PFun.mem_core_res
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
pos : ∀ (h : x ∈ s), x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
neg : ∀ (h : ¬x ∈ s), x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
by_cases h : x ∈ s
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h : x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
simp [h]
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h : ¬x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
simp [h]
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), x ∈ (↑f : α →. β).core s ↔ x ∈ f ⁻¹' s
⊢ (↑f : α →. β).core s = f ⁻¹' s

Tactic:
ext x
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x : α
⊢ x ∈ (↑f : α →. β).core s ↔ x ∈ f ⁻¹' s

Tactic:
simp [core_def]

Premises used: PFun.core_def
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.preimage s ⊆ f.core s

Tactic:
fun _ ⟨y, ys, fxy⟩ y' fxy' =>
  have : y = y' := Part.mem_unique fxy fxy'
  this ▸ ys

Premises used: Set.Mem, setOf, Membership.mem, _private.0.PFun.preimage_subset_dom.match_1, Eq.rec, PFun.core, Set.Subset, SetRel.core, Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.preimage s = f.core s ∩ f.Dom

Tactic:
Set.eq_of_subset_of_subset (Set.subset_inter (f.preimage_subset_core s) (f.preimage_subset_dom s))
    fun x ⟨xcore, xdom⟩ =>
    let y := (f x).get xdom
    have ys : y ∈ s := xcore (Part.get_mem _)
    show x ∈ f.preimage s from ⟨(f x).get xdom, ys, Part.get_mem _⟩

Premises used: Membership.mem, Part.get_mem, Part.get, Set.subset_inter, And.intro, PFun.preimage_subset_dom, Exists.intro, _private.0.PFun.preimage_eq.match_1, PFun.preimage_subset_core, Set.eq_of_subset_of_subset, PFun.preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
rw : f.core s = f.core s ∩ f.Dom ∪ f.Domᶜ
rw₁ : f.core s = (f.core s ∪ f.Domᶜ) ∩ (f.Dom ∪ f.Domᶜ)
rw₂ : f.core s = (f.core s ∪ f.Domᶜ) ∩ (f.Domᶜ ∪ f.Dom)
rw₃ : f.core s = (f.core s ∪ f.Domᶜ) ∩ Set.univ
rw₄ : f.core s = f.core s ∪ f.Domᶜ
rw₅ rw₆ : f.core s = f.core s
⊢ f.core s = f.preimage s ∪ f.Domᶜ

Tactic:
rw [preimage_eq, Set.inter_union_distrib_right, Set.union_comm (Dom f), Set.compl_union_self,
    Set.inter_univ, Set.union_eq_self_of_subset_right (f.compl_dom_subset_core s)]

Premises used: PFun.preimage_eq, Set.inter_univ, Set.union_eq_self_of_subset_right, Set.inter_union_distrib_right, Set.union_comm, PFun.compl_dom_subset_core, Set.compl_union_self, PFun.Dom
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
h :
  ∀ (x : (↑f.Dom : Type u_1)),
    x ∈ f.asSubtype ⁻¹' s ↔
      Membership.mem (γ := Set (↑f.Dom : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ f.Dom) ⁻¹' f.preimage s) x
⊢ f.asSubtype ⁻¹' s = Subtype.val (p := fun (x : α) ↦ x ∈ f.Dom) ⁻¹' f.preimage s

Tactic:
ext x
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : (↑f.Dom : Type u_1)
h : f.fn (↑x : α) ⋯ ∈ s ↔ ∃ (y : β), y ∈ s ∧ y ∈ f (↑x : α)
⊢ x ∈ f.asSubtype ⁻¹' s ↔
    Membership.mem (γ := Set (↑f.Dom : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ f.Dom) ⁻¹' f.preimage s) x

Tactic:
simp only [Set.mem_preimage, PFun.asSubtype, PFun.mem_preimage]

Premises used: PFun.asSubtype, Set.mem_preimage, PFun.mem_preimage
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : (↑f.Dom : Type u_1)
⊢ f.fn (↑x : α) ⋯ ∈ s ↔ ∃ (y : β), y ∈ s ∧ y ∈ f (↑x : α)

Tactic:
Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
      have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
      Part.mem_unique fxy this ▸ ys

Premises used: _private.0.PFun.preimage_asSubtype.match_3, Membership.mem, Eq.rec, Part.get_mem, PFun.fn, PFun.asSubtype._proof_1, And.intro, Iff.intro, Exists.intro, Subtype.val, Subtype.property, Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : (↑f.Dom : Type u_1)
⊢ f.fn (↑x : α) ⋯ ∈ s ↔ ∃ (y : β), y ∈ s ∧ y ∈ f (↑x : α)

Tactic:
exact
    Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
      have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
      Part.mem_unique fxy this ▸ ys

Premises used: Iff.intro
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ (toSubtype p f).Dom = {a : α | p (f a)}

Tactic:
rfl

Premises used: setOf, PFun.Dom, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
⊢ toSubtype p f a = { Dom := p (f a), get := Subtype.mk (p := p) (f a) }

Tactic:
rfl

Premises used: PFun.toSubtype, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
⊢ (toSubtype p f a).Dom ↔ p (f a)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
rw : Membership.mem (γ := Part (Subtype p)) { Dom := p (f a), get := Subtype.mk (p := p) (f a) } b ↔ (↑b : β) = f a
rw₁ : (∃ (h : p (f a)), Subtype.mk (p := p) (f a) h = b) ↔ (↑b : β) = f a
rw₂ : f a = (↑b : β) ↔ (↑b : β) = f a
rw₃ rw₄ : (↑b : β) = f a ↔ (↑b : β) = f a
⊢ b ∈ toSubtype p f a ↔ (↑b : β) = f a

Tactic:
rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]

Premises used: exists_subtype_mk_eq_iff, Part.mem_mk_iff, eq_comm, PFun.toSubtype_apply
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_7
⊢ (↑id : α →. α) = PFun.id α

Tactic:
rfl

Premises used: PFun.id, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
a : α
⊢ PFun.id α a = Part.some a

Tactic:
rfl

Premises used: PFun.id, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : α
⊢ f.comp g a = (g a).bind f

Tactic:
rfl

Premises used: PFun.comp, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
x : α
x_1 : β
⊢ x_1 ∈ (PFun.id β).comp f x ↔ x_1 ∈ f x

Tactic:
simp
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
x : α
x_1 : β
⊢ x_1 ∈ f.comp (PFun.id α) x ↔ x_1 ∈ f x

Tactic:
simp
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
h : ∀ (x : α), x ∈ (f.comp g).Dom ↔ x ∈ g.preimage f.Dom
⊢ (f.comp g).Dom = g.preimage f.Dom

Tactic:
ext
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x : α
h : (∃ (y : γ), ∃ (a : β), a ∈ g x ∧ y ∈ f a) ↔ ∃ (y : β), (∃ (y_1 : γ), y_1 ∈ f y) ∧ y ∈ g x
⊢ x ∈ (f.comp g).Dom ↔ x ∈ g.preimage f.Dom

Tactic:
simp
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x : α
⊢ (∃ (y : γ), ∃ (a : β), a ∈ g x ∧ y ∈ f a) ↔ ∃ (y : β), (∃ (y_1 : γ), y_1 ∈ f y) ∧ y ∈ g x

Tactic:
grind
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
⊢ (f.comp g).preimage s = g.preimage (f.preimage s)

Tactic:
grind
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
H : ∀ (a_1 : γ), a_1 ∈ a.bind (f.comp g) ↔ a_1 ∈ (a.bind g).bind f
⊢ a.bind (f.comp g) = (a.bind g).bind f

Tactic:
ext
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
a_1 : γ
⊢ a_1 ∈ a.bind (f.comp g) ↔ a_1 ∈ (a.bind g).bind f

Tactic:
grind
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : γ →. δ
g : β →. γ
h : α →. β
x : α
x_1 : δ
⊢ x_1 ∈ (f.comp g).comp h x ↔ x_1 ∈ f.comp (g.comp h) x

Tactic:
simp only [comp_apply, Part.bind_comp]

Premises used: PFun.comp_apply, PFun.Part.bind_comp
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x : α
x_1 : γ
⊢ x_1 ∈ (↑(g ∘ f) : α →. γ) x ↔ x_1 ∈ (↑g : β →. γ).comp (↑f : α →. β) x

Tactic:
simp only [coe_val, comp_apply, Function.comp, Part.bind_some]

Premises used: Part.bind_some, PFun.coe_val, Function.comp, PFun.comp_apply
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
⊢ (f.prodLift g).Dom = {x : α | (f x).Dom ∧ (g x).Dom}

Tactic:
rfl

Premises used: setOf, PFun.Dom, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
h : (f.prodLift g x).Dom
⊢ (f.prodLift g x).get h = ((f x).get ⋯, (g x).get ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
⊢ f.prodLift g x = { Dom := (f x).Dom ∧ (g x).Dom, get := fun (h : (f x).Dom ∧ (g x).Dom) ↦ ((f x).get ⋯, (g x).get ⋯) }

Tactic:
rfl

Premises used: PFun.prodLift, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
trans : y ∈ f.prodLift g x ↔ ∃ (hp : (f x).Dom), ∃ (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2
trans₁ : (∃ (hp : (f x).Dom), ∃ (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x
⊢ y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ ∃ (hp : (f x).Dom), ∃ (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2

Tactic:
simp only [prodLift, Part.mem_mk_iff, And.exists, Prod.ext_iff]

Premises used: Part.mem_mk_iff, PFun.prodLift, Prod.ext_iff, And.exists
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ (hp : (f x).Dom), ∃ (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]

Premises used: Part.Mem, Membership.mem, exists_and_left, exists_and_right
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
⊢ (f.prodMap g).Dom = {x : α × β | (f x.1).Dom ∧ (g x.2).Dom}

Tactic:
rfl

Premises used: setOf, PFun.Dom, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
h : (f.prodMap g x).Dom
⊢ (f.prodMap g x).get h = ((f x.1).get ⋯, (g x.2).get ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
⊢ f.prodMap g x =
    { Dom := (f x.1).Dom ∧ (g x.2).Dom, get := fun (h : (f x.1).Dom ∧ (g x.2).Dom) ↦ ((f x.1).get ⋯, (g x.2).get ⋯) }

Tactic:
rfl

Premises used: PFun.prodMap, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
trans : y ∈ f.prodMap g x ↔ ∃ (hp : (f x.1).Dom), ∃ (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
trans₁ :
  (∃ (hp : (f x.1).Dom), ∃ (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
⊢ y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ ∃ (hp : (f x.1).Dom), ∃ (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

Tactic:
simp only [prodMap, Part.mem_mk_iff, And.exists, Prod.ext_iff]

Premises used: Part.mem_mk_iff, Prod.ext_iff, PFun.prodMap, And.exists
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ (hp : (f x.1).Dom), ∃ (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]

Premises used: Part.Mem, Membership.mem, exists_and_left, exists_and_right
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
⊢ prodLift (f.comp (↑Prod.fst : α × β →. α)) (g.comp (↑Prod.snd : α × β →. β)) = f.prodMap g

Tactic:
aesop
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
⊢ (PFun.id α).prodMap (PFun.id β) = PFun.id (α × β)

Tactic:
aesop
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f₁ : α →. β
f₂ : β →. γ
g₁ : δ →. ε
g₂ : ε →. ι
⊢ (f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁)

Tactic:
ext <| fun ⟨_, _⟩ ⟨_, _⟩ ↦
  ⟨fun ⟨⟨⟨h1l1, h1l2⟩, ⟨h1r1, h1r2⟩⟩, h2⟩ ↦ ⟨⟨⟨h1l1, h1r1⟩, ⟨h1l2, h1r2⟩⟩, h2⟩,
   fun ⟨⟨⟨h1l1, h1r1⟩, ⟨h1l2, h1r2⟩⟩, h2⟩ ↦ ⟨⟨⟨h1l1, h1l2⟩, ⟨h1r1, h1r2⟩⟩, h2⟩⟩

Premises used: _private.0.PFun.prodMap_comp_comp.match_1, Membership.mem, Prod.mk, Iff, PFun.prodMap, And.intro, Iff.intro, Exists.intro, _private.0.PFun.prodMap_comp_comp.match_2, PFun.ext, _private.0.PFun.prodMap_comp_comp.match_3, PFun.comp
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f : P.B a ⟹ α
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) β)
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) g
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β) a (TypeVec.comp (α := P.B a) (β := α) (γ := β) g f))

Tactic:
rfl

Premises used: MvPFunctor.map, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : (↑(const n A) : (α : TypeVec.{u} n) → Type u) α
mk :
  ∀ (fst : (const n A).A) (snd : (const n A).B fst ⟹ α),
    get (α := β)
        (MvFunctor.map (F := (↑(const n A) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f
          (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)) =
      get (α := α) (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
⊢ get (α := β) (MvFunctor.map (F := (↑(const n A) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f x) =
    get (α := α) x

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
fst : (const n A).A
snd : (const n A).B fst ⟹ α
⊢ get (α := β)
      (MvFunctor.map (F := (↑(const n A) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f
        (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)) =
    get (α := α) (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
x : A
⊢ get (α := α) (mk n x (α := α)) = x

Tactic:
rfl

Premises used: MvPFunctor.const.get, rfl