internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⋏ q✝ᵇ ⟶ p✝ᵇ
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⋏ q✝ᵇ ⟶ q✝ᵇ
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⟶ q✝ᵇ ⟶ p✝ᵇ ⋏ q✝ᵇ
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⟶ p✝ᵇ ⋎ q✝ᵇ
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐊𝟒 ⊢! q✝ᵇ ⟶ p✝ᵇ ⋎ q✝ᵇ
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐒𝟒 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐊𝟒 ⊢! (p✝ᵇ ⟶ r✝ᵇ) ⟶ (q✝ᵇ ⟶ r✝ᵇ) ⟶ p✝ᵇ ⋎ q✝ᵇ ⟶ r✝ᵇ
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⟶ q✝ᵇ ⟶ p✝ᵇ
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐒𝟒 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ 𝐊𝟒 ⊢! (p✝ᵇ ⟶ q✝ᵇ ⟶ r✝ᵇ) ⟶ (p✝ᵇ ⟶ q✝ᵇ) ⟶ p✝ᵇ ⟶ r✝ᵇ
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! ((p✝ᵇ ⟶ ⊥) ⟶ ⊥) ⟶ p✝ᵇ
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p ⟷ pᵇ
Tactic:
induction p using Formula.rec' with
| hand p q ihp ihq => dsimp [BoxdotTranslation]; exact and_replace_iff! ihp ihq;
| hor p q ihp ihq => dsimp [BoxdotTranslation]; exact or_replace_iff! ihp ihq;
| himp p q ihp ihq => dsimp [BoxdotTranslation]; exact imp_replace_iff! ihp ihq;
| hbox p ihp =>
  dsimp [BoxdotTranslation];
  exact iff_trans! (box_iff! ihp) iff_box_boxdot!;
| _ => dsimp [BoxdotTranslation]; exact iff_id!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ (p ⋏ q)ᵇ
Tactic:
dsimp [BoxdotTranslation]
Proof state after:
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ pᵇ ⋏ qᵇ
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ pᵇ ⋏ qᵇ
Tactic:
exact and_replace_iff! ihp ihq
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hor
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋎ q ⟷ (p ⋎ q)ᵇ
Tactic:
dsimp [BoxdotTranslation]
Proof state after:
case hor
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋎ q ⟷ pᵇ ⋎ qᵇ
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hor
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋎ q ⟷ pᵇ ⋎ qᵇ
Tactic:
exact or_replace_iff! ihp ihq
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case himp
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! (p ⟶ q) ⟷ (p ⟶ q)ᵇ
Tactic:
dsimp [BoxdotTranslation]
Proof state after:
case himp
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! (p ⟶ q) ⟷ (pᵇ ⟶ qᵇ)
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case himp
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! (p ⟶ q) ⟷ (pᵇ ⟶ qᵇ)
Tactic:
exact imp_replace_iff! ihp ihq
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
⊢ 𝐒𝟒 ⊢! □p ⟷ (□p)ᵇ
Tactic:
dsimp [BoxdotTranslation]
Proof state after:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
⊢ 𝐒𝟒 ⊢! □p ⟷ ⊡pᵇ
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
⊢ 𝐒𝟒 ⊢! □p ⟷ ⊡pᵇ
Tactic:
exact iff_trans! (box_iff! ihp) iff_box_boxdot!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝ᵇ
Tactic:
dsimp [BoxdotTranslation]
Proof state after:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝
Theorem: LO.Modal.Standard.iff_boxdotTranslation_S4
Proof state before:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝
Tactic:
exact iff_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.S4_of_boxdotTranslatedK4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! pᵇ
⊢ 𝐒𝟒 ⊢! p
Tactic:
exact (conj₂'! iff_boxdotTranslation_S4) ⨀ (reducible_iff.mp $ reducible_K4_S4) h
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_S4_boxdotTranslatedK4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p ↔ 𝐊𝟒 ⊢! pᵇ
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p → 𝐊𝟒 ⊢! pᵇ

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Theorem: LO.Modal.Standard.iff_S4_boxdotTranslatedK4
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p → 𝐊𝟒 ⊢! pᵇ

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Tactic:
. apply boxdotTranslatedK4_of_S4;
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Theorem: LO.Modal.Standard.iff_S4_boxdotTranslatedK4
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Tactic:
. apply S4_of_boxdotTranslatedK4;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_S4_boxdotTranslatedK4
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p → 𝐊𝟒 ⊢! pᵇ
Tactic:
apply boxdotTranslatedK4_of_S4
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_S4_boxdotTranslatedK4
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Tactic:
apply S4_of_boxdotTranslatedK4
Proof state after:
no goals
Theorem: Nat.ne_step_max
Proof state before:
α : ℕ → Sort u
n m : ℕ
⊢ n ≤ max n m
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.ne_step_max'
Proof state before:
α : ℕ → Sort u
n m : ℕ
⊢ n ≤ max m n
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.rec_eq
Proof state before:
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
H : ∀ m < n, ∀ (a : α), f₁ m a = f₂ m a
⊢ rec a f₁ n = rec a f₂ n
Tactic:
induction' n with n ih <;> simp
Proof state after:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)
Theorem: Nat.rec_eq
Proof state before:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)
Tactic:
have : (n.rec a f₁ : α) = n.rec a f₂ := ih (fun m hm a =>  H m (Nat.lt.step hm) a)
Proof state after:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
this : rec a f₁ n = rec a f₂ n
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)
Theorem: Nat.rec_eq
Proof state before:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
this : rec a f₁ n = rec a f₂ n
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)
Tactic:
simpa[this] using H n (Nat.lt.base n) (n.rec a f₂)
Proof state after:
no goals
Theorem: Nat.least_number
Proof state before:
α : ℕ → Sort u
P : ℕ → Prop
hP : ∃ x, P x
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Tactic:
rcases hP with ⟨n, hn⟩
Proof state after:
case intro
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
hn : P n
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Theorem: Nat.least_number
Proof state before:
case intro
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
hn : P n
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Tactic:
induction' n using Nat.strongRec with n ih
Proof state after:
case intro.ind
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Theorem: Nat.least_number
Proof state before:
case intro.ind
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Tactic:
by_cases H : ∃ m < n, P m
Proof state after:
case pos
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
H : ∃ m < n, P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z

case neg
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
H : ¬∃ m < n, P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Theorem: Nat.least_number
Proof state before:
case pos
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
H : ∃ m < n, P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Tactic:
rcases H with ⟨m, hm, hPm⟩
Proof state after:
case pos.intro.intro
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
m : ℕ
hm : m < n
hPm : P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Theorem: Nat.least_number
Proof state before:
case pos.intro.intro
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
m : ℕ
hm : m < n
hPm : P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Tactic:
exact ih m hm hPm
Proof state after:
no goals
Theorem: Nat.least_number
Proof state before:
case neg
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
H : ¬∃ m < n, P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
Tactic:
exact ⟨n, hn, by simpa using H⟩
Proof state after:
no goals
Theorem: Nat.least_number
Proof state before:
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
H : ¬∃ m < n, P m
⊢ ∀ z < n, ¬P z
Tactic:
simpa using H
Proof state after:
no goals
Theorem: eq_finZeroElim
Proof state before:
α : Sort u
x : Fin 0 → α
⊢ ∀ (x_1 : Fin 0), x x_1 = finZeroElim x_1
Tactic:
rintro ⟨_, _⟩
Proof state after:
case mk
α : Sort u
x : Fin 0 → α
val✝ : ℕ
isLt✝ : val✝ < 0
⊢ x ⟨val✝, isLt✝⟩ = finZeroElim ⟨val✝, isLt✝⟩
Theorem: eq_finZeroElim
Proof state before:
case mk
α : Sort u
x : Fin 0 → α
val✝ : ℕ
isLt✝ : val✝ < 0
⊢ x ⟨val✝, isLt✝⟩ = finZeroElim ⟨val✝, isLt✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: Matrix.vecCons_zero
Proof state before:
n : ℕ
α : Type u
α✝ : Type u_1
a : α✝
n✝ : ℕ
s : Fin n✝ → α✝
⊢ (a :> s) 0 = a
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.vecCons_succ
Proof state before:
n : ℕ
α : Type u
α✝ : Type u_1
a : α✝
s : Fin n → α✝
i : Fin n
⊢ (a :> s) i.succ = s i
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.rightConcat_last
Proof state before:
n : ℕ
α : Type u
α✝ : Type u_1
s : Fin n → α✝
a : α✝
⊢ (s <: a) (last n) = a
Tactic:
simp[vecConsLast]
Proof state after:
no goals
Theorem: Matrix.rightConcat_castSucc
Proof state before:
n : ℕ
α : Type u
α✝ : Type u_1
s : Fin n → α✝
a : α✝
i : Fin n
⊢ (s <: a) i.castSucc = s i
Tactic:
simp[vecConsLast]
Proof state after:
no goals
Theorem: Matrix.zero_succ_eq_id
Proof state before:
n✝ : ℕ
α : Type u
n : ℕ
⊢ (0 :> succ) 0 = id 0
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.zero_succ_eq_id
Proof state before:
n✝ : ℕ
α : Type u
n : ℕ
⊢ ∀ (i : Fin n), (0 :> succ) i.succ = id i.succ
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.zero_cons_succ_eq_self
Proof state before:
n : ℕ
α : Type u
f : Fin (n + 1) → α
⊢ (f 0 :> fun x => f x.succ) = f
Tactic:
funext x
Proof state after:
case h
n : ℕ
α : Type u
f : Fin (n + 1) → α
x : Fin n.succ
⊢ (f 0 :> fun x => f x.succ) x = f x
Theorem: Matrix.zero_cons_succ_eq_self
Proof state before:
case h
n : ℕ
α : Type u
f : Fin (n + 1) → α
x : Fin n.succ
⊢ (f 0 :> fun x => f x.succ) x = f x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: Matrix.eq_vecCons
Proof state before:
n : ℕ
α : Type u
C : Type u_1
s : Fin (n + 1) → C
⊢ s 0 = (s 0 :> s ∘ succ) 0
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.eq_vecCons
Proof state before:
n : ℕ
α : Type u
C : Type u_1
s : Fin (n + 1) → C
⊢ ∀ (i : Fin n), s i.succ = (s 0 :> s ∘ succ) i.succ
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.vecCons_ext
Proof state before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
⊢ a₁ :> s₁ = a₂ :> s₂ → a₁ = a₂ ∧ s₁ = s₂
Tactic:
intros h
Proof state after:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Theorem: Matrix.vecCons_ext
Proof state before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
constructor
Proof state after:
case left
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂

case right
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ s₁ = s₂
Theorem: Matrix.vecCons_ext
Proof state before:
case left
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ a₁ = a₂
Tactic:
exact congrFun h 0
Proof state after:
no goals
Theorem: Matrix.vecCons_ext
Proof state before:
case right
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
⊢ s₁ = s₂
Tactic:
exact funext (fun i => by simpa using congrFun h (Fin.castSucc i + 1))
Proof state after:
no goals
Theorem: Matrix.vecCons_ext
Proof state before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ :> s₁ = a₂ :> s₂
i : Fin n
⊢ s₁ i = s₂ i
Tactic:
simpa using congrFun h (Fin.castSucc i + 1)
Proof state after:
no goals
Theorem: Matrix.vecCons_ext
Proof state before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
⊢ a₁ = a₂ ∧ s₁ = s₂ → a₁ :> s₁ = a₂ :> s₂
Tactic:
intros h
Proof state after:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ :> s₁ = a₂ :> s₂
Theorem: Matrix.vecCons_ext
Proof state before:
n : ℕ
α : Type u
a₁ a₂ : α
s₁ s₂ : Fin n → α
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ :> s₁ = a₂ :> s₂
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Matrix.vecCons_assoc
Proof state before:
n : ℕ
α : Type u
a b : α
s : Fin n → α
⊢ a :> s <: b = (a :> s) <: b
Tactic:
funext x
Proof state after:
case h
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin n.succ.succ
⊢ (a :> s <: b) x = ((a :> s) <: b) x
Theorem: Matrix.vecCons_assoc
Proof state before:
case h
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin n.succ.succ
⊢ (a :> s <: b) x = ((a :> s) <: b) x
Tactic:
cases' x using Fin.cases with x <;> simp
Proof state after:
case h.succ
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin (n + 1)
⊢ (s <: b) x = ((a :> s) <: b) x.succ
Theorem: Matrix.vecCons_assoc
Proof state before:
case h.succ
n : ℕ
α : Type u
a b : α
s : Fin n → α
x : Fin (n + 1)
⊢ (s <: b) x = ((a :> s) <: b) x.succ
Tactic:
cases x using Fin.lastCases <;> simp[Fin.succ_castSucc]
Proof state after:
no goals
Theorem: Matrix.comp_vecCons
Proof state before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
a : α
s : Fin n → α
i : Fin n.succ
⊢ f ((a :> s) 0) = (f a :> f ∘ s) 0
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.comp_vecCons
Proof state before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
a : α
s : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), f ((a :> s) i.succ) = (f a :> f ∘ s) i.succ
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.comp₀
Proof state before:
n : ℕ
α : Type u
δ✝ : Type u_1
f : α → δ✝
⊢ f ∘ ![] = ![]
Tactic:
simp[Matrix.empty_eq]
Proof state after:
no goals
Theorem: Matrix.comp₁
Proof state before:
n : ℕ
α : Type u
δ✝ : Type u_1
f : α → δ✝
a : α
⊢ f ∘ ![a] = ![f a]
Tactic:
simp[comp_vecCons'']
Proof state after:
no goals
Theorem: Matrix.comp₂
Proof state before:
n : ℕ
α : Type u
δ✝ : Type u_1
f : α → δ✝
a₁ a₂ : α
⊢ f ∘ ![a₁, a₂] = ![f a₁, f a₂]
Tactic:
simp[comp_vecCons'']
Proof state after:
no goals
Theorem: Matrix.comp₃
Proof state before:
n : ℕ
α : Type u
δ✝ : Type u_1
f : α → δ✝
a₁ a₂ a₃ : α
⊢ f ∘ ![a₁, a₂, a₃] = ![f a₁, f a₂, f a₃]
Tactic:
simp[comp_vecCons'']
Proof state after:
no goals
Theorem: Matrix.comp_vecConsLast
Proof state before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
a : α
s : Fin n → α
i : Fin n.succ
⊢ f ((s <: a) (last n)) = (f ∘ s <: f a) (last n)
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.comp_vecConsLast
Proof state before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
a : α
s : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), f ((s <: a) i.castSucc) = (f ∘ s <: f a) i.castSucc
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.vecHead_comp
Proof state before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
v : Fin (n + 1) → α
⊢ vecHead (f ∘ v) = f (vecHead v)
Tactic:
simp[vecHead]
Proof state after:
no goals
Theorem: Matrix.vecTail_comp
Proof state before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
v : Fin (n + 1) → α
⊢ vecTail (f ∘ v) = f ∘ vecTail v
Tactic:
simp[vecTail, Function.comp.assoc]
Proof state after:
no goals
Theorem: Matrix.vecConsLast_vecEmpty
Proof state before:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
⊢ (s <: a) x = ![a] x
Tactic:
have : 0 = Fin.last 0 := by rfl
Proof state after:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
this : 0 = last 0
⊢ (s <: a) x = ![a] x
Theorem: Matrix.vecConsLast_vecEmpty
Proof state before:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
this : 0 = last 0
⊢ (s <: a) x = ![a] x
Tactic:
cases' x using Fin.cases with i <;> simp[this]
Proof state after:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this : 0 = last 0
i : Fin 0
⊢ (s <: a) i.succ = a
Theorem: Matrix.vecConsLast_vecEmpty
Proof state before:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this : 0 = last 0
i : Fin 0
⊢ (s <: a) i.succ = a
Tactic:
have := i.isLt
Proof state after:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this✝ : 0 = last 0
i : Fin 0
this : ↑i < 0
⊢ (s <: a) i.succ = a
Theorem: Matrix.vecConsLast_vecEmpty
Proof state before:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this✝ : 0 = last 0
i : Fin 0
this : ↑i < 0
⊢ (s <: a) i.succ = a
Tactic:
contradiction
Proof state after:
no goals
Theorem: Matrix.vecConsLast_vecEmpty
Proof state before:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
⊢ 0 = last 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.constant_eq_singleton
Proof state before:
n : ℕ
α : Type u
a : α
⊢ (fun x => a) = ![a]
Tactic:
funext x
Proof state after:
case h
n : ℕ
α : Type u
a : α
x : Fin (Nat.succ 0)
⊢ a = ![a] x
Theorem: Matrix.constant_eq_singleton
Proof state before:
case h
n : ℕ
α : Type u
a : α
x : Fin (Nat.succ 0)
⊢ a = ![a] x
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.constant_eq_singleton'
Proof state before:
n : ℕ
α : Type u
v : Fin 1 → α
⊢ v = ![v 0]
Tactic:
funext x
Proof state after:
case h
n : ℕ
α : Type u
v : Fin 1 → α
x : Fin 1
⊢ v x = ![v 0] x
Theorem: Matrix.constant_eq_singleton'
Proof state before:
case h
n : ℕ
α : Type u
v : Fin 1 → α
x : Fin 1
⊢ v x = ![v 0] x
Tactic:
simp[Fin.eq_zero]
Proof state after:
no goals
Theorem: Matrix.constant_eq_vec₂
Proof state before:
n : ℕ
α : Type u
a : α
⊢ (fun x => a) = ![a, a]
Tactic:
funext x
Proof state after:
case h
n : ℕ
α : Type u
a : α
x : Fin (Nat.succ 0).succ
⊢ a = ![a, a] x
Theorem: Matrix.constant_eq_vec₂
Proof state before:
case h
n : ℕ
α : Type u
a : α
x : Fin (Nat.succ 0).succ
⊢ a = ![a, a] x
Tactic:
cases x using Fin.cases <;> simp[Fin.eq_zero]
Proof state after:
no goals
Theorem: Matrix.fun_eq_vec₂
Proof state before:
n : ℕ
α : Type u
v : Fin 2 → α
⊢ v = ![v 0, v 1]
Tactic:
funext x
Proof state after:
case h
n : ℕ
α : Type u
v : Fin 2 → α
x : Fin 2
⊢ v x = ![v 0, v 1] x
Theorem: Matrix.fun_eq_vec₂
Proof state before:
case h
n : ℕ
α : Type u
v : Fin 2 → α
x : Fin 2
⊢ v x = ![v 0, v 1] x
Tactic:
cases x using Fin.cases <;> simp[Fin.eq_zero]
Proof state after:
no goals
Theorem: Matrix.injective_vecCons
Proof state before:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
⊢ Function.Injective (a :> f)
Tactic:
have : ∀ i, f i ≠ a := fun i => (ha i).symm
Proof state after:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
⊢ Function.Injective (a :> f)
Theorem: Matrix.injective_vecCons
Proof state before:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
⊢ Function.Injective (a :> f)
Tactic:
intro i j
Proof state after:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i j : Fin n.succ
⊢ (a :> f) i = (a :> f) j → i = j
Theorem: Matrix.injective_vecCons
Proof state before:
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i j : Fin n.succ
⊢ (a :> f) i = (a :> f) j → i = j
Tactic:
cases i using Fin.cases <;> cases j using Fin.cases <;> simp[*]
Proof state after:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
⊢ f i✝¹ = f i✝ → i✝¹ = i✝
Theorem: Matrix.injective_vecCons
Proof state before:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
⊢ f i✝¹ = f i✝ → i✝¹ = i✝
Tactic:
intro hf
Proof state after:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
hf : f i✝¹ = f i✝
⊢ i✝¹ = i✝
Theorem: Matrix.injective_vecCons
Proof state before:
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
hf : f i✝¹ = f i✝
⊢ i✝¹ = i✝
Tactic:
exact h hf
Proof state after:
no goals
Theorem: Matrix.toList_length
Proof state before:
α : Type u_1
n : ℕ
v : Fin n → α
⊢ (toList v).length = n
Tactic:
induction n <;> simp[*]
Proof state after:
no goals
Theorem: Matrix.mem_toList_iff
Proof state before:
α : Type u_1
n : ℕ
v : Fin n → α
a : α
⊢ a ∈ toList v ↔ ∃ i, v i = a
Tactic:
induction n <;> simp[*]
Proof state after:
case succ
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) ↔ ∃ i, v i = a
Theorem: Matrix.mem_toList_iff
Proof state before:
case succ
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) ↔ ∃ i, v i = a
Tactic:
constructor
Proof state after:
case succ.mp
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) → ∃ i, v i = a

case succ.mpr
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (∃ i, v i = a) → a = v 0 ∨ ∃ i, v i.succ = a