internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.push_append
Proof state before:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.copy (Walk.append (push_Walk f p) (push_Walk f q)) (_ : f v = f u) (_ : f c = f c) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)
Tactic:
rw [← Walk.append_copy_copy]
Proof state after:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) ?pos.hv✝)
      (Walk.copy (push_Walk f q) ?pos.hv✝ (_ : f c = f c)) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)

case pos.hv
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ f w = ?m.63832

V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ V'
Theorem: SimpleGraph.push_append
Proof state before:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) ?pos.hv✝)
      (Walk.copy (push_Walk f q) ?pos.hv✝ (_ : f c = f c)) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)

case pos.hv
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ f w = ?m.63832

V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ V'
Tactic:
congr
Proof state after:
no goals
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
hp : ∀ z ∈ Walk.support p, f z = w
⊢ Walk.copy (push_Walk f p) (_ : f a = w) (_ : f b = w) = Walk.nil
Tactic:
induction p with
| nil => simp at hp ; subst hp ; rfl
| cons h p ih =>
  simp at hp ; obtain ⟨h1, hp⟩ := hp
  subst_vars
  simpa [push_Walk, hp _ (Walk.start_mem_support _)] using ih hp
Proof state after:
no goals
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
u✝ : V
hp : ∀ z ∈ Walk.support Walk.nil, f z = w
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = w) (_ : f u✝ = w) = Walk.nil
Tactic:
simp at hp
Proof state after:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
u✝ : V
hp✝ : ∀ z ∈ Walk.support Walk.nil, f z = w
hp : f u✝ = w
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = w) (_ : f u✝ = w) = Walk.nil
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
u✝ : V
hp✝ : ∀ z ∈ Walk.support Walk.nil, f z = w
hp : f u✝ = w
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = w) (_ : f u✝ = w) = Walk.nil
Tactic:
subst hp
Proof state after:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
hp : ∀ z ∈ Walk.support Walk.nil, f z = f u✝
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = f u✝) (_ : f u✝ = f u✝) = Walk.nil
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
hp : ∀ z ∈ Walk.support Walk.nil, f z = f u✝
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = f u✝) (_ : f u✝ = f u✝) = Walk.nil
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Tactic:
simp at hp
Proof state after:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
hp : f u✝ = w ∧ ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
hp : f u✝ = w ∧ ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Tactic:
obtain ⟨h1, hp⟩ := hp
Proof state after:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
h1 : f u✝ = w
hp : ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
h1 : f u✝ = w
hp : ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Tactic:
subst_vars
Proof state after:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = f u✝), Walk.copy (push_Walk f p) (_ : f v✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = f u✝
hp : ∀ a ∈ Walk.support p, f a = f u✝
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil
Theorem: SimpleGraph.push_eq_nil'
Proof state before:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = f u✝), Walk.copy (push_Walk f p) (_ : f v✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = f u✝
hp : ∀ a ∈ Walk.support p, f a = f u✝
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil
Tactic:
simpa [push_Walk, hp _ (Walk.start_mem_support _)] using ih hp
Proof state after:
no goals
Theorem: SimpleGraph.tata
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
q : Walk G c d
h1 : a = c
h2 : b = d
⊢ Walk.copy p h1 h2 = q ↔ p = Walk.copy q (_ : c = a) (_ : d = b)
Tactic:
constructor <;> rintro rfl <;> simp
Proof state after:
no goals
Theorem: SimpleGraph.push_eq_nil
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f✝ : V → V'
p✝ : Walk G a b
x y : V
f : V → V'
w : V'
p : Walk G x y
hp : ∀ z ∈ Walk.support p, f z = w
⊢ Walk.Nil (push_Walk f p)
Tactic:
simp [tata.mp <| push_eq_nil' hp]
Proof state after:
no goals
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
by_cases h1 : P a
Proof state after:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v

case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
left
Proof state after:
case pos.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case pos.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a
Tactic:
assumption
Proof state after:
no goals
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
right
Proof state after:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
simp [h1]
Proof state after:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ∃ v ∈ Walk.tail₀ p, P v
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
by_cases h2 : p.Nil
Proof state after:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v

case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : ¬Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
cases h2
Proof state after:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Tactic:
simp at h
Proof state after:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : P a
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : P a
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Tactic:
contradiction
Proof state after:
no goals
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : ¬Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
cases p
Proof state after:
case neg.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
h2 : ¬Walk.Nil Walk.nil
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v

case neg.cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
v✝ : V
h✝ : Adj G a v✝
p✝ : Walk G v✝ b
h : ∃ v ∈ Walk.support (Walk.cons h✝ p✝), P v
h2 : ¬Walk.Nil (Walk.cons h✝ p✝)
⊢ ∃ v ∈ Walk.tail₀ (Walk.cons h✝ p✝), P v
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case neg.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
h2 : ¬Walk.Nil Walk.nil
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Tactic:
cases h2 Walk.nil_nil
Proof state after:
no goals
Theorem: SimpleGraph.head_or_exists_tail₀
Proof state before:
case neg.cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
v✝ : V
h✝ : Adj G a v✝
p✝ : Walk G v✝ b
h : ∃ v ∈ Walk.support (Walk.cons h✝ p✝), P v
h2 : ¬Walk.Nil (Walk.cons h✝ p✝)
⊢ ∃ v ∈ Walk.tail₀ (Walk.cons h✝ p✝), P v
Tactic:
simpa [h1] using h
Proof state after:
no goals
Theorem: SimpleGraph.Walk.transportable_to_of_le
Proof state before:
V✝ : Type u_1
V' : Type u_2
a✝ b✝ c d : V✝
G✝ G'✝ : SimpleGraph V✝
f : V✝ → V'
p✝ : Walk G✝ a✝ b✝
V : Type u_3
G G' : SimpleGraph V
a b : V
p : Walk G a b
G_le : G ≤ G'
⊢ transportable_to G' p
Tactic:
induction p with
| nil => simp [transportable_to]
| cons h p ih => simpa [transportable_to, G_le h] using ih
Proof state after:
no goals
Theorem: SimpleGraph.Walk.transportable_to_of_le
Proof state before:
case nil
V✝ : Type u_1
V' : Type u_2
a✝ b✝ c d : V✝
G✝ G'✝ : SimpleGraph V✝
f : V✝ → V'
p✝ : Walk G✝ a✝ b✝
V : Type u_3
G G' : SimpleGraph V
a b : V
p : Walk G a b
G_le : G ≤ G'
u✝ : V
⊢ transportable_to G' nil
Tactic:
simp [transportable_to]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.transportable_to_of_le
Proof state before:
case cons
V✝ : Type u_1
V' : Type u_2
a✝ b✝ c d : V✝
G✝ G'✝ : SimpleGraph V✝
f : V✝ → V'
p✝¹ : Walk G✝ a✝ b✝
V : Type u_3
G G' : SimpleGraph V
a b : V
p✝ : Walk G a b
G_le : G ≤ G'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : transportable_to G' p
⊢ transportable_to G' (cons h p)
Tactic:
simpa [transportable_to, G_le h] using ih
Proof state after:
no goals
Theorem: Finset.singleton_inter_nonempty
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ ({a} ∩ X).Nonempty → a ∈ X
Tactic:
simp [nonempty_iff_ne_empty]
Proof state after:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ ¬{a} ∩ X = ∅ → a ∈ X
Theorem: Finset.singleton_inter_nonempty
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ ¬{a} ∩ X = ∅ → a ∈ X
Tactic:
contrapose!
Proof state after:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ a ∉ X → {a} ∩ X = ∅
Theorem: Finset.singleton_inter_nonempty
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ a ∉ X → {a} ∩ X = ∅
Tactic:
exact singleton_inter_of_not_mem
Proof state after:
no goals
Theorem: Finset.singleton_inter_nonempty
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
h : a ∈ X
⊢ ({a} ∩ X).Nonempty
Tactic:
use a
Proof state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
h : a ∈ X
⊢ a ∈ {a} ∩ X
Theorem: Finset.singleton_inter_nonempty
Proof state before:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
h : a ∈ X
⊢ a ∈ {a} ∩ X
Tactic:
simp [h]
Proof state after:
no goals
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
⊢ Adapted G (merge_edge e)
Tactic:
rintro x y hxy
Proof state after:
V : Type u_1
V' : Type u_2
V'' : Type u_3
x✝ y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
x y : V
hxy : merge_edge e x = merge_edge e y
⊢ ∃ p, ∀ z ∈ Walk.support p, merge_edge e z = merge_edge e y
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
V : Type u_1
V' : Type u_2
V'' : Type u_3
x✝ y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
x y : V
hxy : merge_edge e x = merge_edge e y
⊢ ∃ p, ∀ z ∈ Walk.support p, merge_edge e z = merge_edge e y
Tactic:
by_cases hx : x = e.snd <;> by_cases hy : y = e.snd <;>
  simp [merge_edge, Function.update, hx, hy] at hxy ⊢ <;> subst_vars
Proof state after:
case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1

case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1

case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1

case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = y
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
use Walk.nil
Proof state after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∀ z ∈ Walk.support Walk.nil, ¬z = e.toProd.2 → z = e.toProd.1
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∀ z ∈ Walk.support Walk.nil, ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1
Tactic:
use Walk.nil.cons e.symm.is_adj
Proof state after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G (Dart.symm e).toProd.1 (Dart.symm e).toProd.2) Walk.nil),
    (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G (Dart.symm e).toProd.1 (Dart.symm e).toProd.2) Walk.nil),
    (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
use Walk.nil.cons e.is_adj
Proof state after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G e.toProd.1 e.toProd.2) Walk.nil), ¬z = e.toProd.2 → z = e.toProd.1
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G e.toProd.1 e.toProd.2) Walk.nil), ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = y
Tactic:
use Walk.nil
Proof state after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∀ z ∈ Walk.support Walk.nil, (if z = e.toProd.2 then e.toProd.1 else z) = y
Theorem: SimpleGraph.merge_edge_adapted
Proof state before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∀ z ∈ Walk.support Walk.nil, (if z = e.toProd.2 then e.toProd.1 else z) = y
Tactic:
simp [hy]
Proof state after:
no goals
Theorem: Vec.drop_append1'
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
a : α
⊢ drop (append1 v a) = v
Tactic:
funext x
Proof state after:
case h
α : Type u_1
n : ℕ
v : Vec α n
a : α
x : Fin2 n
⊢ drop (append1 v a) x = v x
Theorem: Vec.drop_append1'
Proof state before:
case h
α : Type u_1
n : ℕ
v : Vec α n
a : α
x : Fin2 n
⊢ drop (append1 v a) x = v x
Tactic:
rfl
Proof state after:
no goals