internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
Tactic:
. intro h x y z hxy hxz;
  have := h hxz;
  subst hxy this;
  trivial;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) → ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
Tactic:
intro h x y hyz
Proof state after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
⊢ x = y
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
⊢ x = y
Tactic:
have := h rfl hyz
Proof state after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
this : y = x
⊢ x = y
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
x y : F.World
hyz : F.Rel x y
this : y = x
⊢ x = y
Tactic:
subst this
Proof state after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
y : F.World
hyz : F.Rel y y
⊢ y = y
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ {x y z : F.World}, x = y → x ≺ z → z = y
y : F.World
hyz : F.Rel y y
⊢ y = y
Tactic:
trivial
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
Tactic:
intro h x y z hxy hxz
Proof state after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
⊢ z = y
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
⊢ z = y
Tactic:
have := h hxz
Proof state after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
this : x = z
⊢ z = y
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
this : x = z
⊢ z = y
Tactic:
subst hxy this
Proof state after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x : F.World
hxz : x ≺ x
⊢ x = x
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x : F.World
hxz : x ≺ x
⊢ x = x
Tactic:
trivial
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.functional_def
Proof state before:
α : Sort ?u.162721
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 1, j := 1, m := 0, n := 0 } F ↔ Functional F.Rel
Tactic:
simp [GeachConfluent, Functional]
Proof state after:
α : Sort ?u.162721
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x ≺ y → x ≺ z → z = y) ↔ ∀ ⦃w₁ w₂ w₃ : F.World⦄, F.Rel w₁ w₂ → F.Rel w₁ w₃ → w₂ = w₃
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.functional_def
Proof state before:
α : Sort ?u.162721
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x ≺ y → x ≺ z → z = y) ↔ ∀ ⦃w₁ w₂ w₃ : F.World⦄, F.Rel w₁ w₂ → F.Rel w₁ w₃ → w₂ = w₃
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.dense_def
Proof state before:
α : Sort ?u.204827
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 1, m := 2, n := 0 } F ↔ Dense F.Rel
Tactic:
simp [GeachConfluent, Dense]
Proof state after:
α : Sort ?u.204827
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → ∃ z_1, y ≺ z_1 ∧ z_1 ≺ z) ↔
    ∀ ⦃w₁ w₂ : F.World⦄, F.Rel w₁ w₂ → ∃ w₃, F.Rel w₁ w₃ ∧ F.Rel w₃ w₂
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.dense_def
Proof state before:
α : Sort ?u.204827
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → ∃ z_1, y ≺ z_1 ∧ z_1 ≺ z) ↔
    ∀ ⦃w₁ w₂ : F.World⦄, F.Rel w₁ w₂ → ∃ w₃, F.Rel w₁ w₃ ∧ F.Rel w₃ w₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.terminal_frame
Proof state before:
α : Sort ?u.253943
inst✝ : Inhabited α
F : Frame
t : Geach.Taple
⊢ GeachConfluent t Frame.terminal.toFrame
Tactic:
simp [GeachConfluent, Frame.terminal.relItr.mpr]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame
Proof state before:
α : Sort ?u.255218
inst✝ : Inhabited α
ts : List Geach.Taple
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
Tactic:
induction ts with
| nil => simp;
| cons t ts ih =>
  constructor;
  . exact Kripke.GeachConfluent.terminal_frame;
  . exact ih;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame
Proof state before:
case nil
α : Sort ?u.255218
inst✝ : Inhabited α
⊢ MultiGeachConfluent [] Frame.terminal.toFrame
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame
Proof state before:
case cons
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent (t :: ts) Frame.terminal.toFrame
Tactic:
constructor
Proof state after:
case cons.left
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ GeachConfluent t Frame.terminal.toFrame

case cons.right
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame
Proof state before:
case cons.left
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ GeachConfluent t Frame.terminal.toFrame

case cons.right
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
Tactic:
. exact Kripke.GeachConfluent.terminal_frame;
Proof state after:
case cons.right
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame
Proof state before:
case cons.right
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
Tactic:
. exact ih;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame
Proof state before:
case cons.left
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ GeachConfluent t Frame.terminal.toFrame
Tactic:
exact Kripke.GeachConfluent.terminal_frame
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame
Proof state before:
case cons.right
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
Tactic:
exact ih
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Formula.valAux_neg
Proof state before:
α : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
inst✝ : DeMorgan F
v : α → F
p : Formula α
⊢ valAux v (~p) = ~valAux v p
Tactic:
induction p using rec' <;> simp[*, valAux, ←neg_eq, or_iff_not_imp_left]
Proof state after:
no goals
Theorem: WType.SubWType.ext
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ w₂ : SubWType β s
⊢ ↑w₁ = ↑w₂ → w₁ = w₂
Tactic:
rcases w₁ with ⟨w₁, h₁⟩
Proof state after:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₂ : SubWType β s
w₁ : WType β
h₁ : w₁.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑w₂ → ⟨w₁, h₁⟩ = w₂
Theorem: WType.SubWType.ext
Proof state before:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₂ : SubWType β s
w₁ : WType β
h₁ : w₁.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑w₂ → ⟨w₁, h₁⟩ = w₂
Tactic:
rcases w₂ with ⟨w₂, h₂⟩
Proof state after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑⟨w₂, h₂⟩ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩
Theorem: WType.SubWType.ext
Proof state before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑⟨w₂, h₂⟩ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩
Tactic:
simp
Proof state after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ w₁ = w₂ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩
Theorem: WType.SubWType.ext
Proof state before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ w₁ = w₂ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩
Tactic:
rintro rfl
Proof state after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ : WType β
h₁ h₂ : w₁.depth ≤ s
⊢ ⟨w₁, h₁⟩ = ⟨w₁, h₂⟩
Theorem: WType.SubWType.ext
Proof state before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ : WType β
h₁ h₂ : w₁.depth ≤ s
⊢ ⟨w₁, h₁⟩ = ⟨w₁, h₂⟩
Tactic:
apply Subtype.ext (by simp)
Proof state after:
no goals
Theorem: WType.SubWType.ext
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
w₁ : WType β
h₁ h₂ : w₁.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑⟨w₁, h₂⟩
Tactic:
simp
Proof state after:
no goals
Theorem: WType.SubWType.cast_mk
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s s' : ℕ
hs : s + 1 = s' + 1
a : α
f : β a → SubWType β s
i : β a
⊢ s = s'
Tactic:
apply Nat.succ_inj'.mp hs
Proof state after:
no goals
Theorem: WType.SubWType.cast_mk_one
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
hs : s + 1 = 1
a : α
f : β a → SubWType β s
i : β a
⊢ s = 0
Tactic:
apply Nat.succ_inj'.mp hs
Proof state after:
no goals
Theorem: WType.SubWType.elim_const
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
w₁ : SubWType β s₁
w₂ : SubWType β s₂
h : ↑w₁ = ↑w₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
⊢ elim' γ fγ s₁ w₁ = elim' γ fγ s₂ w₂
Tactic:
rcases w₁ with ⟨w, hw₁⟩
Proof state after:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
w₂ : SubWType β s₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
h : ↑⟨w, hw₁⟩ = ↑w₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ w₂
Theorem: WType.SubWType.elim_const
Proof state before:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
w₂ : SubWType β s₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
h : ↑⟨w, hw₁⟩ = ↑w₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ w₂
Tactic:
rcases w₂ with ⟨w, hw₂⟩
Proof state after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : ↑⟨w✝, hw₁⟩ = ↑⟨w, hw₂⟩
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Theorem: WType.SubWType.elim_const
Proof state before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : ↑⟨w✝, hw₁⟩ = ↑⟨w, hw₂⟩
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Tactic:
simp at h
Proof state after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : w✝ = w
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Theorem: WType.SubWType.elim_const
Proof state before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : w✝ = w
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Tactic:
rcases h with rfl
Proof state after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
hw₂ : w.depth ≤ s₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Theorem: WType.SubWType.elim_const
Proof state before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
hw₂ : w.depth ≤ s₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Tactic:
simp[elim']
Proof state after:
no goals
Theorem: WType.SubWType.decode_zero
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
⊢ decode e = none
Tactic:
rcases (decode e) with (_ | w)
Proof state after:
case none
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
⊢ none = none

case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β 0
⊢ some w = none
Theorem: WType.SubWType.decode_zero
Proof state before:
case none
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
⊢ none = none
Tactic:
rfl
Proof state after:
no goals
Theorem: WType.SubWType.decode_zero
Proof state before:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β 0
⊢ some w = none
Tactic:
exact Empty.elim (equiv_zero w)
Proof state after:
no goals
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
a : α
l : List (SubWType β s)
v : Vector (SubWType β s) (Fintype.card (β a))
⊢ (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)).depth ≤ s + 1
Tactic:
simp[depth, Equiv.vectorEquivFin]
Proof state after:
no goals
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
x : (a : α) × (β a → SubWType β s)
⊢ (WType.mk x.fst fun b => ↑(x.snd b)).depth ≤ s + 1
Tactic:
simp[depth]
Proof state after:
no goals
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ decode e = Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯) (decode e)
Tactic:
simp[Primcodable.SubWType, primcodable_succ, Primcodable.ofEquiv_toEncodable]
Proof state after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ decode e =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ decode e =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))
Tactic:
rw[Encodable.decode_ofEquiv equiv_succ, equiv_succ]
Proof state after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ Option.map
      (⇑{
            toFun := fun x =>
              match x with
              | ⟨t, h⟩ =>
                WType.casesOn (motive := fun x => x.depth ≤ s + 1 → (a : α) × (β a → SubWType β s)) t
                  (fun a f h => ⟨a, fun b => ⟨f b, ⋯⟩⟩) h,
            invFun := fun x =>
              match x with
              | ⟨a, f⟩ => ofWType (WType.mk a fun b => ↑(f b)) (s + 1) ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm)
      (decode e) =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ Option.map
      (⇑{
            toFun := fun x =>
              match x with
              | ⟨t, h⟩ =>
                WType.casesOn (motive := fun x => x.depth ≤ s + 1 → (a : α) × (β a → SubWType β s)) t
                  (fun a f h => ⟨a, fun b => ⟨f b, ⋯⟩⟩) h,
            invFun := fun x =>
              match x with
              | ⟨a, f⟩ => ofWType (WType.mk a fun b => ↑(f b)) (s + 1) ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm)
      (decode e) =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))
Tactic:
simp
Proof state after:
no goals
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
a : α
x : β a → SubWType β s
⊢ (WType.mk a fun b => ↑(x b)).depth ≤ s + 1
Tactic:
simp[depth]
Proof state after:
no goals
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯) (decode e) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)
Tactic:
simp[Encodable.decode_sigma_val, Option.map_bind', Function.comp]
Proof state after:
no goals
Theorem: WType.SubWType.decode_succ
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)) =
    (decode e.unpair.1).bind fun a =>
      (decode e.unpair.2).bind fun l =>
        Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
          (List.toVector (Fintype.card (β a)) l)
Tactic:
congr
Proof state after:
case e_a
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ (fun a => Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)) = fun a =>
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)