[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G ↔ ∀ ⦃v w : V⦄, Adj G v w → IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w))
[PROOFSTEP]
simp_rw [isBridge_iff_adj_and_forall_cycle_not_mem]
[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G ↔
    ∀ ⦃v w : V⦄,
      Adj G v w → Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G →
    ∀ ⦃v w : V⦄,
      Adj G v w → Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
intro ha v w hvw
[GOAL]
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : Adj G v w
⊢ Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
apply And.intro hvw
[GOAL]
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : Adj G v w
⊢ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
intro u p hp
[GOAL]
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : Adj G v w
u : V
p : Walk G u u
hp : IsCycle p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
cases ha p hp
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
⊢ (∀ ⦃v w : V⦄,
      Adj G v w →
        Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p) →
    IsAcyclic G
[PROOFSTEP]
rintro hb v (_ | ⟨ha, p⟩) hp
[GOAL]
case mpr.nil
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G v w → Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v : V
hp : IsCycle nil
⊢ False
[PROOFSTEP]
exact hp.not_of_nil
[GOAL]
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G v w → Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : IsCycle (cons ha p)
⊢ False
[PROOFSTEP]
apply (hb ha).2 _ hp
[GOAL]
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G v w → Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : IsCycle (cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges (cons ha p)
[PROOFSTEP]
rw [Walk.edges_cons]
[GOAL]
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G v w → Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : IsCycle (cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) :: edges p
[PROOFSTEP]
apply List.mem_cons_self
[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G ↔ ∀ ⦃e : Sym2 V⦄, e ∈ edgeSet G → IsBridge G e
[PROOFSTEP]
simp [isAcyclic_iff_forall_adj_isBridge, Sym2.forall]
[GOAL]
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p q : Path G v w
⊢ p = q
[PROOFSTEP]
obtain ⟨p, hp⟩ := p
[GOAL]
case mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
q : Path G v w
p : Walk G v w
hp : IsPath p
⊢ { val := p, property := hp } = q
[PROOFSTEP]
obtain ⟨q, hq⟩ := q
[GOAL]
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
[PROOFSTEP]
rw [Subtype.mk.injEq]
[GOAL]
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ p = q
[PROOFSTEP]
induction p with
| nil =>
  cases (Walk.isPath_iff_eq_nil _).mp hq
  rfl
| cons ph p ih =>
  rw [isAcyclic_iff_forall_adj_isBridge] at h
  specialize h ph
  rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
  replace h := h.2 (q.append p.reverse)
  simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h
  cases' h with h h
  ·
    cases q with
    | nil => simp [Walk.isPath_def] at hp
    | cons _ q =>
      rw [Walk.cons_isPath_iff] at hp hq
      simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
      rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
      · cases ih hp.1 q hq.1
        rfl
      · simp at hq
      · exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
  · rw [Walk.cons_isPath_iff] at hp
    exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2
[GOAL]
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ p = q
[PROOFSTEP]
induction p with
| nil =>
  cases (Walk.isPath_iff_eq_nil _).mp hq
  rfl
| cons ph p ih =>
  rw [isAcyclic_iff_forall_adj_isBridge] at h
  specialize h ph
  rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
  replace h := h.2 (q.append p.reverse)
  simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h
  cases' h with h h
  ·
    cases q with
    | nil => simp [Walk.isPath_def] at hp
    | cons _ q =>
      rw [Walk.cons_isPath_iff] at hp hq
      simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
      rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
      · cases ih hp.1 q hq.1
        rfl
      · simp at hq
      · exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
  · rw [Walk.cons_isPath_iff] at hp
    exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2
[GOAL]
case mk.mk.nil
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp : IsPath nil
q : Walk G u✝ u✝
hq : IsPath q
⊢ nil = q
[PROOFSTEP]

| nil =>
  cases (Walk.isPath_iff_eq_nil _).mp hq
  rfl
[GOAL]
case mk.mk.nil
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp : IsPath nil
q : Walk G u✝ u✝
hq : IsPath q
⊢ nil = q
[PROOFSTEP]
cases (Walk.isPath_iff_eq_nil _).mp hq
[GOAL]
case mk.mk.nil.refl
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp hq : IsPath nil
⊢ nil = nil
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
⊢ cons ph p = q
[PROOFSTEP]

| cons ph p ih =>
  rw [isAcyclic_iff_forall_adj_isBridge] at h
  specialize h ph
  rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
  replace h := h.2 (q.append p.reverse)
  simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h
  cases' h with h h
  ·
    cases q with
    | nil => simp [Walk.isPath_def] at hp
    | cons _ q =>
      rw [Walk.cons_isPath_iff] at hp hq
      simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
      rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
      · cases ih hp.1 q hq.1
        rfl
      · simp at hq
      · exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
  · rw [Walk.cons_isPath_iff] at hp
    exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
⊢ cons ph p = q
[PROOFSTEP]
rw [isAcyclic_iff_forall_adj_isBridge] at h
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : ∀ ⦃v w : V⦄, Adj G v w → IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w))
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
⊢ cons ph p = q
[PROOFSTEP]
specialize h ph
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝))
⊢ cons ph p = q
[PROOFSTEP]
rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Adj G u✝ v✝ ∧ ∀ (p : Walk G u✝ v✝), Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
replace h := h.2 (q.append p.reverse)
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges (append q (reverse p))
⊢ cons ph p = q
[PROOFSTEP]
simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges q ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
cases' h with h h
[GOAL]
case mk.mk.cons.inl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges q
⊢ cons ph p = q
[PROOFSTEP]
cases q with
| nil => simp [Walk.isPath_def] at hp
| cons _ q =>
  rw [Walk.cons_isPath_iff] at hp hq
  simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
  rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
  · cases ih hp.1 q hq.1
    rfl
  · simp at hq
  · exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
[GOAL]
case mk.mk.cons.inl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges q
⊢ cons ph p = q
[PROOFSTEP]
cases q with
| nil => simp [Walk.isPath_def] at hp
| cons _ q =>
  rw [Walk.cons_isPath_iff] at hp hq
  simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
  rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
  · cases ih hp.1 q hq.1
    rfl
  · simp at hq
  · exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
[GOAL]
case mk.mk.cons.inl.nil
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ u✝
ih : IsPath p → ∀ (q : Walk G v✝ u✝), IsPath q → p = q
hp : IsPath (cons ph p)
hq : IsPath nil
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges nil
⊢ cons ph p = nil
[PROOFSTEP]

| nil => simp [Walk.isPath_def] at hp
[GOAL]
case mk.mk.cons.inl.nil
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ u✝
ih : IsPath p → ∀ (q : Walk G v✝ u✝), IsPath q → p = q
hp : IsPath (cons ph p)
hq : IsPath nil
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges nil
⊢ cons ph p = nil
[PROOFSTEP]
simp [Walk.isPath_def] at hp
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath (cons h✝ q)
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges (cons h✝ q)
⊢ cons ph p = cons h✝ q
[PROOFSTEP]

| cons _ q =>
  rw [Walk.cons_isPath_iff] at hp hq
  simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
  rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
  · cases ih hp.1 q hq.1
    rfl
  · simp at hq
  · exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath (cons h✝ q)
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges (cons h✝ q)
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
rw [Walk.cons_isPath_iff] at hp hq
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges (cons h✝ q)
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
h : (v✝¹ = v✝ ∨ u✝ = v✝ ∧ v✝¹ = u✝) ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
[GOAL]
case mk.mk.cons.inl.cons.inl.inl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
cases ih hp.1 q hq.1
[GOAL]
case mk.mk.cons.inl.cons.inl.inl.refl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
hq : IsPath p ∧ ¬u✝ ∈ Walk.support p
⊢ cons ph p = cons h✝ p
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.cons.inl.cons.inl.inr.intro
V : Type u
G✝ G : SimpleGraph V
v w v✝ w✝ : V
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
ph : Adj G v✝ v✝
hp : IsPath p ∧ ¬v✝ ∈ Walk.support p
h✝ : Adj G v✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬v✝ ∈ Walk.support q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
simp at hq
[GOAL]
case mk.mk.cons.inl.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
[GOAL]
case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
rw [Walk.cons_isPath_iff] at hp
[GOAL]
case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
⊢ IsAcyclic G
[PROOFSTEP]
intro v c hc
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : IsCycle c
⊢ False
[PROOFSTEP]
simp only [Walk.isCycle_def, Ne.def] at hc
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : IsTrail c ∧ ¬c = nil ∧ List.Nodup (List.tail (Walk.support c))
⊢ False
[PROOFSTEP]
cases c with
| nil => cases hc.2.1 rfl
| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] at hc
  specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
  rw [Path.singleton, Subtype.mk.injEq] at h
  simp [h] at hc
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : IsTrail c ∧ ¬c = nil ∧ List.Nodup (List.tail (Walk.support c))
⊢ False
[PROOFSTEP]
cases c with
| nil => cases hc.2.1 rfl
| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] at hc
  specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
  rw [Path.singleton, Subtype.mk.injEq] at h
  simp [h] at hc
[GOAL]
case nil
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
hc : IsTrail nil ∧ ¬nil = nil ∧ List.Nodup (List.tail (Walk.support nil))
⊢ False
[PROOFSTEP]

| nil => cases hc.2.1 rfl
[GOAL]
case nil
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
hc : IsTrail nil ∧ ¬nil = nil ∧ List.Nodup (List.tail (Walk.support nil))
⊢ False
[PROOFSTEP]
cases hc.2.1 rfl
[GOAL]
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : IsTrail (cons ha c') ∧ ¬cons ha c' = nil ∧ List.Nodup (List.tail (Walk.support (cons ha c')))
⊢ False
[PROOFSTEP]

| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] at hc
  specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
  rw [Path.singleton, Subtype.mk.injEq] at h
  simp [h] at hc
[GOAL]
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : IsTrail (cons ha c') ∧ ¬cons ha c' = nil ∧ List.Nodup (List.tail (Walk.support (cons ha c')))
⊢ False
[PROOFSTEP]
simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] at hc
[GOAL]
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
⊢ False
[PROOFSTEP]
specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
⊢ IsPath c'
[PROOFSTEP]
simp only [Walk.isPath_def, hc.2]
[GOAL]
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
h : { val := c', property := (_ : IsPath c') } = Path.singleton (_ : Adj G v✝ v)
⊢ False
[PROOFSTEP]
rw [Path.singleton, Subtype.mk.injEq] at h
[GOAL]
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
h : c' = cons (_ : Adj G v✝ v) nil
⊢ False
[PROOFSTEP]
simp [h] at hc
[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsTree G ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
classical
rw [IsTree_iff, isAcyclic_iff_path_unique]
constructor
· rintro ⟨hc, hu⟩
  refine ⟨hc.nonempty, ?_⟩
  intro v w
  let q := (hc v w).some.toPath
  use q
  simp only [true_and_iff, Path.isPath]
  intro p hp
  specialize hu ⟨p, hp⟩ q
  exact Subtype.ext_iff.mp hu
· rintro ⟨hV, h⟩
  refine ⟨Connected.mk ?_, ?_⟩
  · intro v w
    obtain ⟨p, _⟩ := h v w
    exact p.reachable
  · rintro v w ⟨p, hp⟩ ⟨q, hq⟩
    simp only [ExistsUnique.unique (h v w) hp hq]
[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsTree G ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
rw [IsTree_iff, isAcyclic_iff_path_unique]
[GOAL]
V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
rintro ⟨hc, hu⟩
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
refine ⟨hc.nonempty, ?_⟩
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
intro v w
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
⊢ ∃! p, IsPath p
[PROOFSTEP]
let q := (hc v w).some.toPath
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∃! p, IsPath p
[PROOFSTEP]
use q
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
⊢ (fun p => IsPath p) ↑q ∧ ∀ (y : Walk G v w), (fun p => IsPath p) y → y = ↑q
[PROOFSTEP]
simp only [true_and_iff, Path.isPath]
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∀ (y : Walk G v w), IsPath y → y = ↑(toPath (Nonempty.some (_ : Reachable G v w)))
[PROOFSTEP]
intro p hp
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : IsPath p
⊢ p = ↑(toPath (Nonempty.some (_ : Reachable G v w)))
[PROOFSTEP]
specialize hu ⟨p, hp⟩ q
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : IsPath p
hu : { val := p, property := hp } = q
⊢ p = ↑(toPath (Nonempty.some (_ : Reachable G v w)))
[PROOFSTEP]
exact Subtype.ext_iff.mp hu
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p) → Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
[PROOFSTEP]
rintro ⟨hV, h⟩
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
⊢ Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
[PROOFSTEP]
refine ⟨Connected.mk ?_, ?_⟩
[GOAL]
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
⊢ Preconnected G
[PROOFSTEP]
intro v w
[GOAL]
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
v w : V
⊢ Reachable G v w
[PROOFSTEP]
obtain ⟨p, _⟩ := h v w
[GOAL]
case mpr.intro.refine_1.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
v w : V
p : Walk G v w
h✝ : (fun p => IsPath p) p ∧ ∀ (y : Walk G v w), (fun p => IsPath p) y → y = p
⊢ Reachable G v w
[PROOFSTEP]
exact p.reachable
[GOAL]
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
⊢ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
[PROOFSTEP]
rintro v w ⟨p, hp⟩ ⟨q, hq⟩
[GOAL]
case mpr.intro.refine_2.mk.mk
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
[PROOFSTEP]
simp only [ExistsUnique.unique (h v w) hp hq]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
have := hG.isConnected.nonempty
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
inhabit V
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
inhabited_h : Inhabited V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
classical
have : Finset.card ({ default } : Finset V)ᶜ + 1 = Fintype.card V := by
  rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
rw [← this, add_left_inj]
choose f hf hf' using (hG.existsUnique_path · default)
refine Eq.symm <| Finset.card_congr (fun w hw => ((f w).firstDart <| ?notNil).edge) (fun a ha => ?memEdges) ?inj ?surj
case notNil => exact not_nil_of_ne (by simpa using hw)
case memEdges => simp
case inj =>
  intros a b ha hb h
  wlog h' : (f a).length ≤ (f b).length generalizing a b
  · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
  rw [dart_edge_eq_iff] at h
  obtain (h | h) := h
  · exact (congrArg (·.fst) h)
  · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
    have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
    rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3
    · exfalso
      linarith
    · simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
      exact (hf _).tail _
case surj =>
  simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
  intros x y h
  wlog h' : (f x).length ≤ (f y).length generalizing x y
  · rw [Sym2.eq_swap]
    exact this y x h.symm (le_of_not_le h')
  refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
  · rintro rfl
    rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
      length_cons, length_nil] at h'
    simp [le_zero_iff, Nat.one_ne_zero] at h'
  rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
  rfl
  case contra =>
    suffices : (f x).takeUntil y hy = .cons h .nil
    · rw [← take_spec _ hy] at h'
      simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
    refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
    simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
inhabited_h : Inhabited V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
have : Finset.card ({ default } : Finset V)ᶜ + 1 = Fintype.card V := by
  rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
inhabited_h : Inhabited V
⊢ Finset.card {default}ᶜ + 1 = Fintype.card V
[PROOFSTEP]
rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
rw [← this, add_left_inj]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
⊢ Finset.card (edgeFinset G) = Finset.card {default}ᶜ
[PROOFSTEP]
choose f hf hf' using (hG.existsUnique_path · default)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ Finset.card (edgeFinset G) = Finset.card {default}ᶜ
[PROOFSTEP]
refine Eq.symm <| Finset.card_congr (fun w hw => ((f w).firstDart <| ?notNil).edge) (fun a ha => ?memEdges) ?inj ?surj
[GOAL]
case notNil
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ ¬Nil (f w)
case memEdges
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case notNil => exact not_nil_of_ne (by simpa using hw)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ ¬Nil (f w)
[PROOFSTEP]
case notNil => exact not_nil_of_ne (by simpa using hw)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ ¬Nil (f w)
[PROOFSTEP]
exact not_nil_of_ne (by simpa using hw)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ w ≠ default
[PROOFSTEP]
simpa using hw
[GOAL]
case memEdges
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case memEdges => simp
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
[PROOFSTEP]
case memEdges => simp
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
[PROOFSTEP]
simp
[GOAL]
case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case inj =>
  intros a b ha hb h
  wlog h' : (f a).length ≤ (f b).length generalizing a b
  · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
  rw [dart_edge_eq_iff] at h
  obtain (h | h) := h
  · exact (congrArg (·.fst) h)
  · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
    have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
    rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3
    · exfalso
      linarith
    · simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
      exact (hf _).tail _
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
[PROOFSTEP]
case inj =>
  intros a b ha hb h
  wlog h' : (f a).length ≤ (f b).length generalizing a b
  · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
  rw [dart_edge_eq_iff] at h
  obtain (h | h) := h
  · exact (congrArg (·.fst) h)
  · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
    have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
    rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3
    · exfalso
      linarith
    · simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
      exact (hf _).tail _
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
[PROOFSTEP]
intros a b ha hb h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb
⊢ a = b
[PROOFSTEP]
wlog h' : (f a).length ≤ (f b).length generalizing a b
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb
this :
  ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      length (f a) ≤ length (f b) → a = b
h' : ¬length (f a) ≤ length (f b)
⊢ a = b
[PROOFSTEP]
exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb
h' : length (f a) ≤ length (f b)
⊢ a = b
[PROOFSTEP]
rw [dart_edge_eq_iff] at h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  firstDart (f a) (_ : ¬Nil (f a)) = firstDart (f b) (_ : ¬Nil (f b)) ∨
    firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h' : length (f a) ≤ length (f b)
⊢ a = b
[PROOFSTEP]
obtain (h | h) := h
[GOAL]
case inl
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = firstDart (f b) (_ : ¬Nil (f b))
⊢ a = b
[PROOFSTEP]
exact (congrArg (·.fst) h)
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
⊢ a = b
[PROOFSTEP]
have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
⊢ a ≠ default
[PROOFSTEP]
simpa using ha
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ a = b
[PROOFSTEP]
have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
[GOAL]
case inr.refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
h3 : length (Walk.copy (tail (f a) (_ : ¬Nil (f a))) h1 (_ : default = default)) = length (f b)
⊢ a = b
case inr.refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ (fun p => IsPath p) (Walk.copy (tail (f a) (_ : ¬Nil (f a))) h1 (_ : default = default))
[PROOFSTEP]
rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3
[GOAL]
case inr.refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
h3✝ : length (tail (f a) (_ : ¬Nil (f a))) = length (f b)
h3 : length (f a) = length (f b) + 1
⊢ a = b
[PROOFSTEP]
exfalso
[GOAL]
case inr.refine_2.h
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
h3✝ : length (tail (f a) (_ : ¬Nil (f a))) = length (f b)
h3 : length (f a) = length (f b) + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case inr.refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ (fun p => IsPath p) (Walk.copy (tail (f a) (_ : ¬Nil (f a))) h1 (_ : default = default))
[PROOFSTEP]
simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
[GOAL]
case inr.refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ IsPath (tail (f a) (_ : ¬Nil (f a)))
[PROOFSTEP]
exact (hf _).tail _
[GOAL]
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case surj =>
  simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
  intros x y h
  wlog h' : (f x).length ≤ (f y).length generalizing x y
  · rw [Sym2.eq_swap]
    exact this y x h.symm (le_of_not_le h')
  refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
  · rintro rfl
    rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
      length_cons, length_nil] at h'
    simp [le_zero_iff, Nat.one_ne_zero] at h'
  rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
  rfl
  case contra =>
    suffices : (f x).takeUntil y hy = .cons h .nil
    · rw [← take_spec _ hy] at h'
      simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
    refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
    simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case surj =>
  simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
  intros x y h
  wlog h' : (f x).length ≤ (f y).length generalizing x y
  · rw [Sym2.eq_swap]
    exact this y x h.symm (le_of_not_le h')
  refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
  · rintro rfl
    rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
      length_cons, length_nil] at h'
    simp [le_zero_iff, Nat.one_ne_zero] at h'
  rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
  rfl
  case contra =>
    suffices : (f x).takeUntil y hy = .cons h .nil
    · rw [← take_spec _ hy] at h'
      simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
    refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
    simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (x y : V), Adj G x y → ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
intros x y h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
wlog h' : (f x).length ≤ (f y).length generalizing x y
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
this :
  ∀ (x y : V),
    Adj G x y →
      length (f x) ≤ length (f y) →
        ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
h' : ¬length (f x) ≤ length (f y)
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
this :
  ∀ (x y : V),
    Adj G x y →
      length (f x) ≤ length (f y) →
        ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
h' : ¬length (f x) ≤ length (f y)
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (y, x)
[PROOFSTEP]
exact this y x h.symm (le_of_not_le h')
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
[GOAL]
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ ¬y = default
[PROOFSTEP]
rintro rfl
[GOAL]
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x : V
h : Adj G x default
h' : length (f x) ≤ length (f default)
⊢ False
[PROOFSTEP]
rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne), length_cons,
  length_nil] at h'
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x : V
h : Adj G x default
h' : length (f x) ≤ 0
⊢ ¬x ∈ Walk.support nil
[PROOFSTEP]
simpa using h.ne
[GOAL]
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x : V
h : Adj G x default
h' : 0 + 1 ≤ 0
⊢ False
[PROOFSTEP]
simp [le_zero_iff, Nat.one_ne_zero] at h'
[GOAL]
case refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ (firstDart (f y) (_ : ¬Nil (f y))).toProd = Prod.swap (x, y)
[PROOFSTEP]
rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
[GOAL]
case refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ (firstDart (cons (_ : Adj G y x) (f x)) (_ : ¬Nil (cons (_ : Adj G y x) (f x)))).toProd = Prod.swap (x, y)
case contra
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case contra
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
case contra =>
  suffices : (f x).takeUntil y hy = .cons h .nil
  · rw [← take_spec _ hy] at h'
    simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
  refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
  simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
case contra =>
  suffices : (f x).takeUntil y hy = .cons h .nil
  · rw [← take_spec _ hy] at h'
    simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
  refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
  simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
suffices : (f x).takeUntil y hy = .cons h .nil
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
this : takeUntil (f x) y hy = cons h nil
⊢ False
[PROOFSTEP]
rw [← take_spec _ hy] at h'
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
hy : y ∈ Walk.support (f x)
h' : length (append (takeUntil (f x) y hy) (dropUntil (f x) y hy)) ≤ length (f y)
this : takeUntil (f x) y hy = cons h nil
⊢ False
[PROOFSTEP]
simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
[GOAL]
case this
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ takeUntil (f x) y hy = cons h nil
[PROOFSTEP]
refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
[GOAL]
case this
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ IsPath (cons h nil)
[PROOFSTEP]
simp [h.ne]


[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
[PROOFSTEP]
let i : DecidableRel ((· ⊆ ·) : Finset α → Finset α → Prop) := fun _ _ => Classical.dec _
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
⊢ card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
[PROOFSTEP]
refine' card_mul_le_card_mul' (· ⊆ ·) (fun s hs => _) (fun s hs => _)
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ r ≤ card (bipartiteBelow (fun x x_1 => x ⊆ x_1) (∂ 𝒜) s)
[PROOFSTEP]
rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ card (image (erase s) s) ≤ card (bipartiteBelow (fun x x_1 => x ⊆ x_1) (∂ 𝒜) s)
[PROOFSTEP]
refine' card_le_of_subset _
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ image (erase s) s ⊆ bipartiteBelow (fun x x_1 => x ⊆ x_1) (∂ 𝒜) s
[PROOFSTEP]
simp_rw [image_subset_iff, mem_bipartiteBelow]
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ (x : α), x ∈ s → erase s x ∈ ∂ 𝒜 ∧ erase s x ⊆ s
[PROOFSTEP]
exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ Fintype.card α - r + 1
[PROOFSTEP]
refine' le_trans _ tsub_tsub_le_tsub_add
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ Fintype.card α - (r - 1)
[PROOFSTEP]
rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ card (image (fun a => insert a s) sᶜ)
[PROOFSTEP]
refine'
  card_le_of_subset fun t ht =>
    _
      -- porting note: commented out the following line
        -- infer_instance
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
rw [mem_bipartiteAbove] at ht
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
have : ∅ ∉ 𝒜 := by
  rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
  rintro rfl
  rw [shadow_singleton_empty] at hs
  exact not_mem_empty s hs
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬∅ ∈ 𝒜
[PROOFSTEP]
rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∂ {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
[PROOFSTEP]
rw [shadow_singleton_empty] at hs
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
[PROOFSTEP]
exact not_mem_empty s hs
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
have h :=
  exists_eq_insert_iff.2 ⟨ht.2, by rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]⟩
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
⊢ card s + 1 = card t
[PROOFSTEP]
rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
h : ∃ a x, insert a s = t
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
rcases h with ⟨a, ha, rfl⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
this : ¬∅ ∈ 𝒜
a : α
ha : ¬a ∈ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ insert a s ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
exact mem_image_of_mem _ (mem_compl.2 ha)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card (∂ 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
[PROOFSTEP]
obtain hr' | hr' := lt_or_le (Fintype.card α) r
[GOAL]
case inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card (∂ 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
[PROOFSTEP]
rw [choose_eq_zero_of_lt hr', cast_zero, div_zero]
[GOAL]
case inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ 0 ≤ ↑(card (∂ 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
[PROOFSTEP]
exact div_nonneg (cast_nonneg _) (cast_nonneg _)
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : r ≤ Fintype.card α
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card (∂ 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
[PROOFSTEP]
replace h𝒜 := card_mul_le_card_shadow_mul h𝒜
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card (∂ 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
[PROOFSTEP]
rw [div_le_div_iff]
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(card 𝒜) * ↑(Nat.choose (Fintype.card α) (r - 1)) ≤ ↑(card (∂ 𝒜)) * ↑(Nat.choose (Fintype.card α) r)
[PROOFSTEP]
norm_cast
[GOAL]
case inr.b0
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑(Nat.choose (Fintype.card α) r)
[PROOFSTEP]
norm_cast
[GOAL]
case inr.d0
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑(Nat.choose (Fintype.card α) (r - 1))
[PROOFSTEP]
norm_cast
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r - 1) ≤ card (∂ 𝒜) * Nat.choose (Fintype.card α) r
[PROOFSTEP]
cases' r with r
[GOAL]
case inr.zero
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
hr : zero ≠ 0
hr' : zero ≤ Fintype.card α
h𝒜 : card 𝒜 * zero ≤ card (∂ 𝒜) * (Fintype.card α - zero + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (zero - 1) ≤ card (∂ 𝒜) * Nat.choose (Fintype.card α) zero
[PROOFSTEP]
exact (hr rfl).elim
[GOAL]
case inr.succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : succ r ≠ 0
hr' : succ r ≤ Fintype.card α
h𝒜 : card 𝒜 * succ r ≤ card (∂ 𝒜) * (Fintype.card α - succ r + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (succ r - 1) ≤ card (∂ 𝒜) * Nat.choose (Fintype.card α) (succ r)
[PROOFSTEP]
rw [Nat.succ_eq_add_one] at *
[GOAL]
case inr.succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card (∂ 𝒜) * (Fintype.card α - (r + 1) + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) ≤ card (∂ 𝒜) * Nat.choose (Fintype.card α) (r + 1)
[PROOFSTEP]
rw [tsub_add_eq_add_tsub hr', add_tsub_add_eq_tsub_right] at h𝒜
[GOAL]
case inr.succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card (∂ 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) ≤ card (∂ 𝒜) * Nat.choose (Fintype.card α) (r + 1)
[PROOFSTEP]
apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card (∂ 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) * (r + 1) ≤
    card (∂ 𝒜) * Nat.choose (Fintype.card α) (r + 1) * (r + 1)
[PROOFSTEP]
convert Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card (∂ 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) * (r + 1) = card 𝒜 * (r + 1) * Nat.choose (Fintype.card α) r
[PROOFSTEP]
simp [mul_assoc, Nat.choose_succ_right_eq]
[GOAL]
case h.e'_3
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card (∂ 𝒜) * (Fintype.card α - r)
⊢ Nat.choose (Fintype.card α) r * (r + 1) = (r + 1) * Nat.choose (Fintype.card α) r ∨ 𝒜 = ∅
[PROOFSTEP]
exact Or.inl (mul_comm _ _)
[GOAL]
case h.e'_4
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card (∂ 𝒜) * (Fintype.card α - r)
⊢ card (∂ 𝒜) * Nat.choose (Fintype.card α) (r + 1) * (r + 1) =
    card (∂ 𝒜) * (Fintype.card α - r) * Nat.choose (Fintype.card α) r
[PROOFSTEP]
simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
[GOAL]
case h.e'_4
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card (∂ 𝒜) * (Fintype.card α - r)
⊢ Nat.choose (Fintype.card α) r * (Fintype.card α - r) = (Fintype.card α - r) * Nat.choose (Fintype.card α) r ∨
    card (∂ 𝒜) = 0
[PROOFSTEP]
exact Or.inl (mul_comm _ _)
[GOAL]
case inr.b0
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < Nat.choose (Fintype.card α) r
[PROOFSTEP]
exact Nat.choose_pos hr'
[GOAL]
case inr.d0
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < Nat.choose (Fintype.card α) (r - 1)
[PROOFSTEP]
exact Nat.choose_pos (r.pred_le.trans hr')
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ falling k 𝒜 ↔ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
simp_rw [falling, mem_sup, mem_powersetLen]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ v, v ∈ 𝒜 ∧ s ⊆ v ∧ card s = k) ↔ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
aesop
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜
[PROOFSTEP]
ext s
[GOAL]
case a
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
[PROOFSTEP]
simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
[GOAL]
case a
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) ↔
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
constructor
[GOAL]
case a.mp
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) →
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)
[GOAL]
case a.mp.inl
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
h : s ∈ 𝒜 ∧ card s = k
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
[GOAL]
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t, t ∈ 𝒜 ∧ erase s a ⊆ t) ∧ card (erase s a) = k
[PROOFSTEP]
refine' ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, _⟩
[GOAL]
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ card (erase s a) = k
[PROOFSTEP]
rw [card_erase_of_mem ha, hs]
[GOAL]
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k
[PROOFSTEP]
rfl
[GOAL]
case a.mpr
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k →
    s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
rintro ⟨⟨t, ht, hst⟩, hs⟩
[GOAL]
case a.mpr.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
by_cases h : s ∈ 𝒜
[GOAL]
case pos
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
exact Or.inl ⟨h, hs⟩
[GOAL]
case neg
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : ¬s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_not_mem h).symm)
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
refine' Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, _⟩, a, mem_insert_self _ _, erase_insert ha⟩
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ card (insert a s) = k + 1
[PROOFSTEP]
rw [card_insert_of_not_mem ha, hs]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False
[PROOFSTEP]
simp_rw [mem_shadow_iff, mem_falling] at h₁
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = n) ∧ ∃ a, a ∈ t ∧ erase t a = s
⊢ False
[PROOFSTEP]
obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ False
[PROOFSTEP]
refine' h𝒜 (slice_subset h₂) ht _ ((erase_subset _ _).trans hst)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ erase s a ≠ t
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
ht : erase s a ∈ 𝒜
hst : s ⊆ erase s a
⊢ False
[PROOFSTEP]
exact not_mem_erase _ _ (hst ha)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
hk : zero ≤ Fintype.card α
⊢ ∑ r in range (zero + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - zero) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - zero))
[PROOFSTEP]
simp only [tsub_zero, cast_one, cast_le, sum_singleton, div_one, choose_self, range_one, zero_eq, zero_add, range_one,
  ge_iff_le, sum_singleton, nonpos_iff_eq_zero, tsub_zero, choose_self, cast_one, div_one, cast_le]
[GOAL]
case zero
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
hk : zero ≤ Fintype.card α
⊢ card (𝒜 # Fintype.card α) ≤ card (falling (Fintype.card α) 𝒜)
[PROOFSTEP]
exact card_le_of_subset (slice_subset_falling _ _)
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : succ k ≤ Fintype.card α
⊢ ∑ r in range (succ k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - succ k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - succ k))
[PROOFSTEP]
rw [succ_eq_add_one] at *
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ r in range (k + 1 + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - (k + 1)) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1)))
[PROOFSTEP]
rw [sum_range_succ, ← slice_union_shadow_falling_succ,
  card_disjoint_union (IsAntichain.disjoint_slice_shadow_falling h𝒜), cast_add, _root_.add_div, add_comm]
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(card (𝒜 # (Fintype.card α - (k + 1)))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1))) +
      ∑ x in range (k + 1), ↑(card (𝒜 # (Fintype.card α - x))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - x)) ≤
    ↑(card (𝒜 # (Fintype.card α - (k + 1)))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1))) +
      ↑(card (∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1)))
[PROOFSTEP]
rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(card (𝒜 # (Fintype.card α - k - 1))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1)) +
      ∑ x in range (k + 1), ↑(card (𝒜 # (Fintype.card α - x))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - x)) ≤
    ↑(card (𝒜 # (Fintype.card α - k - 1))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1)) +
      ↑(card (∂ (falling (Fintype.card α - k) 𝒜))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1))
[PROOFSTEP]
exact
  add_le_add_left
    ((ih <| le_of_succ_le hk).trans <|
      card_div_choose_le_card_shadow_div_choose (tsub_pos_iff_lt.2 <| Nat.succ_le_iff.1 hk).ne' <| sized_falling _ _)
    _
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (Fintype.card α + 1), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r) ≤ 1
[PROOFSTEP]
classical
rw [← sum_flip]
refine' (le_card_falling_div_choose le_rfl h𝒜).trans _
rw [div_le_iff] <;> norm_cast
· simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using Set.Sized.card_le (sized_falling 0 𝒜)
· rw [tsub_self, choose_zero_right]
  exact zero_lt_one
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (Fintype.card α + 1), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r) ≤ 1
[PROOFSTEP]
rw [← sum_flip]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (Fintype.card α + 1),
      ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    1
[PROOFSTEP]
refine' (le_card_falling_div_choose le_rfl h𝒜).trans _
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ↑(card (falling (Fintype.card α - Fintype.card α) 𝒜)) /
      ↑(Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)) ≤
    1
[PROOFSTEP]
rw [div_le_iff]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ↑(card (falling (Fintype.card α - Fintype.card α) 𝒜)) ≤
    1 * ↑(Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α))
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α))
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card (falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)
[PROOFSTEP]
simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using Set.Sized.card_le (sized_falling 0 𝒜)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)
[PROOFSTEP]
rw [tsub_self, choose_zero_right]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
[PROOFSTEP]
classical
suffices (∑ r in Iic (Fintype.card α), ((𝒜 # r).card : ℚ) / (Fintype.card α).choose (Fintype.card α / 2)) ≤ 1
  by
  rw [← sum_div, ← Nat.cast_sum, div_le_one] at this
  simp only [cast_le] at this
  rwa [sum_card_slice] at this
  simp only [cast_pos]
  exact choose_pos (Nat.div_le_self _ _)
rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range]
refine' (sum_le_sum fun r hr => _).trans (sum_card_slice_div_choose_le_one h𝒜)
rw [mem_range] at hr
refine' div_le_div_of_le_left _ _ _ <;> norm_cast
· exact Nat.zero_le _
· exact choose_pos (lt_succ_iff.1 hr)
· exact choose_le_middle _ _
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
[PROOFSTEP]
suffices (∑ r in Iic (Fintype.card α), ((𝒜 # r).card : ℚ) / (Fintype.card α).choose (Fintype.card α / 2)) ≤ 1
  by
  rw [← sum_div, ← Nat.cast_sum, div_le_one] at this
  simp only [cast_le] at this
  rwa [sum_card_slice] at this
  simp only [cast_pos]
  exact choose_pos (Nat.div_le_self _ _)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ∑ r in Iic (Fintype.card α), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
[PROOFSTEP]
rw [← sum_div, ← Nat.cast_sum, div_le_one] at this
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) ≤ ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
[PROOFSTEP]
simp only [cast_le] at this
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ∑ x in Iic (Fintype.card α), card (𝒜 # x) ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
[PROOFSTEP]
rwa [sum_card_slice] at this
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
[PROOFSTEP]
simp only [cast_pos]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < Nat.choose (Fintype.card α) (Fintype.card α / 2)
[PROOFSTEP]
exact choose_pos (Nat.div_le_self _ _)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in Iic (Fintype.card α), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
[PROOFSTEP]
rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (succ (Fintype.card α)), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
[PROOFSTEP]
refine' (sum_le_sum fun r hr => _).trans (sum_card_slice_div_choose_le_one h𝒜)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r ∈ range (succ (Fintype.card α))
⊢ ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤
    ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r)
[PROOFSTEP]
rw [mem_range] at hr
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤
    ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r)
[PROOFSTEP]
refine' div_le_div_of_le_left _ _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 ≤ ↑(card (𝒜 # r))
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 < ↑(Nat.choose (Fintype.card α) r)
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_3
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ ↑(Nat.choose (Fintype.card α) r) ≤ ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 ≤ card (𝒜 # r)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 < Nat.choose (Fintype.card α) r
[PROOFSTEP]
exact choose_pos (lt_succ_iff.1 hr)
[GOAL]
case refine'_3
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ Nat.choose (Fintype.card α) r ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
[PROOFSTEP]
exact choose_le_middle _ _