[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
⊢ mk' F x' (cast (_ : E x = E x') b) = { proj := x, snd := b }
[PROOFSTEP]
subst h
[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
x : B
b : E x
⊢ mk' F x (cast (_ : E x = E x) b) = { proj := x, snd := b }
[PROOFSTEP]
rfl
[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
y y' : E b
⊢ mk' F b y = mk' F b y' ↔ y = y'
[PROOFSTEP]
simp [TotalSpace.ext_iff]
[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) = proj ⁻¹' {b}
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) ⊆ proj ⁻¹' {b}
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case h₁.intro
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
x : E b
⊢ { proj := b, snd := x } ∈ proj ⁻¹' {b}
[PROOFSTEP]
rfl
[GOAL]
case h₂
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ proj ⁻¹' {b} ⊆ range (mk b)
[PROOFSTEP]
rintro ⟨_, x⟩ rfl
[GOAL]
case h₂.mk
B : Type u_1
F : Type u_2
E : B → Type u_3
proj✝ : B
x : E proj✝
⊢ { proj := proj✝, snd := x } ∈ range (mk { proj := proj✝, snd := x }.proj)
[PROOFSTEP]
exact ⟨x, rfl⟩


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β
x : α
⊢ x ∈ Dom f ↔ ∃ y, y ∈ f x
[PROOFSTEP]
simp [Dom, Part.dom_iff_mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ (fun f => { fst := fun a => (f a).Dom, snd := asSubtype f })
      ((fun f x => { Dom := Sigma.fst f x, get := fun h => Sigma.snd f { val := x, property := h } })
        { fst := p, snd := f }) =
    { fst := p, snd := f }
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ { fst := fun a => p a, snd := asSubtype fun x => { Dom := p x, get := fun h => f { val := x, property := h } } } =
    { fst := p, snd := f }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β
s : Set α
h : s ⊆ Dom f
a : α
b : β
⊢ b ∈ restrict f h a ↔ a ∈ s ∧ b ∈ f a
[PROOFSTEP]
simp [restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α → β
s : Set α
a : α
b : β
⊢ b ∈ res f s a ↔ a ∈ s ∧ f a = b
[PROOFSTEP]
simp [res, @eq_comm _ b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α → β
a : α
b : β
⊢ (∃ x, f a = b) ↔ f a = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type ?u.16924
f : α →. α✝
⊢ id <$> f = f
[PROOFSTEP]
funext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type ?u.16924
f : α →. α✝
a : α
⊢ (id <$> f) a = f a
[PROOFSTEP]
dsimp [Functor.map, PFun.map]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type ?u.16924
f : α →. α✝
a : α
⊢ Part.map id (f a) = f a
[PROOFSTEP]
cases f a
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type ?u.16924
f : α →. α✝
a : α
Dom✝ : Prop
get✝ : Dom✝ → α✝
⊢ Part.map id { Dom := Dom✝, get := get✝ } = { Dom := Dom✝, get := get✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
⊢ (f a).Dom
[PROOFSTEP]
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a h₁
⊢ (f a).Dom
[PROOFSTEP]
rw [WellFounded.fixFEq] at h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf =>
      match e : Part.get (f a) hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
          a' (_ : ∃ h, Part.get (f a) h = Sum.inr a')
⊢ (f a).Dom
[PROOFSTEP]
exact h₂.fst.fst
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a h₁
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
rw [WellFounded.fixFEq] at h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf =>
      match e : Part.get (f a) hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
          a' (_ : ∃ h, Part.get (f a) h = Sum.inr a')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
simp at h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  ∃ h,
    b ∈
      match e : Part.get (f a) h with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          a' (_ : Acc (fun y x => Sum.inr y ∈ f x) a')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
cases' h₂ with h₂ h₃
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
h₃ :
  b ∈
    match e : Part.get (f a) h₂ with
    | Sum.inl b => Part.some b
    | Sum.inr a' =>
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a' (_ : Acc (fun y x => Sum.inr y ∈ f x) a')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
split at h₃
[GOAL]
case intro.h_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
heq✝ : Part.get (f a) h₂ = Sum.inl b✝
h₃ : b ∈ Part.some b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
case intro.h_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
heq✝ : Part.get (f a) h₂ = Sum.inr a'✝
h₃ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
next e => simp at h₃ ; subst b; refine' Or.inl ⟨h₂, e⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : Part.get (f a) h₂ = Sum.inl b✝
h₃ : b ∈ Part.some b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
simp at h₃
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : Part.get (f a) h₂ = Sum.inl b✝
h₃ : b = b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
subst b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : Part.get (f a) h₂ = Sum.inl b✝
h : b✝ ∈ fix f a
⊢ Sum.inl b✝ ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b✝ ∈ fix f a'
[PROOFSTEP]
refine' Or.inl ⟨h₂, e⟩
[GOAL]
case intro.h_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
heq✝ : Part.get (f a) h₂ = Sum.inr a'✝
h₃ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
next e => exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
e : Part.get (f a) h₂ = Sum.inr a'✝
h₃ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
⊢ b ∈ fix f a
[PROOFSTEP]
simp [fix]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a h
[PROOFSTEP]
rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a h
[PROOFSTEP]
refine' ⟨⟨_, fun y h' => _⟩, _⟩
[GOAL]
case inl.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y => Sum.inr x ∈ f y) y
[PROOFSTEP]
injection Part.mem_unique ⟨h₁, h₂⟩ h'
[GOAL]
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
[PROOFSTEP]
rw [WellFounded.fixFEq]
  -- Porting note: used to be simp [h₁, h₂]
[GOAL]
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ b ∈
    Part.assert (f a).Dom fun hf =>
      match e : Part.get (f a) hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
          a' (_ : ∃ h, Part.get (f a) h = Sum.inr a')
[PROOFSTEP]
apply Part.mem_assert h₁
[GOAL]
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ b ∈
    match e : Part.get (f a) h₁ with
    | Sum.inl b => Part.some b
    | Sum.inr a' =>
      (fun y p =>
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
        a' (_ : ∃ h, Part.get (f a) h = Sum.inr a')
[PROOFSTEP]
split
[GOAL]
case inl.intro.refine'_2.h_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
heq✝ : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝
case inl.intro.refine'_2.h_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
next e => injection h₂.symm.trans e with h; simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
e : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝
[PROOFSTEP]
injection h₂.symm.trans e with h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
e : Part.get (f a) h₁ = Sum.inl b✝
h : b = b✝
⊢ b ∈ Part.some b✝
[PROOFSTEP]
simp [h]
[GOAL]
case inl.intro.refine'_2.h_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
next e => injection h₂.symm.trans e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
injection h₂.symm.trans e
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ fix f a'
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a h
[PROOFSTEP]
simp [fix] at h₃
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ :
  ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a' h
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a h
[PROOFSTEP]
cases' h₃ with h₃ h₄
[GOAL]
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a h
[PROOFSTEP]
refine' ⟨⟨_, fun y h' => _⟩, _⟩
[GOAL]
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y => Sum.inr x ∈ f y) y
[PROOFSTEP]
injection Part.mem_unique h h' with e
[GOAL]
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
y : α
h' : Sum.inr y ∈ f a
e : a' = y
⊢ Acc (fun x y => Sum.inr x ∈ f y) y
[PROOFSTEP]
exact e ▸ h₃
[GOAL]
case inr.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
⊢ b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
[PROOFSTEP]
rw [WellFounded.fixFEq]
  -- Porting note: used to be simp [h₁, h₂, h₄]
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ b ∈
    Part.assert (f a).Dom fun hf =>
      match e : Part.get (f a) hf with
      | Sum.inl b => Part.some b
      | Sum.inr a'_1 =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
          a'_1 (_ : ∃ h, Part.get (f a) h = Sum.inr a'_1)
[PROOFSTEP]
apply Part.mem_assert h₁
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ b ∈
    match e : Part.get (f a) h₁ with
    | Sum.inl b => Part.some b
    | Sum.inr a'_1 =>
      (fun y p =>
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
        a'_1 (_ : ∃ h, Part.get (f a) h = Sum.inr a'_1)
[PROOFSTEP]
split
[GOAL]
case inr.intro.intro.intro.refine'_2.intro.h_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
b✝ : β
heq✝ : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝
case inr.intro.intro.intro.refine'_2.intro.h_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
next e => injection h₂.symm.trans e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
b✝ : β
e : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝
[PROOFSTEP]
injection h₂.symm.trans e
[GOAL]
case inr.intro.intro.intro.refine'_2.intro.h_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
next e => injection h₂.symm.trans e; subst a'; exact h₄
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
injection h₂.symm.trans e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a' h₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
val_eq✝ : a' = a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
subst a'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
h₃ : Acc (fun x y => Sum.inr x ∈ f y) a'✝
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a'✝ h₃
h₂ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : Part.get (f a) hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
          y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
      a'✝ (_ : ∃ h, Part.get (f a) h = Sum.inr a'✝)
[PROOFSTEP]
exact h₄
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ b ∈ fix f a
[PROOFSTEP]
rw [PFun.mem_fix_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
exact Or.inl hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
⊢ fix f a = fix f a'
[PROOFSTEP]
ext b
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a ↔ b ∈ fix f a'
[PROOFSTEP]
constructor
[GOAL]
case H.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a → b ∈ fix f a'
[PROOFSTEP]
intro h
[GOAL]
case H.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a
⊢ b ∈ fix f a'
[PROOFSTEP]
obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h
[GOAL]
case H.mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a
h' : Sum.inl b ∈ f a
⊢ b ∈ fix f a'
[PROOFSTEP]
cases Part.mem_unique ha' h'
[GOAL]
case H.mp.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a✝ a' : α
ha' : Sum.inr a' ∈ f a✝
b : β
h : b ∈ fix f a✝
a : α
h' : Sum.inr a ∈ f a✝
e' : b ∈ fix f a
⊢ b ∈ fix f a'
[PROOFSTEP]
cases Part.mem_unique ha' h'
[GOAL]
case H.mp.inr.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a
h' : Sum.inr a' ∈ f a
e' : b ∈ fix f a'
⊢ b ∈ fix f a'
[PROOFSTEP]
exact e'
[GOAL]
case H.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a' → b ∈ fix f a
[PROOFSTEP]
intro h
[GOAL]
case H.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a'
⊢ b ∈ fix f a
[PROOFSTEP]
rw [PFun.mem_fix_iff]
[GOAL]
case H.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a'
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
[PROOFSTEP]
exact Or.inr ⟨a', ha', h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β ⊕ α
b : β
a a' : α
hb : b ∈ fix f a
ha' : Sum.inr a' ∈ f a
⊢ b ∈ fix f a'
[PROOFSTEP]
rwa [← fix_fwd_eq ha']
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ C a
[PROOFSTEP]
have h₂ := (Part.mem_assert_iff.1 h).snd
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
⊢ C a
[PROOFSTEP]
revert h₂
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a (_ : Acc (fun x y => Sum.inr x ∈ f y) a) →
    C a
[PROOFSTEP]
generalize_proofs h₁
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
⊢ b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : Part.get (f a) hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
        a h₁ →
    C a
[PROOFSTEP]
intro h₂
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a h₁
⊢ C a
[PROOFSTEP]
clear h
[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 ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a h₁
⊢ C a
[PROOFSTEP]
induction' h₁ with a ha IH
[GOAL]
case intro
α : 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 ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a✝
h₂✝ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a✝ h₁
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) →
      b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            y (_ : Acc ?m.29240 y) →
        C y
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
⊢ C a
[PROOFSTEP]
have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩
[GOAL]
case intro
α : 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 ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a✝
h₂✝ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a✝ h₁
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) →
      b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            y (_ : Acc ?m.29240 y) →
        C y
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
h : b ∈ fix f a
⊢ C a
[PROOFSTEP]
exact H a h fun a' fa' => IH a' fa' (Part.mem_assert_iff.1 (fix_fwd h fa')).snd
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ fixInduction h H = H a h fun a' h' => fixInduction (_ : b ∈ fix f a') H
[PROOFSTEP]
unfold fixInduction
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ (let_fun h₂ :=
      (_ :
        b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            a (_ : Acc (fun x y => Sum.inr x ∈ f y) a));
    Acc.rec (motive := fun {a} h₁ =>
      b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            a h₁ →
        C a)
      (fun a ha IH h₂ =>
        let_fun h :=
          (_ :
            b ∈
              Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : Part.get (f a) hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                  a h);
        H a h fun a' fa' =>
          IH a' fa'
            (_ :
              b ∈
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : Part.get (f a) hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                  a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
      (_ : Acc (fun x y => Sum.inr x ∈ f y) a) h₂) =
    H a h fun a' h' =>
      let_fun h₂ :=
        (_ :
          b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a'));
      Acc.rec (motive := fun {a} h₁ =>
        b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              a h₁ →
          (fun x => C x) a)
        (fun a ha IH h₂ =>
          let_fun h :=
            (_ :
              b ∈
                Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a h);
          H a h fun a' fa' =>
            IH a' fa'
              (_ :
                b ∈
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
        (_ : Acc (fun x y => Sum.inr x ∈ f y) a') h₂
[PROOFSTEP]
generalize (Part.mem_assert_iff.1 h).fst = ha
[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 ∈ fix f a
H : (a' : α) → b ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
ha : Acc (fun x y => Sum.inr x ∈ f y) a
⊢ (let_fun h₂ :=
      (_ :
        b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            a (_ : Acc (fun x y => Sum.inr x ∈ f y) a));
    Acc.rec (motive := fun {a} h₁ =>
      b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            a h₁ →
        C a)
      (fun a ha IH h₂ =>
        let_fun h :=
          (_ :
            b ∈
              Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : Part.get (f a) hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                  a h);
        H a h fun a' fa' =>
          IH a' fa'
            (_ :
              b ∈
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : Part.get (f a) hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                  a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
      ha h₂) =
    H a h fun a' h' =>
      let_fun h₂ :=
        (_ :
          b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a'));
      Acc.rec (motive := fun {a} h₁ =>
        b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              a h₁ →
          (fun x => C x) a)
        (fun a ha IH h₂ =>
          let_fun h :=
            (_ :
              b ∈
                Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a h);
          H a h fun a' fa' =>
            IH a' fa'
              (_ :
                b ∈
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
        (_ : Acc (fun x y => Sum.inr x ∈ f y) a') h₂
[PROOFSTEP]
induction ha
[GOAL]
case intro
α : 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 ∈ fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
x✝ : α
h✝ : ∀ (y : α), Sum.inr y ∈ f x✝ → Acc (fun x y => Sum.inr x ∈ f y) y
h_ih✝ :
  ∀ (y : α) (a : Sum.inr y ∈ f x✝) (h : b ∈ fix f y),
    (let_fun h₂ :=
        (_ :
          b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              y (_ : Acc (fun x y => Sum.inr x ∈ f y) y));
      Acc.rec (motive := fun {a} h₁ =>
        b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              a h₁ →
          C a)
        (fun a ha IH h₂ =>
          let_fun h :=
            (_ :
              b ∈
                Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a h);
          H a h fun a' fa' =>
            IH a' fa'
              (_ :
                b ∈
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
        (_ : Acc ?m.30282 y) h₂) =
      H y h fun a' h' =>
        let_fun h₂ :=
          (_ :
            b ∈
              WellFounded.fixF
                (fun a IH =>
                  Part.assert (f a).Dom fun hf =>
                    match e : Part.get (f a) hf with
                    | Sum.inl b => Part.some b
                    | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a'));
        Acc.rec (motive := fun {a} h₁ =>
          b ∈
              WellFounded.fixF
                (fun a IH =>
                  Part.assert (f a).Dom fun hf =>
                    match e : Part.get (f a) hf with
                    | Sum.inl b => Part.some b
                    | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                a h₁ →
            (fun x => C x) a)
          (fun a ha IH h₂ =>
            let_fun h :=
              (_ :
                b ∈
                  Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                    WellFounded.fixF
                      (fun a IH =>
                        Part.assert (f a).Dom fun hf =>
                          match e : Part.get (f a) hf with
                          | Sum.inl b => Part.some b
                          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                      a h);
            H a h fun a' fa' =>
              IH a' fa'
                (_ :
                  b ∈
                    WellFounded.fixF
                      (fun a IH =>
                        Part.assert (f a).Dom fun hf =>
                          match e : Part.get (f a) hf with
                          | Sum.inl b => Part.some b
                          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                      a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
          (_ : Acc (fun x y => Sum.inr x ∈ f y) a') h₂
h : b ∈ fix f x✝
⊢ (let_fun h₂ :=
      (_ :
        b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            x✝ (_ : Acc (fun x y => Sum.inr x ∈ f y) x✝));
    Acc.rec (motive := fun {a} h₁ =>
      b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : Part.get (f a) hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
            a h₁ →
        C a)
      (fun a ha IH h₂ =>
        let_fun h :=
          (_ :
            b ∈
              Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : Part.get (f a) hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                  a h);
        H a h fun a' fa' =>
          IH a' fa'
            (_ :
              b ∈
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : Part.get (f a) hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                  a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
      (_ : Acc (fun x y => Sum.inr x ∈ f y) x✝) h₂) =
    H x✝ h fun a' h' =>
      let_fun h₂ :=
        (_ :
          b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a'));
      Acc.rec (motive := fun {a} h₁ =>
        b ∈
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              a h₁ →
          (fun x => C x) a)
        (fun a ha IH h₂ =>
          let_fun h :=
            (_ :
              b ∈
                Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a h);
          H a h fun a' fa' =>
            IH a' fa'
              (_ :
                b ∈
                  WellFounded.fixF
                    (fun a IH =>
                      Part.assert (f a).Dom fun hf =>
                        match e : Part.get (f a) hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
                    a' (_ : Acc (fun x y => Sum.inr x ∈ f y) a')))
        (_ : Acc (fun x y => Sum.inr x ∈ f y) a') h₂
[PROOFSTEP]
rfl
[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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ C a
[PROOFSTEP]
refine' fixInduction h fun a' h ih => _
[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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ fix f a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
⊢ C a'
[PROOFSTEP]
rcases e : (f a').get (dom_of_mem_fix h) with b' | a''
[GOAL]
case inl
α : 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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ fix f a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Part.get (f a') (_ : (f a').Dom) = Sum.inl b'
⊢ C a'
[PROOFSTEP]
replace e : _ ∈ f a' := ⟨_, e⟩
[GOAL]
case inr
α : 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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ fix f a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : Part.get (f a') (_ : (f a').Dom) = Sum.inr a''
⊢ C a'
[PROOFSTEP]
replace e : _ ∈ f a' := ⟨_, e⟩
[GOAL]
case inl
α : 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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ fix f a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ C a'
[PROOFSTEP]
apply hbase
[GOAL]
case inl.a
α : 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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ fix f a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ Sum.inl b ∈ f a'
[PROOFSTEP]
convert e
[GOAL]
case h.e'_4.h.e'_3
α : 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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ fix f a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ b = b'
[PROOFSTEP]
exact Part.mem_unique h (fix_stop e)
[GOAL]
case inr
α : 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 ∈ fix f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ fix f a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : Sum.inr a'' ∈ f a'
⊢ C a'
[PROOFSTEP]
exact hind _ _ (fix_fwd h e) e (ih _ e)
[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 ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ fixInduction' h hbase hind = hbase a fa
[PROOFSTEP]
unfold fixInduction'
[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 ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih =>
      Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a') (Part.get (f a') (_ : (f a').Dom))
        (fun b' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
          hbase a' (_ : Sum.inl b ∈ f a'))
        (fun a'' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
          hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
        (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom))) =
    hbase a fa
[PROOFSTEP]
rw [fixInduction_spec]
  -- Porting note: the explicit motive required because `simp` behaves differently
[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 ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x => Part.get (f a) (_ : (f a).Dom) = x → C a) (Part.get (f a) (_ : (f a).Dom))
      (fun b' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
        hbase a (_ : Sum.inl b ∈ f a))
      (fun a'' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
        hind a a'' (_ : b ∈ fix f a'') e
          ((fun a' h' =>
              fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                  (Part.get (f a') (_ : (f a').Dom))
                  (fun b' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                    hbase a' (_ : Sum.inl b ∈ f a'))
                  (fun a'' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                    hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                  (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
            a'' e))
      (_ : Part.get (f a) (_ : (f a).Dom) = Part.get (f a) (_ : (f a).Dom)) =
    hbase a fa
[PROOFSTEP]
refine'
  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) =
      hbase a fa)
    _ (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm
[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 ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fun x e =>
      Sum.casesOn (motive := fun y => Part.get (f a) (_ : (f a).Dom) = y → C a) x
          (fun val =>
            (fun b' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
                hbase a (_ : Sum.inl b ∈ f a))
              val)
          (fun val =>
            (fun a'' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
                hind a a'' (_ : b ∈ fix f a'') e
                  ((fun a' h' =>
                      fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                        Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                          (Part.get (f a') (_ : (f a').Dom))
                          (fun b' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                            hbase a' (_ : Sum.inl b ∈ f a'))
                          (fun a'' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                            hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                          (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
                    a'' e))
              val)
          (_ : Part.get (f a) (_ : (f a).Dom) = x) =
        hbase a fa)
    (Sum.inl b) (_ : Sum.inl b = Sum.inl b)
[PROOFSTEP]
simp
[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 a' : α
h : b ∈ fix f a
h' : b ∈ fix f a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ fixInduction' h hbase hind = hind a a' h' fa (fixInduction' h' hbase hind)
[PROOFSTEP]
unfold fixInduction'
[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 a' : α
h : b ∈ fix f a
h' : b ∈ fix f a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih =>
      Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a') (Part.get (f a') (_ : (f a').Dom))
        (fun b' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
          hbase a' (_ : Sum.inl b ∈ f a'))
        (fun a'' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
          hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
        (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom))) =
    hind a a' h' fa
      (fixInduction h' fun a' h ih =>
        Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → (fun x => C x) a')
          (Part.get (f a') (_ : (f a').Dom))
          (fun b' e =>
            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
            hbase a' (_ : Sum.inl b ∈ f a'))
          (fun a'' e =>
            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
            hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
          (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
[PROOFSTEP]
rw [fixInduction_spec]
  -- Porting note: the explicit motive required because `simp` behaves differently
[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 a' : α
h : b ∈ fix f a
h' : b ∈ fix f a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x => Part.get (f a) (_ : (f a).Dom) = x → C a) (Part.get (f a) (_ : (f a).Dom))
      (fun b' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
        hbase a (_ : Sum.inl b ∈ f a))
      (fun a'' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
        hind a a'' (_ : b ∈ fix f a'') e
          ((fun a' h' =>
              fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                  (Part.get (f a') (_ : (f a').Dom))
                  (fun b' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                    hbase a' (_ : Sum.inl b ∈ f a'))
                  (fun a'' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                    hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                  (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
            a'' e))
      (_ : Part.get (f a) (_ : (f a).Dom) = Part.get (f a) (_ : (f a).Dom)) =
    hind a a' h' fa
      (fixInduction h' fun a' h ih =>
        Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → (fun x => C x) a')
          (Part.get (f a') (_ : (f a').Dom))
          (fun b' e =>
            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
            hbase a' (_ : Sum.inl b ∈ f a'))
          (fun a'' e =>
            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
            hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
          (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
[PROOFSTEP]
refine'
  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
[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 a' : α
h : b ∈ fix f a
h' : b ∈ fix f a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fun x e =>
      Sum.casesOn (motive := fun y => Part.get (f a) (_ : (f a).Dom) = y → C a) x
          (fun val =>
            (fun b' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
                hbase a (_ : Sum.inl b ∈ f a))
              val)
          (fun val =>
            (fun a'' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
                hind a a'' (_ : b ∈ fix f a'') e
                  ((fun a' h' =>
                      fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                        Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                          (Part.get (f a') (_ : (f a').Dom))
                          (fun b' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                            hbase a' (_ : Sum.inl b ∈ f a'))
                          (fun a'' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                            hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                          (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
                    a'' e))
              val)
          (_ : Part.get (f a) (_ : (f a).Dom) = x) =
        hind a a' h' fa
          (fixInduction h' fun a' h ih =>
            Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → (fun x => C x) a')
              (Part.get (f a') (_ : (f a').Dom))
              (fun b' e =>
                let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                hbase a' (_ : Sum.inl b ∈ f a'))
              (fun a'' e =>
                let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
              (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom))))
    (Sum.inr a') (_ : Sum.inr a' = Sum.inr a')
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β
⊢ preimage f Set.univ = Dom f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β
x✝ : α
⊢ x✝ ∈ preimage f Set.univ ↔ x✝ ∈ Dom f
[PROOFSTEP]
simp [mem_preimage, mem_dom]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set β
⊢ preimage (↑f) s = f ⁻¹' s
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set β
x✝ : α
⊢ x✝ ∈ preimage (↑f) s ↔ x✝ ∈ f ⁻¹' s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ core (res f s) t ↔ x ∈ s → f x ∈ t
[PROOFSTEP]
simp [mem_core, mem_res]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set α
t : Set β
⊢ core (res f s) t = sᶜ ∪ f ⁻¹' t
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ core (res f s) t ↔ x ∈ sᶜ ∪ f ⁻¹' t
[PROOFSTEP]
rw [mem_core_res]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
[PROOFSTEP]
by_cases h : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
h : x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
h : ¬x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set β
⊢ core (↑f) s = f ⁻¹' s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α → β
s : Set β
x : α
⊢ x ∈ core (↑f) s ↔ x ∈ f ⁻¹' s
[PROOFSTEP]
simp [core_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
s : Set β
⊢ core f s = preimage f s ∪ (Dom f)ᶜ
[PROOFSTEP]
rw [preimage_eq, Set.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)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
s : Set β
⊢ asSubtype f ⁻¹' s = Subtype.val ⁻¹' preimage f s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ x ∈ asSubtype f ⁻¹' s ↔ x ∈ Subtype.val ⁻¹' preimage f s
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_setOf_eq, PFun.asSubtype, PFun.mem_preimage]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ fn f ↑x (_ : ↑x ∈ Dom f) ∈ s ↔ ∃ y, y ∈ s ∧ y ∈ f ↑x
[PROOFSTEP]
show f.fn x.val _ ∈ s ↔ ∃ y ∈ s, y ∈ f x.val
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ fn f ↑x (_ : ↑x ∈ Dom f) ∈ s ↔ ∃ y, y ∈ s ∧ y ∈ f ↑x
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ b ∈ toSubtype p f a ↔ ↑b = f a
[PROOFSTEP]
rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ comp (PFun.id β) f x✝¹ ↔ x✝ ∈ f x✝¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ comp f (PFun.id α) x✝¹ ↔ x✝ ∈ f x✝¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
⊢ Dom (comp f g) = preimage g (Dom f)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ x✝ ∈ Dom (comp f g) ↔ x✝ ∈ preimage g (Dom f)
[PROOFSTEP]
simp_rw [mem_preimage, mem_dom, comp_apply, Part.mem_bind_iff, ← exists_and_right]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ y a, a ∈ g x✝ ∧ y ∈ f a) ↔ ∃ y x, x ∈ f y ∧ y ∈ g x✝
[PROOFSTEP]
rw [exists_comm]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ b a, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y x, x ∈ f y ∧ y ∈ g x✝
[PROOFSTEP]
simp_rw [and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
s : Set γ
⊢ preimage (comp f g) s = preimage g (preimage f s)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ x✝ ∈ preimage (comp f g) s ↔ x✝ ∈ preimage g (preimage f s)
[PROOFSTEP]
simp_rw [mem_preimage, comp_apply, Part.mem_bind_iff, ← exists_and_right, ← exists_and_left]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ (∃ y x, y ∈ s ∧ x ∈ g x✝ ∧ y ∈ f x) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝
[PROOFSTEP]
rw [exists_comm]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ (∃ b a, a ∈ s ∧ b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝
[PROOFSTEP]
simp_rw [and_assoc, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
⊢ Part.bind a (comp f g) = Part.bind (Part.bind a g) f
[PROOFSTEP]
ext c
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ c ∈ Part.bind a (comp f g) ↔ c ∈ Part.bind (Part.bind a g) f
[PROOFSTEP]
simp_rw [Part.mem_bind_iff, comp_apply, Part.mem_bind_iff, ← exists_and_right, ← exists_and_left]
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ a_1 x, a_1 ∈ a ∧ x ∈ g a_1 ∧ c ∈ f x) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1
[PROOFSTEP]
rw [exists_comm]
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ b a_1, a_1 ∈ a ∧ b ∈ g a_1 ∧ c ∈ f b) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1
[PROOFSTEP]
simp_rw [and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : γ →. δ
g : β →. γ
h : α →. β
x✝¹ : α
x✝ : δ
⊢ x✝ ∈ comp (comp f g) h x✝¹ ↔ x✝ ∈ comp f (comp g h) x✝¹
[PROOFSTEP]
simp only [comp_apply, Part.bind_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
g : β → γ
f : α → β
x✝¹ : α
x✝ : γ
⊢ x✝ ∈ ↑(g ∘ f) x✝¹ ↔ x✝ ∈ comp (↑g) (↑f) x✝¹
[PROOFSTEP]
simp only [coe_val, comp_apply, Function.comp, Part.bind_some]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ prodLift f g x ↔ y.fst ∈ f x ∧ y.snd ∈ g x
[PROOFSTEP]
trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ prodLift f g x ↔ ∃ hp hq, Part.get (f x) hp = y.fst ∧ Part.get (g x) hq = y.snd
[PROOFSTEP]
simp only [prodLift, Part.mem_mk_iff, And.exists, Prod.ext_iff]
  -- Porting note: was just `[exists_and_left, exists_and_right]`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ hp hq, Part.get (f x) hp = y.fst ∧ Part.get (g x) hq = y.snd) ↔ y.fst ∈ f x ∧ y.snd ∈ g x
[PROOFSTEP]
simp only [exists_and_left, exists_and_right, (· ∈ ·), Part.Mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ prodMap f g x ↔ y.fst ∈ f x.fst ∧ y.snd ∈ g x.snd
[PROOFSTEP]
trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ prodMap f g x ↔ ∃ hp hq, Part.get (f x.fst) hp = y.fst ∧ Part.get (g x.snd) hq = y.snd
[PROOFSTEP]
simp only [prodMap, Part.mem_mk_iff, And.exists, Prod.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ hp hq, Part.get (f x.fst) hp = y.fst ∧ Part.get (g x.snd) hq = y.snd) ↔ y.fst ∈ f x.fst ∧ y.snd ∈ g x.snd
[PROOFSTEP]
simp only [exists_and_left, exists_and_right, (· ∈ ·), Part.Mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f✝ : α →. β
f : α →. γ
g : β →. δ
a : α × β
⊢ ∀ (b : γ × δ), b ∈ prodLift (comp f ↑Prod.fst) (comp g ↑Prod.snd) a ↔ b ∈ prodMap f g a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
f : α →. β
x✝¹ x✝ : α × β
⊢ x✝ ∈ prodMap (PFun.id α) (PFun.id β) x✝¹ ↔ x✝ ∈ PFun.id (α × β) x✝¹
[PROOFSTEP]
simp [eq_comm]


[GOAL]
α : Type u_1
β : Type u_2
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s
[PROOFSTEP]
refine' ⟨congr_arg _, fun h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂
[PROOFSTEP]
cases' q₁ with _ v₁
[GOAL]
case mk'
α : Type u_1
β : Type u_2
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂
[PROOFSTEP]
cases' q₂ with _ v₂
[GOAL]
case mk'.mk'
α : Type u_1
β : Type u_2
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }
[PROOFSTEP]
congr
[GOAL]
case mk'.mk'.h.e_3
α : Type u_1
β : Type u_2
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ HEq v₁ v₂
[PROOFSTEP]
exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur s q = blur' q h
[PROOFSTEP]
unfold blur
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur' q (_ : q.s ⊆ s ∪ q.s) = blur' q h
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
β : Type u_2
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s
[PROOFSTEP]
exact Set.union_eq_self_of_subset_right h
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b
a : α
aq : a ∈ q
⊢ liftOn q f h = f a
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b), liftOn q f h = f a
[PROOFSTEP]
rw [eq_mk_of_mem aq]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b), liftOn (mk aq) f h = f a
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b
⊢ liftOn (mk aq) f h✝ = f a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ bind q f ↔ ∃ a, a ∈ q ∧ b ∈ f a
[PROOFSTEP]
simp_rw [← exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ bind q f ↔ ∃ a _h, b ∈ f a
[PROOFSTEP]
exact Set.mem_iUnion₂
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type ?u.6544
q : Semiquot α
⊢ ∀ (a : α), a ∈ id <$> q ↔ a ∈ q
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : Type ?u.6544
x : α
f : α → Semiquot β
⊢ ∀ (a : β), a ∈ pure x >>= f ↔ a ∈ f x
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β γ : Type ?u.6544
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), a ∈ s >>= f >>= g ↔ a ∈ s >>= fun x => f x >>= g
[PROOFSTEP]
simp only [bind_def, mem_bind]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β γ : Type ?u.6544
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), (∃ a_1, (∃ a, a ∈ s ∧ a_1 ∈ f a) ∧ a ∈ g a_1) ↔ ∃ a_1, a_1 ∈ s ∧ ∃ a_2, a_2 ∈ f a_1 ∧ a ∈ g a_2
[PROOFSTEP]
exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩, fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : Type ?u.6544
f : α → β
s : Semiquot α
⊢ ∀ (a : β),
    (a ∈ do
        let y ← s
        pure (f y)) ↔
      a ∈ f <$> s
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
⊢ get q p ∈ q
[PROOFSTEP]
let ⟨a, h⟩ := exists_mem q
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
h : a ∈ q
⊢ get q p ∈ q
[PROOFSTEP]
unfold get
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
h : a ∈ q
⊢ liftOn q id p ∈ q
[PROOFSTEP]
rw [liftOn_ofMem q _ _ a h]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
h : a ∈ q
⊢ id a ∈ q
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
⊢ a ∈ q ↔ a ∈ pure (get q p)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
⊢ a ∈ q ↔ a = get q p
[PROOFSTEP]
exact ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩
[GOAL]
α : Type u_1
β : Type u_2
a b : α
ab : b ∈ pure a
c : α
ac : c ∈ pure a
⊢ b = c
[PROOFSTEP]
rw [mem_pure] at ab ac
[GOAL]
α : Type u_1
β : Type u_2
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c
[PROOFSTEP]
rwa [← ac] at ab
[GOAL]
α : Type u_1
β : Type u_2
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ t ≤ s
[PROOFSTEP]
rw [eq_pure h, eq_pure (h.mono st)]
[GOAL]
α : Type u_1
β : Type u_2
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ pure (get t h) ≤ pure (get s (_ : IsPure s))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ get t h = get s (_ : IsPure s)
[PROOFSTEP]
exact h _ (get_mem _) _ (st <| get_mem _)


[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Splits (algebraMap K L) (Polynomial.map (algebraMap F K) f)
[PROOFSTEP]
rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Splits (algebraMap F L) f
[PROOFSTEP]
exact splits L f
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Subalgebra.restrictScalars F (Algebra.adjoin K (rootSet (Polynomial.map (algebraMap F K) f) L)) =
    Subalgebra.restrictScalars F ⊤
[PROOFSTEP]
rw [rootSet, map_map, ← IsScalarTower.algebraMap_eq, Subalgebra.restrictScalars_top, eq_top_iff, ← adjoin_rootSet L f,
  Algebra.adjoin_le_iff]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ rootSet f L ⊆
    ↑(Subalgebra.restrictScalars F (Algebra.adjoin K ↑(Multiset.toFinset (roots (Polynomial.map (algebraMap F L) f)))))
[PROOFSTEP]
exact fun x hx => @Algebra.subset_adjoin K _ _ _ _ _ _ hx
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ⊤ = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← adjoin_rootSet L f, rootSet, roots_map (algebraMap K L) h, Algebra.adjoin_le_iff]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f))) ⊆ ↑⊥
[PROOFSTEP]
intro y hy
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
⊢ y ∈ ↑⊥
[PROOFSTEP]
rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy✝ : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
hy : ∃ a, a ∈ Multiset.toFinset (roots f) ∧ ↑(algebraMap K L) a = y
⊢ y ∈ ↑⊥
[PROOFSTEP]
obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
[GOAL]
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ y ∈ ↑⊥
[PROOFSTEP]
rw [← hxy]
[GOAL]
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ ↑(algebraMap K L) x ∈ ↑⊥
[PROOFSTEP]
exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    (RingEquiv.toRingHom
      (RingEquiv.trans (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))
        (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L))))))
    f
[PROOFSTEP]
rw [RingEquiv.toRingHom_trans]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
      (RingEquiv.toRingHom (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
    f
[PROOFSTEP]
exact splits_comp_of_splits _ _ (splits L f)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F (rootSet (f * g) L) = ⊤
[PROOFSTEP]
rw [rootSet, Polynomial.map_mul, roots_mul (mul_ne_zero (map_ne_zero hf : f.map (algebraMap F L) ≠ 0) (map_ne_zero hg)),
  Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin, IsScalarTower.algebraMap_eq F K L, ←
  map_map, roots_map (algebraMap K L) ((splits_id_iff_splits <| algebraMap F K).2 <| splits K f), Multiset.toFinset_map,
  Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet, Algebra.map_top,
  IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet, Subalgebra.restrictScalars_top]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : f = 0
⊢ L →ₐ[K] { x // x ∈ ⊥ }
[PROOFSTEP]
rw [← (splits_iff L f).1 (show f.Splits (RingHom.id K) from hf0.symm ▸ splits_zero _)]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : f = 0
⊢ L →ₐ[K] { x // x ∈ ⊤ }
[PROOFSTEP]
exact Algebra.toTop
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : ¬f = 0
⊢ { x // x ∈ ⊤ } →ₐ[K] F
[PROOFSTEP]
rw [← adjoin_rootSet L f]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : ¬f = 0
⊢ { x // x ∈ Algebra.adjoin K (rootSet f L) } →ₐ[K] F
[PROOFSTEP]
exact
  Classical.choice
    (lift_of_splits _ fun y hy =>
      have : aeval y f = 0 :=
        (eval₂_eq_eval_map _).trans <| (mem_roots <| map_ne_zero hf0).1 (Multiset.mem_toFinset.mp hy)
      ⟨isAlgebraic_iff_isIntegral.1 ⟨f, hf0, this⟩, splits_of_splits_of_dvd _ hf0 hf <| minpoly.dvd _ _ this⟩)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ rootSet f L
hf : f = 0
⊢ IsIntegral K y
[PROOFSTEP]
rw [hf, rootSet_zero] at hy
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ ∅
hf : f = 0
⊢ IsIntegral K y
[PROOFSTEP]
cases hy
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ IsSplittingField K L p
[PROOFSTEP]
constructor
[GOAL]
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits (algebraMap K L) p
[PROOFSTEP]
rw [← f.toAlgHom.comp_algebraMap]
[GOAL]
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits (RingHom.comp (↑↑f) (algebraMap K F)) p
[PROOFSTEP]
exact splits_comp_of_splits _ _ (splits F p)
[GOAL]
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (rootSet p L) = ⊤
[PROOFSTEP]
rw [← (Algebra.range_top_iff_surjective f.toAlgHom).mpr f.surjective, adjoin_rootSet_eq_range (splits F p),
  adjoin_rootSet F p]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ rootSet p L → x ∈ F
⊢ Splits (algebraMap K { x // x ∈ F }) p
[PROOFSTEP]
simp_rw [rootSet_def, Finset.mem_coe, Multiset.mem_toFinset] at hF
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ Splits (algebraMap K { x // x ∈ F }) p
[PROOFSTEP]
rw [splits_iff_exists_multiset]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ ∃ s,
    Polynomial.map (algebraMap K { x // x ∈ F }) p =
      ↑C (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
[PROOFSTEP]
refine' ⟨Multiset.pmap Subtype.mk _ hF, map_injective _ (algebraMap F L).injective _⟩
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p) =
    Polynomial.map (algebraMap { x // x ∈ F } L)
      (↑C (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p)) *
        Multiset.prod
          (Multiset.map (fun a => X - ↑C a) (Multiset.pmap Subtype.mk (roots (Polynomial.map (algebraMap K L) p)) hF)))
[PROOFSTEP]
conv_lhs =>
  rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
| Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p)
[PROOFSTEP]
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
| Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p)
[PROOFSTEP]
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
| Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p)
[PROOFSTEP]
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ ↑C (↑(algebraMap K L) (leadingCoeff p)) *
      Multiset.prod (Multiset.pmap (fun a x => X - ↑C a) (roots (Polynomial.map (algebraMap K L) p)) hF) =
    Polynomial.map (algebraMap { x // x ∈ F } L)
      (↑C (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p)) *
        Multiset.prod
          (Multiset.map (fun a => X - ↑C a) (Multiset.pmap Subtype.mk (roots (Polynomial.map (algebraMap K L) p)) hF)))
[PROOFSTEP]
simp_rw [Polynomial.map_mul, Polynomial.map_multiset_prod, Multiset.map_pmap, Polynomial.map_sub, map_C, map_X]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ ↑C (↑(algebraMap K L) (leadingCoeff p)) *
      Multiset.prod (Multiset.pmap (fun a x => X - ↑C a) (roots (Polynomial.map (algebraMap K L) p)) hF) =
    ↑C (↑(algebraMap { x // x ∈ F } L) (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p))) *
      Multiset.prod
        (Multiset.pmap (fun a h => X - ↑C (↑(algebraMap { x // x ∈ F } L) { val := a, property := h }))
          (roots (Polynomial.map (algebraMap K L) p)) hF)
[PROOFSTEP]
rfl