internlm/Lean-Github huggingface dataset:
Theorem: Notes.totally_ordered_of_sorted
Proof state before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ r (a₂ :: as)[k] (a₂ :: as)[l]
Tactic:
apply totally_ordered_of_sorted h₂
Proof state after:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ k < l
Theorem: Notes.totally_ordered_of_sorted
Proof state before:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ k < l
Tactic:
apply Nat.pred_lt_pred (by simp) h'
Proof state after:
no goals
Theorem: Notes.totally_ordered_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
⊢ Nat.succ k ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Notes.totally_ordered_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ Nat.succ k ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ n
⊢ m ≤ plus n 1
Tactic:
match n with 
| 0 => 
  have meq0 : m = 0 := Nat.eq_zero_of_le_zero h
  rw [meq0]
  simp
| n'+1 => 
  simp [plus]
  calc 
    m ≤ n'+1 := by exact h 
    _ ≤ (n'+1)+1 := by exact Nat.le_succ _
Proof state after:
no goals
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
⊢ m ≤ plus 0 1
Tactic:
have meq0 : m = 0 := Nat.eq_zero_of_le_zero h
Proof state after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
meq0 : m = 0
⊢ m ≤ plus 0 1
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
meq0 : m = 0
⊢ m ≤ plus 0 1
Tactic:
rw [meq0]
Proof state after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
meq0 : m = 0
⊢ 0 ≤ plus 0 1
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
meq0 : m = 0
⊢ 0 ≤ plus 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ m ≤ plus (n' + 1) 1
Tactic:
simp [plus]
Proof state after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ m ≤ Nat.succ (n' + 1)
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ m ≤ Nat.succ (n' + 1)
Tactic:
calc 
  m ≤ n'+1 := by exact h 
  _ ≤ (n'+1)+1 := by exact Nat.le_succ _
Proof state after:
no goals
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ m ≤ n' + 1
Tactic:
exact h
Proof state after:
no goals
Theorem: leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ n' + 1 ≤ n' + 1 + 1
Tactic:
exact Nat.le_succ _
Proof state after:
no goals
Theorem: succ_leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ plus m a ≤ plus n a
Tactic:
match a with 
| 0 => simp [plus]; assumption 
| b+1 => 
  simp [plus] 
  apply Nat.succ_le_succ
  exact succ_leq_succ_of_leq m n b h
Proof state after:
no goals
Theorem: succ_leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ plus m 0 ≤ plus n 0
Tactic:
simp [plus]
Proof state after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ m ≤ n
Theorem: succ_leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ m ≤ n
Tactic:
assumption
Proof state after:
no goals
Theorem: succ_leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ plus m (b + 1) ≤ plus n (b + 1)
Tactic:
simp [plus]
Proof state after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ Nat.succ (plus m b) ≤ Nat.succ (plus n b)
Theorem: succ_leq_succ_of_leq
Proof state before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ Nat.succ (plus m b) ≤ Nat.succ (plus n b)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ plus m b ≤ plus n b
Theorem: succ_leq_succ_of_leq
Proof state before:
case a
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ plus m b ≤ plus n b
Tactic:
exact succ_leq_succ_of_leq m n b h
Proof state after:
no goals
Theorem: exp_eq_exp'
Proof state before:
b e : ℕ
⊢ exp b e = exp' b e
Tactic:
match e with 
| 0 => simp [exp,exp'] 
| n+1 => 
  simp only [exp,exp']
  simp only [Nat.add]
  rw [exp_eq_exp' b n]
Proof state after:
no goals
Theorem: exp_eq_exp'
Proof state before:
b e : ℕ
⊢ exp b 0 = exp' b 0
Tactic:
simp [exp,exp']
Proof state after:
no goals
Theorem: exp_eq_exp'
Proof state before:
b e n : ℕ
⊢ exp b (n + 1) = exp' b (n + 1)
Tactic:
simp only [exp,exp']
Proof state after:
b e n : ℕ
⊢ exp b (Nat.add n 0) * b = exp' b (Nat.add n 0) * b
Theorem: exp_eq_exp'
Proof state before:
b e n : ℕ
⊢ exp b (Nat.add n 0) * b = exp' b (Nat.add n 0) * b
Tactic:
simp only [Nat.add]
Proof state after:
b e n : ℕ
⊢ exp b n * b = exp' b n * b
Theorem: exp_eq_exp'
Proof state before:
b e n : ℕ
⊢ exp b n * b = exp' b n * b
Tactic:
rw [exp_eq_exp' b n]
Proof state after:
no goals
Theorem: Notes.sorted_tail_of_sorted
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
as : List α
h : Sorted f (a :: as)
⊢ Sorted f as
Tactic:
match h with 
| single => apply nil  
| longer _ h'' => exact h''
Proof state after:
no goals
Theorem: Notes.sorted_tail_of_sorted
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
as : List α
h : Sorted f (a :: as)
⊢ Sorted f []
Tactic:
apply nil
Proof state after:
no goals
Theorem: Notes.sorted_tail_of_sorted
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
as : List α
h : Sorted f (a :: as)
a₂✝ : α
as✝ : List α
h✝ : f a a₂✝ = true
h'' : Sorted f (a₂✝ :: as✝)
⊢ Sorted f (a₂✝ :: as✝)
Tactic:
exact h''
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
⊢ List.length (insert f a l) = List.length l + 1
Tactic:
match l with 
| [] => simp [insert]
| a'::as =>
  match h : f a a' with 
  | true => simp [insert, h]
  | false => simp [insert, h]; apply len_insert_eq_succ_len
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
⊢ List.length (insert f a []) = List.length [] + 1
Tactic:
simp [insert]
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
⊢ List.length (insert f a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
match h : f a a' with 
| true => simp [insert, h]
| false => simp [insert, h]; apply len_insert_eq_succ_len
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = true
⊢ List.length (insert f a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
simp [insert, h]
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = false
⊢ List.length (insert f a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
simp [insert, h]
Proof state after:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = false
⊢ List.length (insert f a as) = List.length as + 1
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = false
⊢ List.length (insert f a as) = List.length as + 1
Tactic:
apply len_insert_eq_succ_len
Proof state after:
no goals
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
h : Sorted f [a']
⊢ f a' (insert f a [])[0] = true
Tactic:
simpa [insert]
Proof state after:
no goals
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = true
⊢ f a' (insert f a (a'' :: as'))[0] = true
Tactic:
simpa [insert, h'']
Proof state after:
no goals
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = false
⊢ f a' (insert f a (a'' :: as'))[0] = true
Tactic:
simp [insert, h'']
Proof state after:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = false
⊢ f a' a'' = true
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = false
⊢ f a' a'' = true
Tactic:
apply ordered_of_sorted f h
Proof state after:
no goals
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = true
⊢ Sorted f (insert f a (a' :: as))
Tactic:
simp [insert, h']
Proof state after:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = true
⊢ Sorted f (a :: a' :: as)
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = true
⊢ Sorted f (a :: a' :: as)
Tactic:
apply longer h' h
Proof state after:
no goals
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (insert f a (a' :: as))
Tactic:
simp [insert, h']
Proof state after:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (a' :: insert f a as)
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (a' :: insert f a as)
Tactic:
apply cons f
Proof state after:
case h₁
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (insert f a as)

case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' (insert f a as)[0] = true

case h₂
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ List.length (insert f a as) > 0
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₁
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (insert f a as)
Tactic:
apply insert_sorted_of_sorted <| sorted_tail_of_sorted f a' as h
Proof state after:
no goals
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' (insert f a as)[0] = true
Tactic:
apply ordered_cons_insert_of_unordered f h
Proof state after:
case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' a = true
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' a = true
Tactic:
apply asym
Proof state after:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ (!f a a') = true
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ (!f a a') = true
Tactic:
simp
Proof state after:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a a' = false
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a a' = false
Tactic:
assumption
Proof state after:
no goals
Theorem: Notes.sorted_of_insertSort
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
l : List α
inst✝ : Asymmetric f
a : α
as : List α
⊢ Sorted f (insertSort f (a :: as))
Tactic:
dsimp [insertSort]
Proof state after:
α : Type
f : α → α → Bool
r : α → α → Prop
l : List α
inst✝ : Asymmetric f
a : α
as : List α
⊢ Sorted f (insert f a (insertSort f as))
Theorem: Notes.sorted_of_insertSort
Proof state before:
α : Type
f : α → α → Bool
r : α → α → Prop
l : List α
inst✝ : Asymmetric f
a : α
as : List α
⊢ Sorted f (insert f a (insertSort f as))
Tactic:
apply insert_sorted_of_sorted f <| sorted_of_insertSort as
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction
Proof state before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
⊢ motive G
Tactic:
have : Fintype V := Fintype.ofFinite V
Proof state after:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
this : Fintype V
⊢ motive G
Theorem: Digraph.deleteEdges_induction
Proof state before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
this : Fintype V
⊢ motive G
Tactic:
generalize hs : G.edgeSet.toFinset = s
Proof state after:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
this : Fintype V
s : Finset (V × V)
hs : Set.toFinset (edgeSet G) = s
⊢ motive G
Theorem: Digraph.deleteEdges_induction
Proof state before:
case empty
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
G : Digraph V
hs : Set.toFinset (edgeSet G) = ∅
⊢ motive G
Tactic:
rw [← Set.toFinset_empty, Set.toFinset_inj, ← edgeSet_bot, edgeSet_inj] at hs
Proof state after:
case empty
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
G : Digraph V
hs✝ : Set.toFinset (edgeSet G) = ∅
hs : G = ⊥
⊢ motive G
Theorem: Digraph.deleteEdges_induction
Proof state before:
case empty
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
G : Digraph V
hs✝ : Set.toFinset (edgeSet G) = ∅
hs : G = ⊥
⊢ motive G
Tactic:
rwa [hs]
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction
Proof state before:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
⊢ motive G
Tactic:
have : e ∈ G.edgeSet
Proof state after:
case this
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
⊢ e ∈ edgeSet G

case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive G
Theorem: Digraph.deleteEdges_induction
Proof state before:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive G
Tactic:
apply hdelete G e.1 e.2 this
Proof state after:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive (deleteEdges G {(e.fst, e.snd)})
Theorem: Digraph.deleteEdges_induction
Proof state before:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive (deleteEdges G {(e.fst, e.snd)})
Tactic:
apply ih
Proof state after:
case insert.hs
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) = s
Theorem: Digraph.deleteEdges_induction
Proof state before:
case insert.hs
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) = s
Tactic:
ext ⟨v, w⟩
Proof state after:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
v w : V
⊢ (v, w) ∈ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) ↔ (v, w) ∈ s
Theorem: Digraph.deleteEdges_induction
Proof state before:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
v w : V
⊢ (v, w) ∈ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) ↔ (v, w) ∈ s
Tactic:
simp only [Prod.mk.eta, Set.mem_toFinset, mem_edgeSet, deleteEdges_adj, Set.mem_singleton_iff]
Proof state after:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
v w : V
⊢ G.Adj v w ∧ ¬(v, w) = e ↔ (v, w) ∈ s