internlm/Lean-Github huggingface dataset:
Theorem: List.Sublist.exists_intermediate
Proof state before:
case cons.succ.cons
α : Type u_1
l l' l₁ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
h₂ : n✝ + 1 ≤ (b :: l₂).length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ b :: l₂ ∧ l₁.length = n✝ + 1
Tactic:
obtain ⟨l₁, h₀₁, h₁₂, rfl⟩ := ih sorry (Nat.succ_le_succ_iff.1 h₀) (Nat.le_of_succ_le h₂)
Proof state after:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1
Theorem: List.Sublist.exists_intermediate
Proof state before:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1
Tactic:
rw [cons_sublist_cons_iff'] at hl
Proof state after:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ l₂ ∨ a = b ∧ l₀ <+ l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1
Theorem: List.Sublist.exists_intermediate
Proof state before:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ l₂ ∨ a = b ∧ l₀ <+ l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1
Tactic:
obtain hl | ⟨rfl, hl⟩ := hl
Proof state after:
case cons.succ.cons.intro.intro.intro.inl
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
hl : a :: l₀ <+ l₂
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1

case cons.succ.cons.intro.intro.intro.inr.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ l₁ : List α
h₀₁ : l₀ <+ l₁
h₀ : (a :: l₀).length ≤ l₁.length + 1
hl : l₀ <+ l₂
h₁₂ : l₁ <+ a :: l₂
h₂ : l₁.length + 1 ≤ (a :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ a :: l₂ ∧ l₁_1.length = l₁.length + 1
Theorem: List.Sublist.exists_intermediate
Proof state before:
case nil
α : Type u_1
l l' l₁ : List α
a b : α
m : ℕ
l₂ : List α
n : ℕ
hl : [] <+ l₂
h₀ : [].length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, [] <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
Tactic:
exact (exists_sublist_length_eq h₂).imp (fun l₁ h ↦ ⟨nil_sublist _, h⟩)
Proof state after:
no goals
Theorem: List.Sublist.exists_intermediate
Proof state before:
case cons.zero
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ 0
h₂ : 0 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = 0
Tactic:
cases h₀
Proof state after:
no goals
Theorem: List.Sublist.exists_intermediate
Proof state before:
case cons.succ.nil
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
hl : a :: l₀ <+ []
h₂ : n✝ + 1 ≤ [].length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ [] ∧ l₁.length = n✝ + 1
Tactic:
cases h₂
Proof state after:
no goals
Theorem: List.Subperm.exists_intermediate
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l₀ <+~ l₂
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Tactic:
obtain ⟨l₀', hl₀, hl'⟩ := hl
Proof state after:
case intro.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Theorem: List.Subperm.exists_intermediate
Proof state before:
case intro.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Tactic:
obtain ⟨l₁, h₀₁, h₁₂, hn⟩ := hl'.exists_intermediate (hl₀.length_eq.trans_le h₀) h₂
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
l l' l₀ l₁✝ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
l₁ : List α
h₀₁ : l₀' <+ l₁
h₁₂ : l₁ <+ l₂
hn : l₁.length = n
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Theorem: List.Subperm.exists_intermediate
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
l l' l₀ l₁✝ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
l₁ : List α
h₀₁ : l₀' <+ l₁
h₁₂ : l₁ <+ l₂
hn : l₁.length = n
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Tactic:
exact ⟨l₁, ⟨_, hl₀, h₀₁⟩, h₁₂.subperm, hn⟩
Proof state after:
no goals
Theorem: List.exists_subperm_length_eq
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hn : n ≤ l.length
⊢ ∃ l', l' <+~ l ∧ l'.length = n
Tactic:
simpa using nil_subperm.exists_intermediate (Nat.zero_le _) hn
Proof state after:
no goals
Theorem: Finset.mem_certificator
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ a ∈ s □ t ↔ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t
Tactic:
rw [certificator, mem_filter, and_iff_right_of_imp]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ (∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t) → a ∈ s ∩ t
Theorem: Finset.mem_certificator
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ (∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t) → a ∈ s ∩ t
Tactic:
rintro ⟨u, v, _, hu, hv⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a u v : α
left✝ : IsCompl u v
hu : ∀ ⦃b : α⦄, a ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, a ⊓ v = b ⊓ v → b ∈ t
⊢ a ∈ s ∩ t
Theorem: Finset.mem_certificator
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a u v : α
left✝ : IsCompl u v
hu : ∀ ⦃b : α⦄, a ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, a ⊓ v = b ⊓ v → b ∈ t
⊢ a ∈ s ∩ t
Tactic:
exact mem_inter.2 ⟨hu rfl, hv rfl⟩
Proof state after:
no goals
Theorem: Finset.certificator_subset_disjSups
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ s □ t ⊆ s ○ t
Tactic:
simp_rw [subset_iff, mem_certificator, mem_disjSups]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ ∀ ⦃x : α⦄,
    (∃ x_1 y, IsCompl x_1 y ∧ (∀ ⦃b : α⦄, x ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, x ⊓ y = b ⊓ y → b ∈ t) →
      ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x
Theorem: Finset.certificator_subset_disjSups
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ ∀ ⦃x : α⦄,
    (∃ x_1 y, IsCompl x_1 y ∧ (∀ ⦃b : α⦄, x ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, x ⊓ y = b ⊓ y → b ∈ t) →
      ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x
Tactic:
rintro x ⟨u, v, huv, hu, hv⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x
Theorem: Finset.certificator_subset_disjSups
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x
Tactic:
refine' ⟨x ⊓ u, hu (inf_right_idem _ _).symm, x ⊓ v, hv (inf_right_idem _ _).symm,
  huv.disjoint.mono inf_le_right inf_le_right, _⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ x ⊓ u ⊔ x ⊓ v = x
Theorem: Finset.certificator_subset_disjSups
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ x ⊓ u ⊔ x ⊓ v = x
Tactic:
rw [← inf_sup_left, huv.codisjoint.eq_top, inf_top_eq]
Proof state after:
no goals
Theorem: Finset.certificator_comm
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ s □ t = t □ s
Tactic:
ext s
Proof state after:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ s ∈ s✝ □ t ↔ s ∈ t □ s✝
Theorem: Finset.certificator_comm
Proof state before:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ s ∈ s✝ □ t ↔ s ∈ t □ s✝
Tactic:
rw [mem_certificator, exists_comm]
Proof state after:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ (∃ b a, IsCompl a b ∧ (∀ ⦃b : α⦄, s ⊓ a = b ⊓ a → b ∈ s✝) ∧ ∀ ⦃b_1 : α⦄, s ⊓ b = b_1 ⊓ b → b_1 ∈ t) ↔ s ∈ t □ s✝
Theorem: Finset.certificator_comm
Proof state before:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ (∃ b a, IsCompl a b ∧ (∀ ⦃b : α⦄, s ⊓ a = b ⊓ a → b ∈ s✝) ∧ ∀ ⦃b_1 : α⦄, s ⊓ b = b_1 ⊓ b → b_1 ∈ t) ↔ s ∈ t □ s✝
Tactic:
simp [isCompl_comm, and_comm]
Proof state after:
no goals
Theorem: Finset.IsUpperSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsLowerSet ↑t
⊢ s □ t = s ∩ t
Tactic:
refine'
  certificator_subset_inter.antisymm fun a ha ↦ mem_certificator.2 ⟨a, aᶜ, isCompl_compl, _⟩
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsLowerSet ↑t
a : α
ha : a ∈ s ∩ t
⊢ (∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ t
Theorem: Finset.IsUpperSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsLowerSet ↑t
a : α
ha : a ∈ s ∩ t
⊢ (∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ t
Tactic:
rw [mem_inter] at ha
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsLowerSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ t
Theorem: Finset.IsUpperSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsLowerSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ t
Tactic:
simp only [@eq_comm _ ⊥, ← sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsLowerSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ≤ b → b ∈ s) ∧ ∀ ⦃b : α⦄, b ≤ a → b ∈ t
Theorem: Finset.IsUpperSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsLowerSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ≤ b → b ∈ s) ∧ ∀ ⦃b : α⦄, b ≤ a → b ∈ t
Tactic:
exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
Proof state after:
no goals
Theorem: Finset.IsLowerSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
⊢ s □ t = s ∩ t
Tactic:
refine' certificator_subset_inter.antisymm fun a ha ↦
  mem_certificator.2 ⟨aᶜ, a, isCompl_compl.symm, _⟩
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∩ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t
Theorem: Finset.IsLowerSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∩ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t
Tactic:
rw [mem_inter] at ha
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t
Theorem: Finset.IsLowerSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t
Tactic:
simp only [@eq_comm _ ⊥, ← sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, b ≤ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ≤ b → b ∈ t
Theorem: Finset.IsLowerSet.certificator_eq_inter
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, b ≤ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ≤ b → b ∈ t
Tactic:
exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
Proof state after:
no goals
Theorem: Finset.IsUpperSet.certificator_eq_disjSups
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
⊢ s □ t = s ○ t
Tactic:
refine' certificator_subset_disjSups.antisymm fun a ha ↦ mem_certificator.2 _
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ○ t
⊢ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t
Theorem: Finset.IsUpperSet.certificator_eq_disjSups
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ○ t
⊢ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t
Tactic:
obtain ⟨x, hx, y, hy, hxy, rfl⟩ := mem_disjSups.1 ha
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ ∃ x_1 y_1, IsCompl x_1 y_1 ∧ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ y_1 = b ⊓ y_1 → b ∈ t
Theorem: Finset.IsUpperSet.certificator_eq_disjSups
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ ∃ x_1 y_1, IsCompl x_1 y_1 ∧ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ y_1 = b ⊓ y_1 → b ∈ t
Tactic:
refine' ⟨x, xᶜ, isCompl_compl, _⟩
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ xᶜ = b ⊓ xᶜ → b ∈ t
Theorem: Finset.IsUpperSet.certificator_eq_disjSups
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ xᶜ = b ⊓ xᶜ → b ∈ t
Tactic:
simp only [inf_of_le_right, le_sup_left, right_eq_inf, ← sdiff_eq, hxy.sup_sdiff_cancel_left]
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, x ≤ b → b ∈ s) ∧ ∀ ⦃b : α⦄, y = b \ x → b ∈ t
Theorem: Finset.IsUpperSet.certificator_eq_disjSups
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, x ≤ b → b ∈ s) ∧ ∀ ⦃b : α⦄, y = b \ x → b ∈ t
Tactic:
exact ⟨fun b hab ↦ hs hab hx, fun b hab ↦ ht (hab.trans_le sdiff_le) hy⟩
Proof state after:
no goals
Theorem: SBtw.sbtw.symm
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
huv : u ≠ v
huw : u ≠ w
hvw : v ≠ w
d : Dist.dist u v + Dist.dist v w = Dist.dist u w
⊢ Dist.dist w v + Dist.dist v u = Dist.dist w u
Tactic:
simpa [dist_comm, add_comm] using d
Proof state after:
no goals
Theorem: sbtw_iff_of_ne
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
h12 : u ≠ v
h13 : u ≠ w
h23 : v ≠ w
⊢ sbtw u v w ↔ dist u v + dist v w = dist u w
Tactic:
simp [MetricSpace.sbtw_iff, h12, h13, h23]
Proof state after:
no goals
Theorem: sbtw_mk
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
h12 : u ≠ v
h23 : v ≠ w
h : dist u v + dist v w ≤ dist u w
⊢ sbtw u v w
Tactic:
refine ⟨h12, ?_, h23, h.antisymm (dist_triangle _ _ _)⟩
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
h12 : u ≠ v
h23 : v ≠ w
h : dist u v + dist v w ≤ dist u w
⊢ u ≠ w
Theorem: sbtw_mk
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
h12 : u ≠ v
h23 : v ≠ w
h : dist u v + dist v w ≤ dist u w
⊢ u ≠ w
Tactic:
rintro rfl
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ dist u u
⊢ False
Theorem: sbtw_mk
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ dist u u
⊢ False
Tactic:
rw [dist_self] at h
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ 0
⊢ False
Theorem: sbtw_mk
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ 0
⊢ False
Tactic:
replace h : dist v u ≤ 0 := by linarith [dist_comm v u]
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist v u ≤ 0
⊢ False
Theorem: sbtw_mk
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist v u ≤ 0
⊢ False
Tactic:
simp only [dist_le_zero] at h
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : v = u
⊢ False
Theorem: sbtw_mk
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : v = u
⊢ False
Tactic:
exact h23 h
Proof state after:
no goals
Theorem: sbtw_mk
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ 0
⊢ dist v u ≤ 0
Tactic:
linarith [dist_comm v u]
Proof state after:
no goals
Theorem: SBtw.sbtw.right_cancel
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ u v w x : V
h : sbtw u v x
h' : sbtw v w x
⊢ Dist.dist u v + Dist.dist v w ≤ Dist.dist u w
Tactic:
linarith [h.dist, h'.dist, dist_triangle u w x, dist_triangle u v w]
Proof state after:
no goals
Theorem: SBtw.sbtw.asymm_right
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
⊢ False
Tactic:
have := h'.dist
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist v u + Dist.dist u x = Dist.dist v x
⊢ False
Theorem: SBtw.sbtw.asymm_right
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist v u + Dist.dist u x = Dist.dist v x
⊢ False
Tactic:
rw [dist_comm] at this
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist u v + Dist.dist u x = Dist.dist v x
⊢ False
Theorem: SBtw.sbtw.asymm_right
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist u v + Dist.dist u x = Dist.dist v x
⊢ False
Tactic:
have : Dist.dist u v = 0 := by linarith [h.dist]
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this✝ : Dist.dist u v + Dist.dist u x = Dist.dist v x
this : Dist.dist u v = 0
⊢ False
Theorem: SBtw.sbtw.asymm_right
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this✝ : Dist.dist u v + Dist.dist u x = Dist.dist v x
this : Dist.dist u v = 0
⊢ False
Tactic:
simp [h.ne12] at this
Proof state after:
no goals
Theorem: SBtw.sbtw.asymm_right
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist u v + Dist.dist u x = Dist.dist v x
⊢ Dist.dist u v = 0
Tactic:
linarith [h.dist]
Proof state after:
no goals
Theorem: SBtw.sbtw.trans_right'
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ u v w x : V
h : sbtw u v x
h' : sbtw v w x
⊢ u ≠ w
Tactic:
rintro rfl
Proof state after:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
⊢ False
Theorem: SBtw.sbtw.trans_right'
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
⊢ False
Tactic:
exact h.asymm_right h'
Proof state after:
no goals
Theorem: SBtw.sbtw.trans_right'
Proof state before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ u v w x : V
h : sbtw u v x
h' : sbtw v w x
this : u ≠ w
⊢ Dist.dist u w + Dist.dist w x ≤ Dist.dist u x
Tactic:
linarith [h.dist, h'.dist, dist_triangle u v w]
Proof state after:
no goals
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
⊢ (modPartitions s d hd h).parts = image (fun i => image (fun x => i + d * x) (range ((s - i - 1) / d + 1))) (range d)
Tactic:
rw [modPartitions]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
⊢ { parts := image (fun i => filter (fun j => j % d = i) (range s)) (range d), supIndep := ⋯, sup_parts := ⋯,
        not_bot_mem := ⋯ }.parts =
    image (fun i => image (fun x => i + d * x) (range ((s - i - 1) / d + 1))) (range d)