Theorem: ftr.iff' (Pdl/Closure.lean)

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ y ∈ ftr f m isDec x ↔ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
constructor
State after:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ y ∈ ftr f m isDec x → y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ (y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z) → y ∈ ftr f m isDec x

State before:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ y ∈ ftr f m isDec x → y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
intro y_in
State after:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in : y ∈ ftr f m isDec x
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in : y ∈ ftr f m isDec x
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
unfold ftr at y_in
State after:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in :
  y ∈
    let x := x;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in :
  y ∈
    let x := x;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
simp at y_in
State after:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in : y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in : y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
cases y_in
State after:
case mp.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

case mp.inr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
case inr hyp =>
  right
  rcases hyp with ⟨a, a_in_x, y_in_ftr_a⟩
  rw [ftr.iff'] at y_in_ftr_a cases y_in_ftr_a
  case inl y_is_a =>
    subst y_is_a
    use x
    unfold ftr
    aesop
  case inr hyp =>
    rcases hyp with ⟨z, z_in_ftr_a, y_in_fz⟩
    use z
    rw [ftr.iff]
    aesop
State after:
no goals

State before:
case mp.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
left
State after:
case mp.inl.h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x

State before:
case mp.inl.h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x
Tactic:
assumption
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
right
State after:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
rcases hyp with ⟨a, a_in_x, y_in_ftr_a⟩
State after:
case h.intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
y_in_ftr_a : y ∈ ftr f m isDec a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case h.intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
y_in_ftr_a : y ∈ ftr f m isDec a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
rw [ftr.iff'] at y_in_ftr_a
State after:
case h.intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
y_in_ftr_a : y = a ∨ ∃ z ∈ ftr f m isDec a, y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case h.intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
y_in_ftr_a : y = a ∨ ∃ z ∈ ftr f m isDec a, y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
cases y_in_ftr_a
State after:
case h.intro.intro.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
h✝ : y = a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

case h.intro.intro.inr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
h✝ : ∃ z ∈ ftr f m isDec a, y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
y_is_a : y = a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
case inl y_is_a =>
  subst y_is_a
  use x
  unfold ftr
  aesop
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
hyp : ∃ z ∈ ftr f m isDec a, y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
case inr hyp =>
  rcases hyp with ⟨z, z_in_ftr_a, y_in_fz⟩
  use z
  rw [ftr.iff]
  aesop
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
y_is_a : y = a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
subst y_is_a
State after:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
use x
State after:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ x ∈ ftr f m isDec x ∧ y ∈ f x

State before:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ x ∈ ftr f m isDec x ∧ y ∈ f x
Tactic:
unfold ftr
State after:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ (x ∈
      let x := x;
      [x] ++
        (List.map
            (fun x_1 =>
              match x_1 with
              | ⟨y, y_in⟩ =>
                let_fun this := y_in;
                ftr f m isDec y)
            (f x).attach).join) ∧
    y ∈ f x

State before:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ (x ∈
      let x := x;
      [x] ++
        (List.map
            (fun x_1 =>
              match x_1 with
              | ⟨y, y_in⟩ =>
                let_fun this := y_in;
                ftr f m isDec y)
            (f x).attach).join) ∧
    y ∈ f x
Tactic:
aesop
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
hyp : ∃ z ∈ ftr f m isDec a, y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
rcases hyp with ⟨z, z_in_ftr_a, y_in_fz⟩
State after:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
z : α
z_in_ftr_a : z ∈ ftr f m isDec a
y_in_fz : y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
z : α
z_in_ftr_a : z ∈ ftr f m isDec a
y_in_fz : y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
use z
State after:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
z : α
z_in_ftr_a : z ∈ ftr f m isDec a
y_in_fz : y ∈ f z
⊢ z ∈ ftr f m isDec x ∧ y ∈ f z

State before:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
z : α
z_in_ftr_a : z ∈ ftr f m isDec a
y_in_fz : y ∈ f z
⊢ z ∈ ftr f m isDec x ∧ y ∈ f z
Tactic:
rw [ftr.iff]
State after:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
z : α
z_in_ftr_a : z ∈ ftr f m isDec a
y_in_fz : y ∈ f z
⊢ (z = x ∨ ∃ z_1 ∈ f x, z ∈ ftr f m isDec z_1) ∧ y ∈ f z

State before:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
z : α
z_in_ftr_a : z ∈ ftr f m isDec a
y_in_fz : y ∈ f z
⊢ (z = x ∨ ∃ z_1 ∈ f x, z ∈ ftr f m isDec z_1) ∧ y ∈ f z
Tactic:
aesop
State after:
no goals

State before:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ (y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z) → y ∈ ftr f m isDec x
Tactic:
intro claim
State after:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
⊢ y ∈ ftr f m isDec x

State before:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
⊢ y ∈ ftr f m isDec x
Tactic:
cases claim
State after:
case mpr.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y ∈ ftr f m isDec x

case mpr.inr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : ∃ z ∈ ftr f m isDec x, y ∈ f z
⊢ y ∈ ftr f m isDec x

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ z ∈ ftr f m isDec x, y ∈ f z
⊢ y ∈ ftr f m isDec x
Tactic:
case inr hyp =>
  rcases hyp with ⟨a, a_in_ftr_x, y_in_fa⟩
  rw [ftr.iff] at a_in_ftr_x
  cases a_in_ftr_x
  case inl a_is_x =>
    subst a_is_x
    unfold ftr
    unfold ftr
    aesop
  case inr hyp =>
    rcases hyp with ⟨z, z_in_fx, a_in_ftr_z⟩
    have y_in_ftr_z : y ∈ ftr f m isDec z := by
      rw [ftr.iff']
      right
      use a
    unfold ftr
    aesop
State after:
no goals

State before:
case mpr.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y ∈ ftr f m isDec x
Tactic:
unfold ftr
State after:
case mpr.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y ∈
    let x := x;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join

State before:
case mpr.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y ∈
    let x := x;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join
Tactic:
simp
State after:
case mpr.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a

State before:
case mpr.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
Tactic:
left
State after:
case mpr.inl.h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x

State before:
case mpr.inl.h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
h✝ : y = x
⊢ y = x
Tactic:
assumption
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ z ∈ ftr f m isDec x, y ∈ f z
⊢ y ∈ ftr f m isDec x
Tactic:
rcases hyp with ⟨a, a_in_ftr_x, y_in_fa⟩
State after:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_ftr_x : a ∈ ftr f m isDec x
y_in_fa : y ∈ f a
⊢ y ∈ ftr f m isDec x

State before:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_ftr_x : a ∈ ftr f m isDec x
y_in_fa : y ∈ f a
⊢ y ∈ ftr f m isDec x
Tactic:
rw [ftr.iff] at a_in_ftr_x
State after:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_ftr_x : a = x ∨ ∃ z ∈ f x, a ∈ ftr f m isDec z
y_in_fa : y ∈ f a
⊢ y ∈ ftr f m isDec x

State before:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_ftr_x : a = x ∨ ∃ z ∈ f x, a ∈ ftr f m isDec z
y_in_fa : y ∈ f a
⊢ y ∈ ftr f m isDec x
Tactic:
cases a_in_ftr_x
State after:
case intro.intro.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
h✝ : a = x
⊢ y ∈ ftr f m isDec x

case intro.intro.inr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
h✝ : ∃ z ∈ f x, a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
a_is_x : a = x
⊢ y ∈ ftr f m isDec x
Tactic:
case inl a_is_x =>
  subst a_is_x
  unfold ftr
  unfold ftr
  aesop
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
hyp : ∃ z ∈ f x, a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
Tactic:
case inr hyp =>
  rcases hyp with ⟨z, z_in_fx, a_in_ftr_z⟩
  have y_in_ftr_z : y ∈ ftr f m isDec z := by
    rw [ftr.iff']
    right
    use a
  unfold ftr
  aesop
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
a_is_x : a = x
⊢ y ∈ ftr f m isDec x
Tactic:
subst a_is_x
State after:
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈ ftr f m isDec a

State before:
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈ ftr f m isDec a
Tactic:
unfold ftr
State after:
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈
    let x := a;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join

State before:
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈
    let x := a;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join
Tactic:
unfold ftr
State after:
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈
    let x := a;
    [x] ++
      (List.map
          (fun x_1 =>
            let x := ↑x_1;
            [x] ++
              (List.map
                  (fun x_2 =>
                    match x_2 with
                    | ⟨y, y_in⟩ =>
                      let_fun this := y_in;
                      ftr f m isDec y)
                  (f x).attach).join)
          (f x).attach).join

State before:
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈
    let x := a;
    [x] ++
      (List.map
          (fun x_1 =>
            let x := ↑x_1;
            [x] ++
              (List.map
                  (fun x_2 =>
                    match x_2 with
                    | ⟨y, y_in⟩ =>
                      let_fun this := y_in;
                      ftr f m isDec y)
                  (f x).attach).join)
          (f x).attach).join
Tactic:
aesop
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
hyp : ∃ z ∈ f x, a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
Tactic:
rcases hyp with ⟨z, z_in_fx, a_in_ftr_z⟩
State after:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x

State before:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
Tactic:
have y_in_ftr_z : y ∈ ftr f m isDec z := by
  rw [ftr.iff']
  right
  use a
State after:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x

State before:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
Tactic:
unfold ftr
State after:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ y ∈
    let x := x;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join

State before:
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ y ∈
    let x := x;
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join
Tactic:
aesop
State after:
no goals

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec z
Tactic:
rw [ftr.iff']
State after:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ y = z ∨ ∃ z_1 ∈ ftr f m isDec z, y ∈ f z_1

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ y = z ∨ ∃ z_1 ∈ ftr f m isDec z, y ∈ f z_1
Tactic:
right
State after:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ ∃ z_1 ∈ ftr f m isDec z, y ∈ f z_1

State before:
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ ∃ z_1 ∈ ftr f m isDec z, y ∈ f z_1
Tactic:
use a
State after:
no goals

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)
y_in : y ∈ ftr f m isDec x
h✝² : ∃ a ∈ f x, y ∈ ftr f m isDec a
h✝¹ : ⋯ = ⋯
a : α
h✝ : a ∈ f x ∧ y ∈ ftr f m isDec a
a_in_x : a ∈ f x
y_in_ftr_a : y ∈ ftr f m isDec a
⊢ (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
    ⟨a, ⟨y, ⟨f, ⟨m, isDec⟩⟩⟩⟩ ⟨x, ⟨y, ⟨f, ⟨m, isDec⟩⟩⟩⟩

α : 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:
all_goals (simp_wf; apply isDec; tauto)
State after:
no goals

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)
State after:
no goals

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
State after:
α : 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
⊢ m z < m x

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
⊢ m z < m x
Tactic:
apply isDec
State after:
case a
α : 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
⊢ z ∈ f x

State before:
case a
α : 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
⊢ z ∈ f x
Tactic:
tauto
State after:
no goals