internlm/Lean-Github huggingface dataset:
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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⟩
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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]
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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⟩
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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⟩
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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']
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
⊢ ∀ (i : ℕ) (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
Tactic:
intro i
Proof state after:
α : Type u_1
f : α → List α
i : ℕ
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
i : ℕ
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
Tactic:
induction i
Proof state after:
case zero
α : Type u_1
f : α → List α
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y

case succ
α : Type u_1
f : α → List α
n✝ : ℕ
a✝ : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[n✝] X ⊆ (fun X => (List.map f X).join)^[n✝] Y
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[n✝ + 1] X ⊆ (fun X => (List.map f X).join)^[n✝ + 1] Y
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
case zero =>
  intro X Y
  intro X_sub_Y
  simp at *
  assumption
Proof state after:
no goals
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
Tactic:
case succ i IH =>
  intro X Y
  simp
  intro X_sub_Y
  apply IH
  have := List.map_subset f X_sub_Y
  intro a a_in
  aesop
Proof state after:
no goals
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
intro X Y
Proof state after:
α : Type u_1
f : α → List α
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
intro X_sub_Y
Proof state after:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
simp at *
Proof state after:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ X ⊆ Y
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ X ⊆ Y
Tactic:
assumption
Proof state after:
no goals
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
Tactic:
intro X Y
Proof state after:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
Tactic:
simp
Proof state after:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y →
    (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y →
    (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join
Tactic:
intro X_sub_Y
Proof state after:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join
Theorem: biUnion_subset
Proof state before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join
Tactic:
apply IH
Proof state after:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (List.map f X).join ⊆ (List.map f Y).join
Theorem: biUnion_subset
Proof state before:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (List.map f X).join ⊆ (List.map f Y).join
Tactic:
have := List.map_subset f X_sub_Y
Proof state after:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
⊢ (List.map f X).join ⊆ (List.map f Y).join
Theorem: biUnion_subset
Proof state before:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
⊢ (List.map f X).join ⊆ (List.map f Y).join
Tactic:
intro a a_in
Proof state after:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
a : α
a_in : a ∈ (List.map f X).join
⊢ a ∈ (List.map f Y).join
Theorem: biUnion_subset
Proof state before:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
a : α
a_in : a ∈ (List.map f X).join
⊢ a ∈ (List.map f Y).join
Tactic:
aesop
Proof state after:
no goals
Theorem: ftr.fromNth
Proof state before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
Tactic:
induction i
Proof state after:
case zero
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[0] [x] → y ∈ ftr f m isDec x

case succ
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝] [x] → y ∈ ftr f m isDec x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝ + 1] [x] → y ∈ ftr f m isDec x