internlm/Lean-Github huggingface dataset:
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h.h.h.fz
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ Vec.append1 Vec.nil (x 0) Fin2.fz = x Fin2.fz
Tactic:
simp [Vec.append1, OfNat.ofNat]
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h.h.h.fs
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
a✝ : Fin2 0
⊢ Vec.append1 Vec.nil (x 0) (Fin2.fs a✝) = x (Fin2.fs a✝)
Tactic:
contradiction
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
funext x
Proof state after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) x = F x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) x = F x
Tactic:
simp [ofCurriedAux, curriedAux]
Proof state after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Tactic:
let F' := fun α => F (α ::: x.last)
Proof state after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Tactic:
have : F x = F' x.drop := by simp [F']
Proof state after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Tactic:
rw [this]
Proof state after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F' (TypeVec.drop x)
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F' (TypeVec.drop x)
Tactic:
rw [@ih F']
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
⊢ F x = F' (TypeVec.drop x)
Tactic:
simp [F']
Proof state after:
no goals
Theorem: TypeFun.ofCurried_curried_involution
Proof state before:
n : ℕ
F : TypeFun n
⊢ ofCurried (curried F) = F
Tactic:
simp only [ofCurried, curried, ofCurriedAux_curriedAux_involution]
Proof state after:
n : ℕ
F : TypeFun n
⊢ reverseArgs (reverseArgs F) = F
Theorem: TypeFun.ofCurried_curried_involution
Proof state before:
n : ℕ
F : TypeFun n
⊢ reverseArgs (reverseArgs F) = F
Tactic:
apply reverseArgs_involution
Proof state after:
no goals
Theorem: MvQPF.Cofix.bisim_aux
Proof state before:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h' : ∀ (x : sorryAx (Type u_3) true), r x x
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.27762 r h' x y = ?m.27766 r h' x y
⊢ ∀ (x y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
intro x
Proof state after:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h' : ∀ (x : sorryAx (Type u_3) true), r x x
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.27762 r h' x y = ?m.27766 r h' x y
x : sorryAx (Type u_3) true
⊢ ∀ (y : sorryAx (Type u_3) true), r x y → x = y
Theorem: MvQPF.Cofix.bisim_aux
Proof state before:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h' : ∀ (x : sorryAx (Type u_3) true), r x x
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.27762 r h' x y = ?m.27766 r h' x y
x : sorryAx (Type u_3) true
⊢ ∀ (y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
rcases x
Proof state after:
no goals
Theorem: MvQPF.Cofix.bisim_rel
Proof state before:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
⊢ ∀ (x y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
let r' (x y) := x = y ∨ r x y
Proof state after:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
r' : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : sorryAx (Type u_3) true), r x y → x = y
Theorem: MvQPF.Cofix.bisim_rel
Proof state before:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
r' : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
intro x y rxy
Proof state after:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
r' : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop := fun x y => x = y ∨ r x y
x y : sorryAx (Type u_3) true
rxy : r x y
⊢ x = y
Theorem: MvQPF.liftR_map
Proof state before:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ LiftR' R (f <$$> x) (g <$$> x)
Tactic:
rw [LiftR_def]
Proof state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ ∃ u, (prod.fst ⊚ subtypeVal R) <$$> u = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> u = g <$$> x
Theorem: MvQPF.liftR_map
Proof state before:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ ∃ u, (prod.fst ⊚ subtypeVal R) <$$> u = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> u = g <$$> x
Tactic:
exists h <$$> x
Proof state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (prod.fst ⊚ subtypeVal R) <$$> h <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Theorem: MvQPF.liftR_map
Proof state before:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (prod.fst ⊚ subtypeVal R) <$$> h <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Tactic:
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, fst_prod_mk, comp_assoc, fst_diag]
Proof state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Theorem: MvQPF.liftR_map
Proof state before:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Tactic:
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, snd_prod_mk, comp_assoc, snd_diag]
Proof state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (g ⊚ TypeVec.id) <$$> x = g <$$> x
Theorem: MvQPF.liftR_map
Proof state before:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (g ⊚ TypeVec.id) <$$> x = g <$$> x
Tactic:
dsimp [LiftR']
Proof state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ f <$$> x = f <$$> x ∧ g <$$> x = g <$$> x
Theorem: MvQPF.liftR_map
Proof state before:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ repeat n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ f <$$> x = f <$$> x ∧ g <$$> x = g <$$> x
Tactic:
constructor <;> rfl
Proof state after:
no goals
Theorem: MvQPF.List.typeext
Proof state before:
α : Sort u_1
f g : α → Sort u_2
f_eq_g : f = g
⊢ ((a : α) → f a) = ((a : α) → g a)
Tactic:
cases f_eq_g
Proof state after:
case refl
α : Sort u_1
f : α → Sort u_2
⊢ ((a : α) → f a) = ((a : α) → f a)
Theorem: MvQPF.List.typeext
Proof state before:
case refl
α : Sort u_1
f : α → Sort u_2
⊢ ((a : α) → f a) = ((a : α) → f a)
Tactic:
rfl
Proof state after:
no goals
Theorem: MvQPF.Arrow.box_unbox_id
Proof state before:
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ box (unbox f) = f
Tactic:
simp[box, unbox]
Proof state after:
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ { fst := (),
      snd := fun x =>
        match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
        | Fin2.fz =>
          match f with
          | { fst := fst, snd := f } => f Fin2.fz } =
    f
Theorem: MvQPF.Arrow.box_unbox_id
Proof state before:
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ { fst := (),
      snd := fun x =>
        match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
        | Fin2.fz =>
          match f with
          | { fst := fst, snd := f } => f Fin2.fz } =
    f
Tactic:
apply congrArg
Proof state after:
case h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (fun x =>
      match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
      | Fin2.fz =>
        match f with
        | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd
Theorem: MvQPF.Arrow.box_unbox_id
Proof state before:
case h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (fun x =>
      match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
      | Fin2.fz =>
        match f with
        | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd
Tactic:
funext i
Proof state after:
case h.h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
i : Fin2 1
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) i with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd i
Theorem: MvQPF.Arrow.box_unbox_id
Proof state before:
case h.h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
i : Fin2 1
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) i with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd i
Tactic:
fin_cases i
Proof state after:
case h.h.head
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) Fin2.fz with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd Fin2.fz
Theorem: MvQPF.Arrow.box_unbox_id
Proof state before:
case h.h.head
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) Fin2.fz with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd Fin2.fz
Tactic:
rfl
Proof state after:
no goals
Theorem: MvQPF.Arrow.unbox_box_id
Proof state before:
α : Type
Γ : TypeVec.{0} 1
f : Arrow' α Γ
⊢ unbox (box f) = f
Tactic:
rfl
Proof state after:
no goals
Theorem: PFin2.toNat_lt
Proof state before:
n : ℕ
i : PFin2 n
⊢ toNat i < n
Tactic:
induction i
Proof state after:
case fz
n n✝ : ℕ
⊢ toNat fz < succ n✝

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : toNat a✝ < n✝
⊢ toNat (fs a✝) < succ n✝
Theorem: PFin2.toNat_lt
Proof state before:
n n✝ : ℕ
⊢ toNat fz < succ n✝
Tactic:
case fz       => apply succ_pos
Proof state after:
no goals
Theorem: PFin2.toNat_lt
Proof state before:
n n✝ : ℕ
a✝ : PFin2 n✝
ih : toNat a✝ < n✝
⊢ toNat (fs a✝) < succ n✝
Tactic:
case fs _ ih  => apply lt_succ_of_le ih
Proof state after:
no goals
Theorem: PFin2.toNat_lt
Proof state before:
n n✝ : ℕ
⊢ toNat fz < succ n✝
Tactic:
apply succ_pos
Proof state after:
no goals
Theorem: PFin2.toNat_lt
Proof state before:
n n✝ : ℕ
a✝ : PFin2 n✝
ih : toNat a✝ < n✝
⊢ toNat (fs a✝) < succ n✝
Tactic:
apply lt_succ_of_le ih
Proof state after:
no goals
Theorem: PFin2.inv_last_eq_fz
Proof state before:
n : ℕ
⊢ inv last = fz
Tactic:
induction n <;> simp [inv, last, weaken, *]
Proof state after:
no goals
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
n : ℕ
i : PFin2 n
⊢ inv (weaken i) = fs (inv i)
Tactic:
induction i
<;> simp[inv, weaken, last]
Proof state after:
case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (weaken a✝) = fs (inv a✝)
⊢ weaken (inv (weaken a✝)) = fs (inv (fs a✝))
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
n✝ n : ℕ
i : PFin2 n
ih : inv (weaken i) = fs (inv i)
⊢ weaken (inv (weaken i)) = fs (inv (fs i))
Tactic:
case fs n i ih =>
  simp[ih]
  cases n
  . contradiction
  . simp[inv, weaken]
Proof state after:
no goals
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
n✝ n : ℕ
i : PFin2 n
ih : inv (weaken i) = fs (inv i)
⊢ weaken (inv (weaken i)) = fs (inv (fs i))
Tactic:
simp[ih]
Proof state after:
n✝ n : ℕ
i : PFin2 n
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
n✝ n : ℕ
i : PFin2 n
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Tactic:
cases n
Proof state after:
case zero
n : ℕ
i : PFin2 zero
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))

case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
case zero
n : ℕ
i : PFin2 zero
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))

case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Tactic:
. contradiction
Proof state after:
case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Tactic:
. simp[inv, weaken]
Proof state after:
no goals
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
case zero
n : ℕ
i : PFin2 zero
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Tactic:
contradiction
Proof state after:
no goals
Theorem: PFin2.inv_weaken_eq_fs_inv
Proof state before:
case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Tactic:
simp[inv, weaken]
Proof state after:
no goals
Theorem: PFin2.inv_involution
Proof state before:
n : ℕ
i : PFin2 n
⊢ inv (inv i) = i
Tactic:
induction i
Proof state after:
case fz
n n✝ : ℕ
⊢ inv (inv fz) = fz

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (inv a✝) = a✝
⊢ inv (inv (fs a✝)) = fs a✝
Theorem: PFin2.inv_involution
Proof state before:
case fz
n n✝ : ℕ
⊢ inv (inv fz) = fz

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (inv a✝) = a✝
⊢ inv (inv (fs a✝)) = fs a✝
Tactic:
simp [inv]
Proof state after:
case fz
n n✝ : ℕ
⊢ inv last = fz

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (inv a✝) = a✝
⊢ inv (inv (fs a✝)) = fs a✝
Theorem: PFin2.inv_involution
Proof state before:
n n✝ : ℕ
⊢ inv last = fz
Tactic:
case fz => apply inv_last_eq_fz
Proof state after:
no goals
Theorem: PFin2.inv_involution
Proof state before:
n✝ n : ℕ
i : PFin2 n
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
case fs n i ih => {
  cases n;
  case zero => contradiction
  case succ n =>
    simp[inv]
    rw[inv_weaken_eq_fs_inv i.inv]
    apply congrArg
    apply ih
}
Proof state after:
no goals
Theorem: PFin2.inv_involution
Proof state before:
n n✝ : ℕ
⊢ inv last = fz
Tactic:
apply inv_last_eq_fz
Proof state after:
no goals
Theorem: PFin2.inv_involution
Proof state before:
n✝ n : ℕ
i : PFin2 n
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
cases n
Proof state after:
case zero
n : ℕ
i : PFin2 zero
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i

case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Theorem: PFin2.inv_involution
Proof state before:
n : ℕ
i : PFin2 zero
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
case zero => contradiction
Proof state after:
no goals
Theorem: PFin2.inv_involution
Proof state before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
case succ n =>
  simp[inv]
  rw[inv_weaken_eq_fs_inv i.inv]
  apply congrArg
  apply ih
Proof state after:
no goals
Theorem: PFin2.inv_involution
Proof state before:
n : ℕ
i : PFin2 zero
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
contradiction
Proof state after:
no goals
Theorem: PFin2.inv_involution
Proof state before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
simp[inv]
Proof state after:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (weaken (inv i)) = fs i
Theorem: PFin2.inv_involution
Proof state before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (weaken (inv i)) = fs i
Tactic:
rw[inv_weaken_eq_fs_inv i.inv]
Proof state after:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ fs (inv (inv i)) = fs i
Theorem: PFin2.inv_involution
Proof state before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ fs (inv (inv i)) = fs i
Tactic:
apply congrArg
Proof state after:
case h
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv i) = i
Theorem: PFin2.inv_involution
Proof state before:
case h
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv i) = i
Tactic:
apply ih
Proof state after:
no goals
Theorem: PFin2.ofFin2_toFin2
Proof state before:
n : ℕ
i : Fin2 n
⊢ toFin2 (ofFin2 i) = i
Tactic:
induction i <;> simp [ofFin2, toFin2, *]
Proof state after:
no goals
Theorem: PFin2.toFin2_ofFin2
Proof state before:
n : ℕ
i : PFin2 n
⊢ ofFin2 (toFin2 i) = i
Tactic:
induction i <;> simp [ofFin2, toFin2, *]
Proof state after:
no goals
Theorem: cast_trans
Proof state before:
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ cast h₂ (cast h₁ a) = cast ⋯ a
Tactic:
apply eq_of_heq
Proof state after:
case h
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₂ (cast h₁ a)) (cast ⋯ a)
Theorem: cast_trans
Proof state before:
case h
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₂ (cast h₁ a)) (cast ⋯ a)
Tactic:
apply HEq.trans (b:=cast h₁ a)
Proof state after:
case h.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₂ (cast h₁ a)) (cast h₁ a)

case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)
Theorem: cast_trans
Proof state before:
case h.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₂ (cast h₁ a)) (cast h₁ a)

case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)
Tactic:
apply cast_heq
Proof state after:
case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)
Theorem: cast_trans
Proof state before:
case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)
Tactic:
apply HEq.trans
Proof state after:
case h.h₂.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) ?h.h₂.b

case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq ?h.h₂.b (cast ⋯ a)

case h.h₂.β
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ Sort u_1

case h.h₂.b
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ ?h.h₂.β
Theorem: cast_trans
Proof state before:
case h.h₂.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) ?h.h₂.b

case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq ?h.h₂.b (cast ⋯ a)

case h.h₂.β
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ Sort u_1

case h.h₂.b
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ ?h.h₂.β
Tactic:
apply cast_heq
Proof state after:
case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq a (cast ⋯ a)
Theorem: cast_trans
Proof state before:
case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq a (cast ⋯ a)
Tactic:
apply HEq.symm
Proof state after:
case h.h₂.h₂.h
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast ⋯ a) a
Theorem: cast_trans
Proof state before:
case h.h₂.h₂.h
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast ⋯ a) a
Tactic:
apply cast_heq
Proof state after:
no goals
Theorem: heq_cast_left
Proof state before:
α α' β : Sort u_1
a : α
b : β
h : α = α'
⊢ HEq (cast h a) b = HEq a b
Tactic:
apply propext
Proof state after:
case a
α α' β : Sort u_1
a : α
b : β
h : α = α'
⊢ HEq (cast h a) b ↔ HEq a b