internlm/Lean-Github huggingface dataset:
Theorem: Graph.SpanningSubtree.surroundEdge_cast
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v u' v' : V
huu' : u = u'
hvv' : v = v'
e : EdgeBetween G u v
e' : EdgeBetween G u' v'
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Tactic:
cases huu'
Proof state after:
case refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v' : V
hvv' : v = v'
e : EdgeBetween G u v
e' : EdgeBetween G u v'
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Theorem: Graph.SpanningSubtree.surroundEdge_cast
Proof state before:
case refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v' : V
hvv' : v = v'
e : EdgeBetween G u v
e' : EdgeBetween G u v'
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Tactic:
cases hvv'
Proof state after:
case refl.refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Theorem: Graph.SpanningSubtree.surroundEdge_cast
Proof state before:
case refl.refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Tactic:
congr
Proof state after:
case refl.refl.e_e
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e = e'
Theorem: Graph.SpanningSubtree.surroundEdge_cast
Proof state before:
case refl.refl.e_e
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e = e'
Tactic:
ext
Proof state after:
case refl.refl.e_e.edge
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e.edge = e'.edge
Theorem: Graph.SpanningSubtree.surroundEdge_cast
Proof state before:
case refl.refl.e_e.edge
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e.edge = e'.edge
Tactic:
exact hee'
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surroundEdge_bar'
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = inv (surroundEdge Γ (EdgeBetween.ofEdge e))
Tactic:
rw [← surroundEdge_bar]
Proof state after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = surroundEdge Γ (EdgeBetween.bar (EdgeBetween.ofEdge e))
Theorem: Graph.SpanningSubtree.surroundEdge_bar'
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = surroundEdge Γ (EdgeBetween.bar (EdgeBetween.ofEdge e))
Tactic:
apply surroundEdge_cast <;> simp
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_eq
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
⊢ surround Γ [[p]] = surroundEdgewise Γ p
Tactic:
induction p with
| nil _ => simp only [surround, Subgraph.contains_nil, SpanningSubgraph.spanning, Set.top_eq_univ, Set.mem_univ,
  Graph.PathClass.nil_eq_id, path_to_base_eq, Category.id_comp, IsIso.hom_inv_id, surroundEdgewise_nil]
| cons _ _ ih => simp only [surroundEdgewise_cons, ← ih, surround_cons]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_eq
Proof state before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v✝ : V
⊢ surround Γ [[EdgePath.nil v✝]] = surroundEdgewise Γ (EdgePath.nil v✝)
Tactic:
simp only [surround, Subgraph.contains_nil, SpanningSubgraph.spanning, Set.top_eq_univ, Set.mem_univ,
Graph.PathClass.nil_eq_id, path_to_base_eq, Category.id_comp, IsIso.hom_inv_id, surroundEdgewise_nil]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_eq
Proof state before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v✝ w✝ u✝ : V
a✝¹ : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
ih : surround Γ [[a✝]] = surroundEdgewise Γ a✝
⊢ surround Γ [[EdgePath.cons a✝¹ a✝]] = surroundEdgewise Γ (EdgePath.cons a✝¹ a✝)
Tactic:
simp only [surroundEdgewise_cons, ← ih, surround_cons]
Proof state after:
no goals
Theorem: label_path_map
Proof state before:
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
u v : V
p : Graph.EdgePath X u v
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) p = φ (Graph.SpanningSubtree.surround Γ [[p]])
Tactic:
induction p with
  | nil _ => rw [GroupLabelledGraph.pathLabel_nil, Graph.PathClass.nil_eq_id, Γ.surround_nil,
      Graph.π₁.one_def, map_one]
  | cons e p ih => simp only [Γ.surround_cons, GroupLabelledGraph.pathLabel_cons, ih,
      Graph.π₁.mul_def, map_mul, mul_right_cancel_iff, induced_label_eq_surround_map]
Proof state after:
no goals
Theorem: label_path_map
Proof state before:
case nil
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
u v v✝ : V
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) (Graph.EdgePath.nil v✝) =
    φ (Graph.SpanningSubtree.surround Γ [[Graph.EdgePath.nil v✝]])
Tactic:
rw [GroupLabelledGraph.pathLabel_nil, Graph.PathClass.nil_eq_id, Γ.surround_nil,
Graph.π₁.one_def, map_one]
Proof state after:
no goals
Theorem: label_path_map
Proof state before:
case cons
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
u v v✝ w✝ u✝ : V
e : Graph.EdgeBetween X v✝ w✝
p : Graph.EdgePath X w✝ u✝
ih : GroupLabelledGraph.pathLabel (inducedLabelling φ) p = φ (Graph.SpanningSubtree.surround Γ [[p]])
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) (Graph.EdgePath.cons e p) =
    φ (Graph.SpanningSubtree.surround Γ [[Graph.EdgePath.cons e p]])
Tactic:
simp only [Γ.surround_cons, GroupLabelledGraph.pathLabel_cons, ih,
Graph.π₁.mul_def, map_mul, mul_right_cancel_iff, induced_label_eq_surround_map]
Proof state after:
no goals
Theorem: hom_induce_induce_eq_self
Proof state before:
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
⊢ GroupLabelledGraph.inducedHom (inducedLabelling φ) = φ
Tactic:
ext x
Proof state after:
case h
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
x : Graph.π₁ X (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) x = φ x
Theorem: hom_induce_induce_eq_self
Proof state before:
case h
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
x : Graph.π₁ X (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) x = φ x
Tactic:
revert x
Proof state after:
case h
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
⊢ ∀ (x : Graph.π₁ X (Graph.SpanningSubtree.base Γ)), (GroupLabelledGraph.inducedHom (inducedLabelling φ)) x = φ x
Theorem: hom_induce_induce_eq_self
Proof state before:
case h
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
⊢ ∀ (x : Graph.π₁ X (Graph.SpanningSubtree.base Γ)), (GroupLabelledGraph.inducedHom (inducedLabelling φ)) x = φ x
Tactic:
apply Graph.PathClass.ind
Proof state after:
case h.a
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
⊢ ∀ (p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)),
    (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]
Theorem: hom_induce_induce_eq_self
Proof state before:
case h.a
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
⊢ ∀ (p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)),
    (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]
Tactic:
intro p
Proof state after:
case h.a
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]
Theorem: hom_induce_induce_eq_self
Proof state before:
case h.a
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]
Tactic:
simp only [GroupLabelledGraph.inducedHom, MonoidHom.coe_mk, OneHom.coe_mk,
  GroupLabelledGraph.pathClassLabel_of_pathLabel, label_path_map, Graph.SpanningSubtree.surround_loop]
Proof state after:
no goals
Theorem: Graph.pathLabel_on_tree_path
Proof state before:
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.113042
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
p : EdgePath X u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) p = 1
Tactic:
induction p with
  | nil _ => simp
  | cons _ _ ih => simp_all [ih]
Proof state after:
no goals
Theorem: Graph.pathLabel_on_tree_path
Proof state before:
case nil
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.113042
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v v✝ : V
hpΓ : Subgraph.contains Γ.toSubgraph (EdgePath.nil v✝)
⊢ GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) (EdgePath.nil v✝) = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Graph.pathLabel_on_tree_path
Proof state before:
case cons
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.113042
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v v✝ w✝ u✝ : V
a✝¹ : EdgeBetween X v✝ w✝
a✝ : EdgePath X w✝ u✝
ih : Subgraph.contains Γ.toSubgraph a✝ → GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) a✝ = 1
hpΓ : Subgraph.contains Γ.toSubgraph (EdgePath.cons a✝¹ a✝)
⊢ GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) (EdgePath.cons a✝¹ a✝) = 1
Tactic:
simp_all [ih]
Proof state after:
no goals
Theorem: Graph.pathClassLabel_on_tree_path
Proof state before:
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ) (u ⤳[Γ] v) = 1
Tactic:
show (Γ.edgeLabelExtension φ).pathClassLabel ([[_]]) = _
Proof state after:
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ)
      [[↑((SpanningSubtree.toSubtree Γ).toPreconnectedSubgraph.path (SpanningSubtree.vertex_coe Γ u)
            (SpanningSubtree.vertex_coe Γ v))]] =
    1
Theorem: Graph.pathClassLabel_on_tree_path
Proof state before:
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ)
      [[↑((SpanningSubtree.toSubtree Γ).toPreconnectedSubgraph.path (SpanningSubtree.vertex_coe Γ u)
            (SpanningSubtree.vertex_coe Γ v))]] =
    1
Tactic:
simp only [GroupLabelledGraph.pathClassLabel_of_pathLabel, SpanningSubtree.contains_path, pathLabel_on_tree_path]
Proof state after:
no goals
Theorem: smallest_mem
Proof state before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
simp [smallest]
Proof state after:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ (if c : tail = [] then head else min head (smallest tail c)) ∈ tail
Theorem: smallest_mem
Proof state before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ (if c : tail = [] then head else min head (smallest tail c)) ∈ tail
Tactic:
split
Proof state after:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail

case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h✝) ∈ tail
Theorem: smallest_mem
Proof state before:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail
Tactic:
rename_i h
Proof state after:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail
Theorem: smallest_mem
Proof state before:
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail
Tactic:
simp [h]
Proof state after:
no goals
Theorem: smallest_mem
Proof state before:
case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h✝) ∈ tail
Tactic:
rename_i h
Proof state after:
case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Theorem: smallest_mem
Proof state before:
case inr
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Tactic:
by_cases h':(head ≤ smallest tail h)
Proof state after:
case pos
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail

case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Theorem: smallest_mem
Proof state before:
case pos
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Tactic:
simp [h']
Proof state after:
no goals
Theorem: smallest_mem
Proof state before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
Tactic:
simp [h', h]
Proof state after:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ min head (smallest tail h) ∈ tail
Theorem: smallest_mem
Proof state before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ min head (smallest tail h) ∈ tail
Tactic:
have lem :
  min head (smallest tail h) = smallest tail h :=   by
    apply min_eq_right
    apply le_of_not_ge
    exact h'
Proof state after:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ min head (smallest tail h) ∈ tail
Theorem: smallest_mem
Proof state before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ min head (smallest tail h) ∈ tail
Tactic:
rw [lem]
Proof state after:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ smallest tail h ∈ tail
Theorem: smallest_mem
Proof state before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ smallest tail h ∈ tail
Tactic:
simp [smallest_mem]
Proof state after:
no goals
Theorem: smallest_mem
Proof state before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ min head (smallest tail h) = smallest tail h
Tactic:
apply min_eq_right
Proof state after:
case h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ smallest tail h ≤ head
Theorem: smallest_mem
Proof state before:
case h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ smallest tail h ≤ head
Tactic:
apply le_of_not_ge
Proof state after:
case h.a
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ ¬smallest tail h ≥ head
Theorem: smallest_mem
Proof state before:
case h.a
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ ¬smallest tail h ≥ head
Tactic:
exact h'
Proof state after:
no goals
Theorem: smallest_le
Proof state before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ ∀ a ∈ head :: tail, smallest (head :: tail) hyp ≤ a
Tactic:
simp [smallest, hyp]
Proof state after:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ head ∧
    ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ head ∧
    ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Tactic:
apply And.intro
Proof state after:
case left
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ head

case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
case left
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ head
Tactic:
split  <;> simp
Proof state after:
no goals
Theorem: smallest_le
Proof state before:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Tactic:
intro a hyp'
Proof state after:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Tactic:
have c''  := List.ne_nil_of_mem hyp'
Proof state after:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else min head (smallest tail c)) ≤ a
Tactic:
simp [c'']
Proof state after:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ head ≤ a ∨ smallest tail (_ : ¬tail = []) ≤ a
Theorem: smallest_le
Proof state before:
case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ head ≤ a ∨ smallest tail (_ : ¬tail = []) ≤ a
Tactic:
right
Proof state after:
case right.h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail (_ : ¬tail = []) ≤ a
Theorem: smallest_le
Proof state before:
case right.h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail (_ : ¬tail = []) ≤ a
Tactic:
exact smallest_le tail c'' a hyp'
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
n : ℕ
⊢ ↑(sumUpto n) = ↑n * (↑n + 1) / 2
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  simp [sumUpto, ih]
  linarith
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
case zero

⊢ ↑(sumUpto Nat.zero) = ↑Nat.zero * (↑Nat.zero + 1) / 2
Tactic:
rfl
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
case succ
n : ℕ
ih : ↑(sumUpto n) = ↑n * (↑n + 1) / 2
⊢ ↑(sumUpto (Nat.succ n)) = ↑(Nat.succ n) * (↑(Nat.succ n) + 1) / 2
Tactic:
simp [sumUpto, ih]
Proof state after:
case succ
n : ℕ
ih : ↑(sumUpto n) = ↑n * (↑n + 1) / 2
⊢ ↑n + 1 + ↑n * (↑n + 1) / 2 = (↑n + 1) * (↑n + 1 + 1) / 2
Theorem: sum_formula
Proof state before:
case succ
n : ℕ
ih : ↑(sumUpto n) = ↑n * (↑n + 1) / 2
⊢ ↑n + 1 + ↑n * (↑n + 1) / 2 = (↑n + 1) * (↑n + 1 + 1) / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: vac_contra
Proof state before:
⊢ ∀ (e : Empty) (n : ℕ), wrong n = e → n = 2
Tactic:
intro e
Proof state after:
e : Empty
⊢ ∀ (n : ℕ), wrong n = e → n = 2
Theorem: vac_contra
Proof state before:
e : Empty
⊢ ∀ (n : ℕ), wrong n = e → n = 2
Tactic:
induction e
Proof state after:
no goals
Theorem: one_eq_two
Proof state before:
⊢ 1 = 2
Tactic:
let e := wrong 1
Proof state after:
e : Empty := wrong 1
⊢ 1 = 2
Theorem: one_eq_two
Proof state before:
e : Empty := wrong 1
⊢ 1 = 2
Tactic:
let h := vac_contra e 1
Proof state after:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ 1 = 2
Theorem: one_eq_two
Proof state before:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ 1 = 2
Tactic:
apply h
Proof state after:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ wrong 1 = e
Theorem: one_eq_two
Proof state before:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ wrong 1 = e
Tactic:
rfl
Proof state after:
no goals