Theorem: ftr.iff'
Proof state before:
α : Type
x✝ : (_ : α) ×' (_ : α) ×' (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x
a✝⁴ :
  ∀ (y : (_ : α) ×' (_ : α) ×' (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x),
    (invImage
            (fun x =>
              PSigma.casesOn x fun x y =>
                PSigma.casesOn y fun y f => PSigma.casesOn f fun f m => PSigma.casesOn m fun m isDec => m x)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      (y.2.1 ∈ ftr y.2.2.1 y.2.2.2.1 ⋯ y.1 ↔ y.2.1 = y.1 ∨ ∃ z ∈ ftr y.2.2.1 y.2.2.2.1 ⋯ y.1, y.2.1 ∈ y.2.2.1 z)
x : α
y✝ : (_ : α) ×' (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x
a✝³ :
  ∀ (y : (_ : α) ×' (_ : α) ×' (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x),
    (invImage
            (fun x =>
              PSigma.casesOn x fun x y =>
                PSigma.casesOn y fun y f => PSigma.casesOn f fun f m => PSigma.casesOn m fun m isDec => m x)
            instWellFoundedRelationOfSizeOf).1
        y ⟨x, y✝⟩ →
      (y.2.1 ∈ ftr y.2.2.1 y.2.2.2.1 ⋯ y.1 ↔ y.2.1 = y.1 ∨ ∃ z ∈ ftr y.2.2.1 y.2.2.2.1 ⋯ y.1, y.2.1 ∈ y.2.2.1 z)
y : α
f✝ : (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x
a✝² :
  ∀ (y_1 : (_ : α) ×' (_ : α) ×' (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x),
    (invImage
            (fun x =>
              PSigma.casesOn x fun x y =>
                PSigma.casesOn y fun y f => PSigma.casesOn f fun f m => PSigma.casesOn m fun m isDec => m x)
            instWellFoundedRelationOfSizeOf).1
        y_1 ⟨x, ⟨y, f✝⟩⟩ →
      (y_1.2.1 ∈ ftr y_1.2.2.1 y_1.2.2.2.1 ⋯ y_1.1 ↔
        y_1.2.1 = y_1.1 ∨ ∃ z ∈ ftr y_1.2.2.1 y_1.2.2.2.1 ⋯ y_1.1, y_1.2.1 ∈ y_1.2.2.1 z)
f : α → List α
m✝ : (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x
a✝¹ :
  ∀ (y_1 : (_ : α) ×' (_ : α) ×' (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x),
    (invImage
            (fun x =>
              PSigma.casesOn x fun x y =>
                PSigma.casesOn y fun y f => PSigma.casesOn f fun f m => PSigma.casesOn m fun m isDec => m x)
            instWellFoundedRelationOfSizeOf).1
        y_1 ⟨x, ⟨y, ⟨f, m✝⟩⟩⟩ →
      (y_1.2.1 ∈ ftr y_1.2.2.1 y_1.2.2.2.1 ⋯ y_1.1 ↔
        y_1.2.1 = y_1.1 ∨ ∃ z ∈ ftr y_1.2.2.1 y_1.2.2.2.1 ⋯ y_1.1, y_1.2.1 ∈ y_1.2.2.1 z)
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a✝ :
  ∀ (y_1 : (_ : α) ×' (_ : α) ×' (f : α → List α) ×' (m : α → ℕ) ×' ∀ (x y : α), y ∈ f x → m y < m x),
    (invImage
            (fun x =>
              PSigma.casesOn x fun x y =>
                PSigma.casesOn y fun y f => PSigma.casesOn f fun f m => PSigma.casesOn m fun m isDec => m x)
            instWellFoundedRelationOfSizeOf).1
        y_1 ⟨x, ⟨y, ⟨f, ⟨m, isDec⟩⟩⟩⟩ →
      (y_1.2.1 ∈ ftr y_1.2.2.1 y_1.2.2.2.1 ⋯ y_1.1 ↔
        y_1.2.1 = y_1.1 ∨ ∃ z ∈ ftr y_1.2.2.1 y_1.2.2.2.1 ⋯ y_1.1, y_1.2.1 ∈ y_1.2.2.1 z)
claim : y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
h✝⁵ : ∃ z ∈ ftr f m isDec x, y ∈ f z
h✝⁴ : claim = ⋯
a : α
h✝³ : a ∈ ftr f m isDec x ∧ y ∈ f a
a_in_ftr_x : a ∈ ftr f m isDec x
y_in_fa : y ∈ f a
h✝² : ∃ z ∈ f x, a ∈ ftr f m isDec z
h✝¹ : ⋯ = ⋯
z : α
h✝ : z ∈ f x ∧ a ∈ ftr f m isDec z
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ (invImage
        (fun x =>
          PSigma.casesOn x fun x y =>
            PSigma.casesOn y fun y f => PSigma.casesOn f fun f m => PSigma.casesOn m fun m isDec => m x)
        instWellFoundedRelationOfSizeOf).1
    ⟨z, ⟨y, ⟨f, ⟨m, isDec⟩⟩⟩⟩ ⟨x, ⟨y, ⟨f, ⟨m, isDec⟩⟩⟩⟩
Tactic:
(simp_wf; apply isDec; tauto)
Proof state after:
no goals