internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Subgraph.image_coe_edgeSet_coe
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
⊢ Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet
Tactic:
rw [edgeSet_coe, Set.image_preimage_eq_iff]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)
Theorem: SimpleGraph.Subgraph.image_coe_edgeSet_coe
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)
Tactic:
rintro e he
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
⊢ e ∈ Set.range (Sym2.map Subtype.val)
Theorem: SimpleGraph.Subgraph.image_coe_edgeSet_coe
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
⊢ e ∈ Set.range (Sym2.map Subtype.val)
Tactic:
induction' e using Sym2.ind with a b
Proof state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : V
he : s(a, b) ∈ G'.edgeSet
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)
Theorem: SimpleGraph.Subgraph.image_coe_edgeSet_coe
Proof state before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : V
he : s(a, b) ∈ G'.edgeSet
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)
Tactic:
rw [Subgraph.mem_edgeSet] at he
Proof state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)
Theorem: SimpleGraph.Subgraph.image_coe_edgeSet_coe
Proof state before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)
Tactic:
exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_pair_eq _ _ _⟩
Proof state after:
no goals
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
⊢ ∂ (initSeg s) = initSeg (s.erase (s.min' hs))
Tactic:
ext t
Proof state after:
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))
Tactic:
simp only [mem_shadow_iff_insert_mem, mem_initSeg, exists_prop]
Proof state after:
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }) ↔
    (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }) ↔
    (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
Tactic:
constructor
Proof state after:
case a.mp
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }) →
    (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }

case a.mpr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) } →
    ∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) } →
    ∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }
Tactic:
simp_rw [le_iff_eq_or_lt, lt_iff_exists_forall_lt_mem_iff_mem]
Proof state after:
case a.mpr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (s.erase (s.min' hs)).card = t.card ∧
      ({ ofColex := t } = { ofColex := s.erase (s.min' hs) } ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
    ∃ a ∉ t,
      s.card = (insert a t).card ∧
        ({ ofColex := insert a t } = { ofColex := s } ∨
          ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (s.erase (s.min' hs)).card = t.card ∧
      ({ ofColex := t } = { ofColex := s.erase (s.min' hs) } ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
    ∃ a ∉ t,
      s.card = (insert a t).card ∧
        ({ ofColex := insert a t } = { ofColex := s } ∨
          ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic:
simp only [toColex_inj, ofColex_toColex, ne_eq, and_imp]
Proof state after:
case a.mpr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (s.erase (s.min' hs)).card = t.card →
    (t = s.erase (s.min' hs) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
      ∃ a ∉ t,
        s.card = (insert a t).card ∧
          (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (s.erase (s.min' hs)).card = t.card →
    (t = s.erase (s.min' hs) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
      ∃ a ∉ t,
        s.card = (insert a t).card ∧
          (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic:
rintro cards' (rfl | ⟨k, hks, hkt, z⟩)
Proof state after:
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ ∃ a ∉ s.erase (s.min' hs),
    s.card = (insert a (s.erase (s.min' hs))).card ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))

case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic:
set j := min' tᶜ ⟨k, mem_compl.2 hkt⟩
Proof state after:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic:
have hjk : j ≤ k := min'_le _ _ (mem_compl.2 ‹k ∉ t›)
Proof state after:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic:
have : j ∉ t := mem_compl.1 (min'_mem _ _)
Proof state after:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic:
have hcard : card s = card (insert j t) := by
  rw [card_insert_of_not_mem ‹j ∉ t›, ← ‹_ = card t›, card_erase_add_one (min'_mem _ _)]
Proof state after:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic:
refine' ⟨j, ‹_›, hcard, _⟩
Proof state after:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Tactic:
obtain hjk | r₁ := hjk.lt_or_eq
Proof state after:
case a.mpr.inr.intro.intro.intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk✝ : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
hjk : j < k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

case a.mpr.inr.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Tactic:
refine' Or.inl (eq_of_subset_of_card_le (fun a ha ↦ _) hcard.ge).symm
Proof state after:
case a.mpr.inr.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
⊢ a ∈ insert j t
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
⊢ a ∈ insert j t
Tactic:
rcases lt_trichotomy k a with (lt | rfl | gt)
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ insert j t

case a.mpr.inr.intro.intro.intro.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert j t

case a.mpr.inr.intro.intro.intro.inr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ insert j t
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mp
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }) →
    (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
Tactic:
rintro ⟨a, ha, hst, hts⟩
Proof state after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : s.card = (insert a t).card
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : s.card = (insert a t).card
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
Tactic:
constructor
Proof state after:
case a.mp.intro.intro.intro.left
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : s.card = (insert a t).card
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ (s.erase (s.min' hs)).card = t.card

case a.mp.intro.intro.intro.right
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : s.card = (insert a t).card
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mp.intro.intro.intro.left
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : s.card = (insert a t).card
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ (s.erase (s.min' hs)).card = t.card
Tactic:
rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_not_mem ha, add_tsub_cancel_right]
Proof state after:
no goals
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mp.intro.intro.intro.right
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : s.card = (insert a t).card
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
Tactic:
simpa [ha] using erase_le_erase_min' hts hst.ge (mem_insert_self _ _)
Proof state after:
no goals
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ ∃ a ∉ s.erase (s.min' hs),
    s.card = (insert a (s.erase (s.min' hs))).card ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))
Tactic:
refine' ⟨min' s hs, not_mem_erase _ _, _⟩
Proof state after:
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ s.card = (insert (s.min' hs) (s.erase (s.min' hs))).card ∧
    (insert (s.min' hs) (s.erase (s.min' hs)) = s ∨
      ∃ w ∈ s,
        w ∉ insert (s.min' hs) (s.erase (s.min' hs)) ∧
          ∀ ⦃a : α⦄, w < a → (a ∈ insert (s.min' hs) (s.erase (s.min' hs)) ↔ a ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ s.card = (insert (s.min' hs) (s.erase (s.min' hs))).card ∧
    (insert (s.min' hs) (s.erase (s.min' hs)) = s ∨
      ∃ w ∈ s,
        w ∉ insert (s.min' hs) (s.erase (s.min' hs)) ∧
          ∀ ⦃a : α⦄, w < a → (a ∈ insert (s.min' hs) (s.erase (s.min' hs)) ↔ a ∈ s))
Tactic:
rw [insert_erase (min'_mem _ _)]
Proof state after:
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ s.card = s.card ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ s.card = s.card ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))
Tactic:
exact ⟨rfl, Or.inl rfl⟩
Proof state after:
no goals
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
⊢ s.card = (insert j t).card
Tactic:
rw [card_insert_of_not_mem ‹j ∉ t›, ← ‹_ = card t›, card_erase_add_one (min'_mem _ _)]
Proof state after:
no goals