internlm/Lean-Github huggingface dataset:
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : Relation.ReflTransGen (relate M a) w x
⊢ evaluate M x φ
Tactic:
rw [starIffFinitelyManyStepsModel] at w_starA_x
Proof state after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : ∃ n ys, w = ys.head ∧ x = ys.last ∧ ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M x φ
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : ∃ n ys, w = ys.head ∧ x = ys.last ∧ ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M x φ
Tactic:
rcases w_starA_x with ⟨n, ys, w_is_head, x_is_last, i_a_isucc⟩
Proof state after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M x φ
Theorem: inductionAxiom
Proof state before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : ∀ (i : Fin n.succ), evaluate M (ys.get i) φ
⊢ evaluate M x φ
Tactic:
specialize claim n.succ
Proof state after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M (ys.get ↑n.succ) φ
⊢ evaluate M x φ
Theorem: inductionAxiom
Proof state before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M (ys.get ↑n.succ) φ
⊢ evaluate M x φ
Tactic:
simp at claim
Proof state after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ evaluate M x φ
Theorem: inductionAxiom
Proof state before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ evaluate M x φ
Tactic:
have x_is_ys_nsucc : x = ys.get (n + 1) :=
  by
  simp [Vector.last_def] at x_is_last
  sorry
Proof state after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M x φ
Theorem: inductionAxiom
Proof state before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M x φ
Tactic:
rw [x_is_ys_nsucc]
Proof state after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M (ys.get (↑n + 1)) φ
Theorem: inductionAxiom
Proof state before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M (ys.get (↑n + 1)) φ
Tactic:
sorry
Proof state after:
no goals
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ ∀ (i : Fin n.succ), evaluate M (ys.get i) φ
Tactic:
apply Fin.induction
Proof state after:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get 0) φ

case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ ∀ (i : Fin n), evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Theorem: inductionAxiom
Proof state before:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get 0) φ
Tactic:
simp
Proof state after:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M ys.head φ
Theorem: inductionAxiom
Proof state before:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M ys.head φ
Tactic:
rw [← w_is_head]
Proof state after:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M w φ
Theorem: inductionAxiom
Proof state before:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M w φ
Tactic:
exact Mwφ
Proof state after:
no goals
Theorem: inductionAxiom
Proof state before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ ∀ (i : Fin n), evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Tactic:
intro i
Proof state after:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
i : Fin n
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Theorem: inductionAxiom
Proof state before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
i : Fin n
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Tactic:
specialize i_a_isucc i
Proof state after:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Theorem: inductionAxiom
Proof state before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Tactic:
intro sat_phi
Proof state after:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
sat_phi : evaluate M (ys.get i.castSucc) φ
⊢ evaluate M (ys.get i.succ) φ
Theorem: inductionAxiom
Proof state before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
sat_phi : evaluate M (ys.get i.castSucc) φ
⊢ evaluate M (ys.get i.succ) φ
Tactic:
sorry
Proof state after:
no goals
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ x = ys.get (↑n + 1)
Tactic:
simp [Vector.last_def] at x_is_last
Proof state after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.get (Fin.last n)
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ x = ys.get (↑n + 1)
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.get (Fin.last n)
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ x = ys.get (↑n + 1)
Tactic:
sorry
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
⊢ y ∈ ftr f m isDec x ↔ y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
Tactic:
constructor
Proof 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 ∈ f x, y ∈ ftr f m isDec z

case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ (y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z) → y ∈ ftr f m isDec x
Theorem: ftr.iff
Proof 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 ∈ f x, y ∈ ftr f m isDec z
Tactic:
intro y_in
Proof 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 ∈ f x, y ∈ ftr f m isDec z
Theorem: ftr.iff
Proof 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 ∈ f x, y ∈ ftr f m isDec z
Tactic:
unfold ftr at y_in
Proof 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 ∈ f x, y ∈ ftr f m isDec z
Theorem: ftr.iff
Proof 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 ∈ f x, y ∈ ftr f m isDec z
Tactic:
simp at y_in
Proof 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 ∈ f x, y ∈ ftr f m isDec z
Theorem: ftr.iff
Proof 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 ∈ f x, y ∈ ftr f m isDec z
Tactic:
convert y_in
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 ∈ f x, y ∈ ftr f m isDec 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 ∈ f x, y ∈ ftr f m isDec 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 ∈ f x, y ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
Tactic:
unfold ftr
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 ∈ f x, 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 mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ f x, 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:
simp
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 ∈ f x, y ∈ ftr f m isDec z
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
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 ∈ f x, y ∈ ftr f m isDec z
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
Tactic:
convert claim
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
⊢ y ∈ ftr f m isDec x ↔ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
constructor
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
Proof state after:
no goals
Theorem: ftr.iff'
Proof 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
Proof 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
Theorem: ftr.iff'
Proof 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
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 : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
right
Proof 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
Theorem: ftr.iff'
Proof 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⟩
Proof 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
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 ∈ ftr f m isDec a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
rw [ftr.iff'] at y_in_ftr_a
Proof 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