internlm/Lean-Github huggingface dataset:
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle s p q r
Tactic:
apply quadrangle_rotate
Proof state after:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle r s p q
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle r s p q
Tactic:
apply quadrangle_rotate
Proof state after:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle q r s p
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle q r s p
Tactic:
apply quadrangle_rotate
Proof state after:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle p q r s
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
no goals
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear a c d
Tactic:
apply triangle_rotate
Proof state after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear d a c
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear d a c
Tactic:
apply triangle_rotate
Proof state after:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear c d a
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear c d a
Tactic:
apply dual_quadrangle_part
Proof state after:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle r s p q
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle r s p q
Tactic:
apply quadrangle_rotate
Proof state after:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle q r s p
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle q r s p
Tactic:
apply quadrangle_rotate
Proof state after:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle p q r s
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
no goals
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ ¬collinear b c d
Tactic:
apply dual_quadrangle_part
Proof state after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle q r s p
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle q r s p
Tactic:
apply quadrangle_rotate
Proof state after:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle p q r s
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
no goals
Theorem: ProjectivePlane.dual_involution
Proof state before:
P L : Type
p q r s : P
h : ProjectivePlane P
⊢ let h' := inferInstance;
  h' = h
Tactic:
rfl
Proof state after:
no goals
Theorem: Fano.Fano.quadrangle1236
Proof state before:
P L : Type
⊢ ¬collinear Points.p1 Points.p2 Points.p3
Tactic:
simp[collinear]
Proof state after:
no goals
Theorem: Fano.Fano.quadrangle1236
Proof state before:
P L : Type
⊢ ¬collinear Points.p1 Points.p2 Points.p6
Tactic:
simp[collinear]
Proof state after:
no goals
Theorem: Fano.Fano.quadrangle1236
Proof state before:
P L : Type
⊢ ¬collinear Points.p1 Points.p3 Points.p6
Tactic:
simp[collinear]
Proof state after:
no goals
Theorem: Fano.Fano.quadrangle1236
Proof state before:
P L : Type
⊢ ¬collinear Points.p2 Points.p3 Points.p6
Tactic:
simp[collinear]
Proof state after:
no goals
Theorem: Fano.Fano.point_line_uniq
Proof state before:
P L : Type
⊢ ∀ {p q : Points} {l m : Lines}, p ∈ l → q ∈ l → p ∈ m → q ∈ m → p = q ∨ l = m
Tactic:
decide
Proof state after:
no goals
Theorem: max_var_name_mem
Proof state before:
⊢ ∀ (v : String) (vars : List String), v ∈ vars → String.length v ≤ max_var_name vars
Tactic:
intro v vars
Proof state after:
v : String
vars : List String
⊢ v ∈ vars → String.length v ≤ max_var_name vars
Theorem: max_var_name_mem
Proof state before:
v : String
vars : List String
⊢ v ∈ vars → String.length v ≤ max_var_name vars
Tactic:
induction vars with
| nil =>
  intro hm
  exact absurd hm (List.not_mem_nil v)
| cons x xs ih =>
  intro h
  rw [List.mem_cons] at h
  cases h with
  | inl hvx =>
    unfold max_var_name
    conv => rhs; rw [← hvx]
    apply Nat.le_max_left
  | inr hvxs =>
    unfold max_var_name
    calc
      v.length ≤ max_var_name xs := ih hvxs
      _        ≤ Nat.max x.length (max_var_name xs) := by apply Nat.le_max_right
Proof state after:
no goals
Theorem: max_var_name_mem
Proof state before:
case nil
v : String
⊢ v ∈ [] → String.length v ≤ max_var_name []
Tactic:
intro hm
Proof state after:
case nil
v : String
hm : v ∈ []
⊢ String.length v ≤ max_var_name []
Theorem: max_var_name_mem
Proof state before:
case nil
v : String
hm : v ∈ []
⊢ String.length v ≤ max_var_name []
Tactic:
exact absurd hm (List.not_mem_nil v)
Proof state after:
no goals
Theorem: max_var_name_mem
Proof state before:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
⊢ v ∈ x :: xs → String.length v ≤ max_var_name (x :: xs)
Tactic:
intro h
Proof state after:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v ∈ x :: xs
⊢ String.length v ≤ max_var_name (x :: xs)
Theorem: max_var_name_mem
Proof state before:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v ∈ x :: xs
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
rw [List.mem_cons] at h
Proof state after:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v = x ∨ v ∈ xs
⊢ String.length v ≤ max_var_name (x :: xs)
Theorem: max_var_name_mem
Proof state before:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v = x ∨ v ∈ xs
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
cases h with
| inl hvx =>
  unfold max_var_name
  conv => rhs; rw [← hvx]
  apply Nat.le_max_left
| inr hvxs =>
  unfold max_var_name
  calc
    v.length ≤ max_var_name xs := ih hvxs
    _        ≤ Nat.max x.length (max_var_name xs) := by apply Nat.le_max_right
Proof state after:
no goals
Theorem: max_var_name_mem
Proof state before:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
unfold max_var_name
Proof state after:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)
Theorem: max_var_name_mem
Proof state before:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)
Tactic:
conv => rhs; rw [← hvx]
Proof state after:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length v) (max_var_name xs)
Theorem: max_var_name_mem
Proof state before:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length v) (max_var_name xs)
Tactic:
apply Nat.le_max_left
Proof state after:
no goals
Theorem: max_var_name_mem
Proof state before:
case cons.inr
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
unfold max_var_name
Proof state after:
case cons.inr
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)
Theorem: max_var_name_mem
Proof state before:
case cons.inr
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)
Tactic:
calc
  v.length ≤ max_var_name xs := ih hvxs
  _        ≤ Nat.max x.length (max_var_name xs) := by apply Nat.le_max_right
Proof state after:
no goals
Theorem: max_var_name_mem
Proof state before:
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ max_var_name xs ≤ Nat.max (String.length x) (max_var_name xs)
Tactic:
apply Nat.le_max_right
Proof state after:
no goals
Theorem: lexwhile_monotonic
Proof state before:
⊢ ∀ (p : Char → Bool) (inp : List Char), List.length (lexwhile p inp).snd ≤ List.length inp
Tactic:
intro p inp
Proof state after:
p : Char → Bool
inp : List Char
⊢ List.length (lexwhile p inp).snd ≤ List.length inp
Theorem: lexwhile_monotonic
Proof state before:
p : Char → Bool
inp : List Char
⊢ List.length (lexwhile p inp).snd ≤ List.length inp
Tactic:
induction inp with
| nil => simp [lexwhile]
| cons c cs ih =>
  simp [lexwhile]
  cases p c <;> simp
  exact Nat.le_succ_of_le ih
Proof state after:
no goals
Theorem: lexwhile_monotonic
Proof state before:
case nil
p : Char → Bool
⊢ List.length (lexwhile p []).snd ≤ List.length []
Tactic:
simp [lexwhile]
Proof state after:
no goals
Theorem: lexwhile_monotonic
Proof state before:
case cons
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length (lexwhile p (c :: cs)).snd ≤ List.length (c :: cs)
Tactic:
simp [lexwhile]
Proof state after:
case cons
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length
      (if p c = true then (String.append (Char.toString c) (lexwhile p cs).fst, (lexwhile p cs).snd)
        else ("", c :: cs)).snd ≤
    Nat.succ (List.length cs)
Theorem: lexwhile_monotonic
Proof state before:
case cons
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length
      (if p c = true then (String.append (Char.toString c) (lexwhile p cs).fst, (lexwhile p cs).snd)
        else ("", c :: cs)).snd ≤
    Nat.succ (List.length cs)
Tactic:
cases p c <;> simp
Proof state after:
case cons.true
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length (lexwhile p cs).snd ≤ Nat.succ (List.length cs)
Theorem: lexwhile_monotonic
Proof state before:
case cons.true
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length (lexwhile p cs).snd ≤ Nat.succ (List.length cs)
Tactic:
exact Nat.le_succ_of_le ih
Proof state after:
no goals
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
⊢ ∀ (l1 l2 : List α), List.length (merge l1 l2) = List.length l1 + List.length l2
Tactic:
intro l1 l2
Proof state after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length (merge l1 l2) = List.length l1 + List.length l2
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length (merge l1 l2) = List.length l1 + List.length l2
Tactic:
match l1 with
| .nil => unfold merge; rw [List.length_nil, Nat.zero_add]
| .cons h1 t1 =>
  unfold merge
  match l2 with
  | .nil => simp only [List.length_cons, List.length_nil, Nat.add_zero]
  | .cons h2 t2 =>
    simp only [List.length_cons]
    split
    . rw [List.length_cons, merge_length t1 (h2 :: t2)]
      simp only [List.length_cons]
      omega
    . rw [List.length_cons, merge_length (h1 :: t1) t2]
      simp only [List.length_cons]
      omega
Proof state after:
no goals
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length (merge [] l2) = List.length [] + List.length l2
Tactic:
unfold merge
Proof state after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length l2 = List.length [] + List.length l2
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length l2 = List.length [] + List.length l2
Tactic:
rw [List.length_nil, Nat.zero_add]
Proof state after:
no goals
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length (merge (h1 :: t1) l2) = List.length (h1 :: t1) + List.length l2
Tactic:
unfold merge
Proof state after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length
      (match l2 with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length l2
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length
      (match l2 with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length l2
Tactic:
match l2 with
| .nil => simp only [List.length_cons, List.length_nil, Nat.add_zero]
| .cons h2 t2 =>
  simp only [List.length_cons]
  split
  . rw [List.length_cons, merge_length t1 (h2 :: t2)]
    simp only [List.length_cons]
    omega
  . rw [List.length_cons, merge_length (h1 :: t1) t2]
    simp only [List.length_cons]
    omega
Proof state after:
no goals
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length
      (match [] with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length []
Tactic:
simp only [List.length_cons, List.length_nil, Nat.add_zero]
Proof state after:
no goals
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
⊢ List.length
      (match h2 :: t2 with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length (h2 :: t2)
Tactic:
simp only [List.length_cons]
Proof state after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
⊢ List.length (if isLE (compare h1 h2) = true then h1 :: merge t1 (h2 :: t2) else h2 :: merge (h1 :: t1) t2) =
    Nat.succ (List.length t1) + Nat.succ (List.length t2)
Theorem: Set.merge_length
Proof state before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
⊢ List.length (if isLE (compare h1 h2) = true then h1 :: merge t1 (h2 :: t2) else h2 :: merge (h1 :: t1) t2) =
    Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
split
Proof state after:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ List.length (h1 :: merge t1 (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Theorem: Set.merge_length
Proof state before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ List.length (h1 :: merge t1 (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
. rw [List.length_cons, merge_length t1 (h2 :: t2)]
  simp only [List.length_cons]
  omega
Proof state after:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Theorem: Set.merge_length
Proof state before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
. rw [List.length_cons, merge_length (h1 :: t1) t2]
  simp only [List.length_cons]
  omega
Proof state after:
no goals