internlm/Lean-Github huggingface dataset:
Theorem: Nat.ArithPart₁.of_partrec
Proof state before:
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
⊢ ArithPart₁ f
Tactic:
induction hf
Proof state after:
case prim
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
a✝ : Primrec' f✝
⊢ ArithPart₁ ↑f✝

case comp
n : ℕ
f : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f✝
a✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
a_ih✝¹ : ArithPart₁ f✝
a_ih✝ : ∀ (i : Fin n✝), ArithPart₁ (g✝ i)
⊢ ArithPart₁ fun v => (mOfFn fun i => g✝ i v) >>= f✝

case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
a_ih✝ : ArithPart₁ ↑f✝
⊢ ArithPart₁ fun v => rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))
Theorem: Nat.ArithPart₁.of_partrec
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
hf : Primrec' f
⊢ ArithPart₁ ↑f
Tactic:
case prim f hf          => exact of_primrec hf
Proof state after:
no goals
Theorem: Nat.ArithPart₁.of_partrec
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f
a✝ : ∀ (i : Fin n✝), Partrec' (g i)
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
⊢ ArithPart₁ fun v => (mOfFn fun i => g i v) >>= f
Tactic:
case comp f g _ _ hf hg => exact hf.comp _ hg
Proof state after:
no goals
Theorem: Nat.ArithPart₁.of_partrec
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f
hf : ArithPart₁ ↑f
⊢ ArithPart₁ fun v => rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
case rfind f _ hf       => exact ArithPart₁.rfind hf
Proof state after:
no goals
Theorem: Nat.ArithPart₁.of_partrec
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
hf : Primrec' f
⊢ ArithPart₁ ↑f
Tactic:
exact of_primrec hf
Proof state after:
no goals
Theorem: Nat.ArithPart₁.of_partrec
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f
a✝ : ∀ (i : Fin n✝), Partrec' (g i)
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
⊢ ArithPart₁ fun v => (mOfFn fun i => g i v) >>= f
Tactic:
exact hf.comp _ hg
Proof state after:
no goals
Theorem: Nat.ArithPart₁.of_partrec
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f
hf : ArithPart₁ ↑f
⊢ ArithPart₁ fun v => rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
exact ArithPart₁.rfind hf
Proof state after:
no goals
Theorem: Nat.ArithPart₁.exists_code
Proof state before:
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Tactic:
rcases exists_code hf with ⟨cf, hcf⟩
Proof state after:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Theorem: Nat.ArithPart₁.exists_code
Proof state before:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Tactic:
choose cg hcg using fun i            => exists_code (hg i)
Proof state after:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
cg : Fin n✝ → Code n✝¹
hcg : ∀ (i : Fin n✝), (cg i).eval (g i)
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Theorem: Nat.ArithPart₁.exists_code
Proof state before:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
cg : Fin n✝ → Code n✝¹
hcg : ∀ (i : Fin n✝), (cg i).eval (g i)
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Tactic:
exact ⟨cf.comp cg, Code.eval.comp cf cg f g hcf hcg⟩
Proof state after:
no goals
Theorem: Nat.ArithPart₁.exists_code
Proof state before:
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : ArithPart₁ ↑f
⊢ ∃ c, c.eval fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
rcases exists_code hf with ⟨cf, hcf⟩
Proof state after:
case intro
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : ArithPart₁ ↑f
cf : Code (n✝ + 1)
hcf : cf.eval ↑f
⊢ ∃ c, c.eval fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Theorem: Nat.ArithPart₁.exists_code
Proof state before:
case intro
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : ArithPart₁ ↑f
cf : Code (n✝ + 1)
hcf : cf.eval ↑f
⊢ ∃ c, c.eval fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
exact ⟨cf.rfind, Code.eval.rfind cf f hcf⟩
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
⊢ F ⊧* .𝟯 → Connected F.Rel
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
⊢ ¬Connected F.Rel → ¬F ⊧* .𝟯
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
⊢ ¬Connected F.Rel → ¬F ⊧* .𝟯
Tactic:
intro hCon
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : ¬Connected F.Rel
⊢ ¬F ⊧* .𝟯
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : ¬Connected F.Rel
⊢ ¬F ⊧* .𝟯
Tactic:
simp [Connected] at hCon
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x x_2 ∧ ¬F.Rel x_1 x_2 ∧ ¬F.Rel x_2 x_1
⊢ ¬F ⊧* .𝟯
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x x_2 ∧ ¬F.Rel x_1 x_2 ∧ ¬F.Rel x_2 x_1
⊢ ¬F ⊧* .𝟯
Tactic:
obtain ⟨x, y, rxy, z, ryz, nryz, nrzy⟩ := hCon
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
⊢ ¬F ⊧* .𝟯
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
⊢ ¬F ⊧* .𝟯
Tactic:
simp [ValidOnFrame]
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)
Tactic:
obtain ⟨f, finv, fInj⟩ := atleast.mapping
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)
Tactic:
existsi f 0, f 1, (λ w a =>
  match (finv a) with
  | 0 => y ≺ w
  | 1 => z ≺ w
)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ¬ValidOnModel
      { Frame := F,
        Valuation := fun w a =>
          match finv a with
          | 0 => y ≺ w
          | 1 => z ≺ w }
      (Axioms.Dot3 (atom (f 0)) (atom (f 1)))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ¬ValidOnModel
      { Frame := F,
        Valuation := fun w a =>
          match finv a with
          | 0 => y ≺ w
          | 1 => z ≺ w }
      (Axioms.Dot3 (atom (f 0)) (atom (f 1)))
Tactic:
simp [ValidOnModel, not_forall, Axioms.Dot3]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x,
    (∃ x_1,
        x ≺ x_1 ∧
          (∀ (w' : F.World),
              x_1 ≺ w' →
                Satisfies
                  { Frame := F,
                    Valuation := fun w a =>
                      match finv a with
                      | 0 => y ≺ w
                      | 1 => z ≺ w }
                  w' (atom (f 0))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 1))) ∧
      ∃ x_1,
        x ≺ x_1 ∧
          (∀ (w' : F.World),
              x_1 ≺ w' →
                Satisfies
                  { Frame := F,
                    Valuation := fun w a =>
                      match finv a with
                      | 0 => y ≺ w
                      | 1 => z ≺ w }
                  w' (atom (f 1))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 0))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x,
    (∃ x_1,
        x ≺ x_1 ∧
          (∀ (w' : F.World),
              x_1 ≺ w' →
                Satisfies
                  { Frame := F,
                    Valuation := fun w a =>
                      match finv a with
                      | 0 => y ≺ w
                      | 1 => z ≺ w }
                  w' (atom (f 0))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 1))) ∧
      ∃ x_1,
        x ≺ x_1 ∧
          (∀ (w' : F.World),
              x_1 ≺ w' →
                Satisfies
                  { Frame := F,
                    Valuation := fun w a =>
                      match finv a with
                      | 0 => y ≺ w
                      | 1 => z ≺ w }
                  w' (atom (f 1))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 0))
Tactic:
existsi x
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∃ x_1,
      x ≺ x_1 ∧
        (∀ (w' : F.World),
            x_1 ≺ w' →
              Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                w' (atom (f 0))) ∧
          ¬Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              x_1 (atom (f 1))) ∧
    ∃ x_1,
      x ≺ x_1 ∧
        (∀ (w' : F.World),
            x_1 ≺ w' →
              Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                w' (atom (f 1))) ∧
          ¬Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              x_1 (atom (f 0))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∃ x_1,
      x ≺ x_1 ∧
        (∀ (w' : F.World),
            x_1 ≺ w' →
              Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                w' (atom (f 0))) ∧
          ¬Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              x_1 (atom (f 1))) ∧
    ∃ x_1,
      x ≺ x_1 ∧
        (∀ (w' : F.World),
            x_1 ≺ w' →
              Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                w' (atom (f 1))) ∧
          ¬Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              x_1 (atom (f 0))
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 0))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 1))

case intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 1))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 0))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 0))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 1))

case intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 1))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 0))
Tactic:
. existsi y;
  constructor;
  . assumption;
  . simp_all [Satisfies, (fInj 0), (fInj 1)];
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 1))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 0))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 1))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 0))
Tactic:
. existsi z;
  constructor;
  . assumption;
  . simp_all [Satisfies, (fInj 0), (fInj 1)];
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 0))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 1))
Tactic:
existsi y
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ y ∧
    (∀ (w' : F.World),
        y ≺ w' →
          Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            w' (atom (f 0))) ∧
      ¬Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          y (atom (f 1))