internlm/Lean-Github huggingface dataset:
Theorem: List.getLast_filter
Proof state before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a : α
h : filter p [a] ≠ []
h' : p a = true
⊢ (filter p [a]).getLast h = [a].getLast ⋯
Tactic:
simp [List.filter_cons, h']
Proof state after:
no goals
Theorem: List.getLast_filter
Proof state before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((a :: b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (a :: b :: as).getLast ⋯
Tactic:
rw [List.getLast_cons_cons] at h' ⊢
Proof state after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (b :: as).getLast ⋯
Theorem: List.getLast_filter
Proof state before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (b :: as).getLast ⋯
Tactic:
simp only [List.filter_cons (x := a)] at h ⊢
Proof state after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Theorem: List.getLast_filter
Proof state before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
obtain ha | ha := Bool.eq_false_or_eq_true (p a)
Proof state after:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯

case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = false
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Theorem: List.getLast_filter
Proof state before:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
simp only [ha, ite_true]
Proof state after:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (a :: filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Theorem: List.getLast_filter
Proof state before:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (a :: filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
rw [getLast_cons, getLast_filter (b :: as) _ h']
Proof state after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ filter p (b :: as) ≠ []
Theorem: List.getLast_filter
Proof state before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ filter p (b :: as) ≠ []
Tactic:
exact ne_nil_of_mem $ mem_filter.2 ⟨getLast_mem _, h'⟩
Proof state after:
no goals
Theorem: List.getLast_filter
Proof state before:
case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = false
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
simp only [ha, cond_false] at h ⊢
Proof state after:
case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
ha : p a = false
h : (if False then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if False then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Theorem: List.getLast_filter
Proof state before:
case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
ha : p a = false
h : (if False then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if False then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
exact getLast_filter (b :: as) h h'
Proof state after:
no goals
Theorem: List.cons_sublist_cons_iff'
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ b :: l₂ → a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

case mpr
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ → a :: l₁ <+ b :: l₂
Theorem: List.cons_sublist_cons_iff'
Proof state before:
case mp
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ b :: l₂ → a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂
Tactic:
rintro (_ | _)
Proof state after:
case mp.cons
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
a✝ : a :: l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

case mp.cons₂
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
a✝ : l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = a ∧ l₁ <+ l₂
Theorem: List.cons_sublist_cons_iff'
Proof state before:
case mp.cons
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
a✝ : a :: l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂
Tactic:
exact Or.inl ‹_›
Proof state after:
no goals
Theorem: List.cons_sublist_cons_iff'
Proof state before:
case mp.cons₂
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
a✝ : l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = a ∧ l₁ <+ l₂
Tactic:
exact Or.inr ⟨rfl, ‹_›⟩
Proof state after:
no goals
Theorem: List.cons_sublist_cons_iff'
Proof state before:
case mpr
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ → a :: l₁ <+ b :: l₂
Tactic:
rintro (h | ⟨rfl, h⟩)
Proof state after:
case mpr.inl
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h : a :: l₁ <+ l₂
⊢ a :: l₁ <+ b :: l₂

case mpr.inr.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
h : l₁ <+ l₂
⊢ a :: l₁ <+ a :: l₂
Theorem: List.cons_sublist_cons_iff'
Proof state before:
case mpr.inl
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h : a :: l₁ <+ l₂
⊢ a :: l₁ <+ b :: l₂
Tactic:
exact sublist_cons_of_sublist _ h
Proof state after:
no goals
Theorem: List.cons_sublist_cons_iff'
Proof state before:
case mpr.inr.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
h : l₁ <+ l₂
⊢ a :: l₁ <+ a :: l₂
Tactic:
rwa [cons_sublist_cons]
Proof state after:
no goals
Theorem: List.subperm_nil
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ l = [] → l <+~ []
Tactic:
rintro rfl
Proof state after:
α : Type u_1
l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ [] <+~ []
Theorem: List.subperm_nil
Proof state before:
α : Type u_1
l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ [] <+~ []
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.spanningCoe_induce
Proof state before:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (induce s G).spanningCoe = G.ind s
Tactic:
ext
Proof state after:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
s : Set α
x✝¹ x✝ : α
⊢ (induce s G).spanningCoe.Adj x✝¹ x✝ ↔ (G.ind s).Adj x✝¹ x✝
Theorem: SimpleGraph.spanningCoe_induce
Proof state before:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
s : Set α
x✝¹ x✝ : α
⊢ (induce s G).spanningCoe.Adj x✝¹ x✝ ↔ (G.ind s).Adj x✝¹ x✝
Tactic:
simp [← and_assoc]
Proof state after:
no goals
Theorem: supClosure_prod
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
⊢ supClosure s ×ˢ supClosure t ≤ supClosure (s ×ˢ t)
Tactic:
rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
Proof state after:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)
Theorem: supClosure_prod
Proof state before:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)
Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
Proof state after:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)
Theorem: supClosure_prod
Proof state before:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t
Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt
Proof state after:
no goals
Theorem: supClosure_prod
Proof state before:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)
Tactic:
simp [prodMk_sup'_sup']
Proof state after:
no goals
Theorem: infClosure_prod
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
⊢ infClosure s ×ˢ infClosure t ≤ infClosure (s ×ˢ t)
Tactic:
rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
Proof state after:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.inf' hu id, v.inf' hv id) ∈ infClosure (s ×ˢ t)
Theorem: infClosure_prod
Proof state before:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.inf' hu id, v.inf' hv id) ∈ infClosure (s ×ˢ t)
Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
Proof state after:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)
Theorem: infClosure_prod
Proof state before:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t
Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt
Proof state after:
no goals
Theorem: infClosure_prod
Proof state before:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)
Tactic:
simp [prodMk_inf'_inf']
Proof state after:
no goals
Theorem: latticeClosure_prod
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s✝ s : Set α
t : Set β
⊢ latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t
Tactic:
simp_rw [← supClosure_infClosure]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s✝ s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)
Theorem: latticeClosure_prod
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s✝ s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.degOn_empty
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ a : α
⊢ G.degOn ∅ a = 0
Tactic:
simp [degOn]
Proof state after:
no goals
Theorem: SimpleGraph.degOn_univ
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ a : α
⊢ G.degOn univ a = G.degree a
Tactic:
rw [degOn, degree, univ_inter]
Proof state after:
no goals
Theorem: SimpleGraph.degOn_union
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ G.degOn (s ∪ t) a = G.degOn s a + G.degOn t a
Tactic:
unfold degOn
Proof state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ ((s ∪ t) ∩ G.neighborFinset a).card = (s ∩ G.neighborFinset a).card + (t ∩ G.neighborFinset a).card
Theorem: SimpleGraph.degOn_union
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ ((s ∪ t) ∩ G.neighborFinset a).card = (s ∩ G.neighborFinset a).card + (t ∩ G.neighborFinset a).card
Tactic:
rw [← card_union_of_disjoint, ← union_inter_distrib_right]
Proof state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ Disjoint (s ∩ G.neighborFinset a) (t ∩ G.neighborFinset a)
Theorem: SimpleGraph.degOn_union
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ Disjoint (s ∩ G.neighborFinset a) (t ∩ G.neighborFinset a)
Tactic:
exact h.mono inter_subset_left inter_subset_left
Proof state after:
no goals
Theorem: SimpleGraph.sum_degOn_comm
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ a ∈ s, G.degOn t a = ∑ a ∈ t, G.degOn s a
Tactic:
simp_rw [degOn, card_eq_sum_ones, ← sum_indicator_eq_sum_inter]
Proof state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ x ∈ s, ∑ i ∈ t, (↑(G.neighborFinset x)).indicator (fun x => 1) i =
    ∑ x ∈ t, ∑ i ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) i
Theorem: SimpleGraph.sum_degOn_comm
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ x ∈ s, ∑ i ∈ t, (↑(G.neighborFinset x)).indicator (fun x => 1) i =
    ∑ x ∈ t, ∑ i ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) i
Tactic:
rw [sum_comm]
Proof state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ y ∈ t, ∑ x ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) y =
    ∑ x ∈ t, ∑ i ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) i
Theorem: SimpleGraph.sum_degOn_comm
Proof state before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ y ∈ t, ∑ x ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) y =
    ∑ x ∈ t, ∑ i ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) i
Tactic:
simp [Set.indicator_apply, adj_comm]
Proof state after:
no goals
Theorem: Nat.eq_of_dvd_of_lt_two_mul
Proof state before:
a b : ℕ
ha : a ≠ 0
hdvd : b ∣ a
hlt : a < 2 * b
⊢ a = b
Tactic:
obtain ⟨_ | _ | c, rfl⟩ := hdvd
Proof state after:
case intro.zero
b : ℕ
ha : b * 0 ≠ 0
hlt : b * 0 < 2 * b
⊢ b * 0 = b

case intro.succ.zero
b : ℕ
ha : b * (0 + 1) ≠ 0
hlt : b * (0 + 1) < 2 * b
⊢ b * (0 + 1) = b

case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b
Theorem: Nat.eq_of_dvd_of_lt_two_mul
Proof state before:
case intro.zero
b : ℕ
ha : b * 0 ≠ 0
hlt : b * 0 < 2 * b
⊢ b * 0 = b
Tactic:
simp at ha
Proof state after:
no goals
Theorem: Nat.eq_of_dvd_of_lt_two_mul
Proof state before:
case intro.succ.zero
b : ℕ
ha : b * (0 + 1) ≠ 0
hlt : b * (0 + 1) < 2 * b
⊢ b * (0 + 1) = b
Tactic:
exact Nat.mul_one _
Proof state after:
no goals
Theorem: Nat.eq_of_dvd_of_lt_two_mul
Proof state before:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b
Tactic:
rw [Nat.mul_comm] at hlt
Proof state after:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ b * (c + 1 + 1) = b
Theorem: Nat.eq_of_dvd_of_lt_two_mul
Proof state before:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ b * (c + 1 + 1) = b
Tactic:
cases Nat.not_le_of_lt hlt (Nat.mul_le_mul_right _ (by omega))
Proof state after:
no goals
Theorem: Nat.eq_of_dvd_of_lt_two_mul
Proof state before:
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ 2 ≤ c + 1 + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
hf : ∀ i ∈ s, r ≤ ‖f i‖
⊢ ∃ P,
    P.parts.card = s.card.choose (s.card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
induction' s using Finset.induction with i s hi ih
Proof state after:
case empty
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
hf : ∀ i ∈ ∅, r ≤ ‖f i‖
⊢ ∃ P,
    P.parts.card = ∅.card.choose (∅.card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ ∅) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)

case insert
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, r ≤ ‖f i‖) →
    ∃ P,
      P.parts.card = s.card.choose (s.card / 2) ∧
        (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
case insert
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, r ≤ ‖f i‖) →
    ∃ P,
      P.parts.card = s.card.choose (s.card / 2) ∧
        (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
obtain ⟨P, hP, hs, hPr⟩ := ih fun j hj ↦ hf _ $ mem_insert_of_mem hj
Proof state after:
case insert.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, r ≤ ‖f i‖) →
    ∃ P,
      P.parts.card = s.card.choose (s.card / 2) ∧
        (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)