awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₂ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b
pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a
⊢ C a
have pf₁ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
Tactic: generalize_proofs at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a
pf_1 : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
h₂ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a pf_1 :
      Part β)
    b
⊢ C a
have intro : (a : α) →
  (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y) →
    (IH :
        (y : α) →
          (a : Sum.inr y ∈ f a) →
            (h₂ :
                Membership.mem (γ := Part β)
                  (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                      (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                        (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                            match (motive := β ⊕ α → Part β) e : (f a).get hf with
                            | Sum.inl b => Part.some b
                            | Sum.inr a' => IH a' sorry :
                          Part β))
                      y sorry :
                    Part β)
                  b) →
              C y) →
      (h₂ :
          Membership.mem (γ := Part β)
            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' sorry :
                    Part β))
                a sorry :
              Part β)
            b) →
        C a
Tactic: induction ‹Acc (Sum.inr · ∈ f ·) a› with | intro a ha IH => _
Cleared hypotheses: pf_1, h₂
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a_1 : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a
a : α
ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y
IH :
  (y : α) →
    (a : Sum.inr y ∈ f a) →
      (h₂ :
          Membership.mem (γ := Part β)
            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯ :
                    Part β))
                y ⋯ :
              Part β)
            b) →
        C y
h₂ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b
⊢ C a
have h : b ∈ f.fix a
Tactic: have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix 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₀
⊢ C a
have refine : (a' : α) → (h : b ∈ f.fix a') → (ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
Tactic: refine fixInduction h fun a' h ih => ?_
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
⊢ C a'
have inl : (b' : β) → (e : (f a').get sorry = Sum.inl b') → C a'
Tactic: rcases e : (f a').get (dom_of_mem_fix h) with b' | a''
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
inl : (b' : β) → (e : (f a').get ⋯ = Sum.inl b') → C a'
⊢ C a'
have inr : (a'' : α) → (e : (f a').get sorry = Sum.inr a'') → C a'
Tactic: rcases e : (f a').get (dom_of_mem_fix h) with b' | a''
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : (f a').get ⋯ = Sum.inl b'
⊢ C a'
have inl : (e : Sum.inl b' ∈ f a') → C a'
Tactic: replace e : _ ∈ f a' := ⟨_, e⟩
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : (f a').get ⋯ = Sum.inr a''
⊢ C a'
have inr : (e : Sum.inr a'' ∈ f a') → C a'
Tactic: replace e : _ ∈ f a' := ⟨_, e⟩
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ C a'
have inl : Sum.inl b ∈ f a'
Tactic: apply hbase
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ Sum.inl b ∈ f a'
have h₁ : b = b'
Tactic: convert! e
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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₀
⊢ fixInduction' (C := C) h hbase hind = hbase a fa
have unfold : (fixInduction (C := fun (x : α) ↦ C x) h 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 sorry = x) → C a') ((f a').get sorry)
      (fun (b' : β) (e : (f a').get sorry = Sum.inl b') ↦
        have e := sorry;
        hbase a' sorry)
      (fun (a'' : α) (e : (f a').get sorry = Sum.inr a'') ↦
        have e := sorry;
        hind a' a'' sorry e (ih a'' e))
      sorry) =
  hbase a fa
Tactic: unfold fixInduction'
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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₀
⊢ (fixInduction (C := fun (x : α) ↦ C x) h
      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))
        ⋯) =
    hbase a fa
have rw : Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a).get sorry = x) → C a) ((f a).get sorry)
    (fun (b' : β) (e : (f a).get sorry = Sum.inl b') ↦
      have e := sorry;
      hbase a sorry)
    (fun (a'' : α) (e : (f a).get sorry = Sum.inr a'') ↦
      have e := sorry;
      hind a a'' sorry e
        ((fun (x : α) (h' : Sum.inr x ∈ f a) ↦
            (fixInduction (C := fun (x : α) ↦ C x) sorry
                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 sorry = x) → C a') ((f a').get sorry)
                  (fun (b' : β) (e : (f a').get sorry = Sum.inl b') ↦
                    have e := sorry;
                    hbase a' sorry)
                  (fun (a'' : α) (e : (f a').get sorry = Sum.inr a'') ↦
                    have e := sorry;
                    hind a' a'' sorry e (ih a'' e))
                  sorry :
              C x))
          a'' e))
    sorry =
  hbase a fa
Tactic: rw [fixInduction_spec]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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))
      ⋯ =
    hbase a fa
have refine : (fun (x : β ⊕ α) (e : Sum.inl b = x) ↦
    Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (f a).get sorry = x → C a) x
        (fun (b' : β) (e : (f a).get sorry = Sum.inl b') ↦
          have e := sorry;
          hbase a sorry)
        (fun (a'' : α) (e : (f a).get sorry = Sum.inr a'') ↦
          have e := sorry;
          hind a a'' sorry e
            ((fun (x : α) (h' : Sum.inr x ∈ f a) ↦
                (fixInduction (C := fun (x : α) ↦ C x) sorry
                    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 sorry = x) → C a') ((f a').get sorry)
                      (fun (b' : β) (e : (f a').get sorry = Sum.inl b') ↦
                        have e := sorry;
                        hbase a' sorry)
                      (fun (a'' : α) (e : (f a').get sorry = Sum.inr a'') ↦
                        have e := sorry;
                        hind a' a'' sorry e (ih a'' e))
                      sorry :
                  C x))
              a'' e))
        sorry =
      hbase a fa)
  (Sum.inl b) sorry
Tactic: refine Eq.rec (motive := fun x e ↦
      Sum.casesOn x ?_ ?_ (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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₀
⊢ fixInduction' (C := C) h hbase hind = hind a a' h' fa (fixInduction' (C := fun (x : α) ↦ C x) h' hbase hind)
have unfold : (fixInduction (C := fun (x : α) ↦ C x) h 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 sorry = x) → C a') ((f a').get sorry)
      (fun (b' : β) (e : (f a').get sorry = Sum.inl b') ↦
        have e := sorry;
        hbase a' sorry)
      (fun (a'' : α) (e : (f a').get sorry = Sum.inr a'') ↦
        have e := sorry;
        hind a' a'' sorry e (ih a'' e))
      sorry) =
  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 sorry = x) → (fun (x : α) ↦ C x) a') ((f a').get sorry)
        (fun (b' : β) (e : (f a').get sorry = Sum.inl b') ↦
          have e := sorry;
          hbase a' sorry)
        (fun (a'' : α) (e : (f a').get sorry = Sum.inr a'') ↦
          have e := sorry;
          hind a' a'' sorry e (ih a'' e))
        sorry)
Tactic: unfold fixInduction'
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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₀
⊢ (fixInduction (C := fun (x : α) ↦ C x) h
      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))
        ⋯) =
    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))
          ⋯)
have rw : Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a).get sorry = x) → C a) ((f a).get sorry)
    (fun (b' : β) (e : (f a).get sorry = Sum.inl b') ↦
      have e := sorry;
      hbase a sorry)
    (fun (a'' : α) (e : (f a).get sorry = Sum.inr a'') ↦
      have e := sorry;
      hind a a'' sorry e
        ((fun (x : α) (h' : Sum.inr x ∈ f a) ↦
            (fixInduction (C := fun (x : α) ↦ C x) sorry
                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 sorry = x) → C a') ((f a').get sorry)
                  (fun (b' : β) (e : (f a').get sorry = Sum.inl b') ↦
                    have e := sorry;
                    hbase a' sorry)
                  (fun (a'' : α) (e : (f a').get sorry = Sum.inr a'') ↦
                    have e := sorry;
                    hind a' a'' sorry e (ih a'' e))
                  sorry :
              C x))
          a'' e))
    sorry =
  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 sorry = x) → (fun (x : α) ↦ C x) a') ((f a').get sorry)
        (fun (b' : β) (e : (f a').get sorry = Sum.inl b') ↦
          have e := sorry;
          hbase a' sorry)
        (fun (a'' : α) (e : (f a').get sorry = Sum.inr a'') ↦
          have e := sorry;
          hind a' a'' sorry e (ih a'' e))
        sorry)
Tactic: rw [fixInduction_spec]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β
⊢ f.preimage Set.univ = f.Dom
have h : ∀ (x : α), x ∈ f.preimage Set.univ ↔ x ∈ f.Dom
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f : α →. β).preimage s = f ⁻¹' s
have h : ∀ (x : α), x ∈ (↑f : α →. β).preimage s ↔ x ∈ f ⁻¹' s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (res f s).core t = sᶜ ∪ f ⁻¹' t
have h : ∀ (x : α), x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t
have h : x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Tactic: rw [mem_core_res]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
have pos : ∀ (h : x ∈ s), x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
have neg : ∀ (h : ¬x ∈ s), x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f : α →. β).core s = f ⁻¹' s
have h : ∀ (x : α), x ∈ (↑f : α →. β).core s ↔ x ∈ f ⁻¹' s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = f.preimage s ∪ f.Domᶜ
have rw : f.core s = f.core s ∩ f.Dom ∪ 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)]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
rw : f.core s = f.core s ∩ f.Dom ∪ f.Domᶜ
⊢ f.core s = f.preimage s ∪ f.Domᶜ
have rw₁ : f.core s = (f.core s ∪ f.Domᶜ) ∩ (f.Dom ∪ 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)]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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ᶜ)
⊢ f.core s = f.preimage s ∪ f.Domᶜ
have rw₂ : f.core s = (f.core s ∪ f.Domᶜ) ∩ (f.Domᶜ ∪ 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)]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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)
⊢ f.core s = f.preimage s ∪ f.Domᶜ
have rw₃ : f.core s = (f.core s ∪ f.Domᶜ) ∩ Set.univ
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)]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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
⊢ f.core s = f.preimage s ∪ f.Domᶜ
have rw₄ : f.core s = f.core 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)]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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ᶜ
⊢ f.core s = f.preimage s ∪ f.Domᶜ
have rw₅ : f.core s = f.core s
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)]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.asSubtype ⁻¹' s = Subtype.val (p := fun (x : α) ↦ x ∈ f.Dom) ⁻¹' f.preimage s
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
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
have h : f.fn (↑x : α) sorry ∈ s ↔ ∃ (y : β), y ∈ s ∧ y ∈ f (↑x : α)
Tactic: simp only [Set.mem_preimage, PFun.asSubtype, PFun.mem_preimage]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ b ∈ toSubtype p f a ↔ (↑b : β) = f a
have rw : Membership.mem (γ := Part (Subtype p)) { Dom := p (f a), get := Subtype.mk (p := p) (f a) } b ↔ (↑b : β) = f a
Tactic: rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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
⊢ b ∈ toSubtype p f a ↔ (↑b : β) = f a
have rw₁ : (∃ (h : p (f a)), Subtype.mk (p := p) (f a) h = b) ↔ (↑b : β) = f a
Tactic: rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]