-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma IsMaximumClique.isMaximalClique [Fintype α] (s : Finset α) (M : G.IsMaximumClique s) :
    Maximal G.IsClique s :=
  ⟨ M.isClique,
    fun t ht hsub => by
      by_contra hc
      have fint : Fintype t := ofFinite ↑t
      have ne : s ≠ t.toFinset := fun a ↦ by subst a; simp_all[Set.coe_toFinset, not_true_eq_false]
      have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])
      have hlt : #s < #t.toFinset :=
        card_lt_card (ssubset_of_ne_of_subset ne (Set.subset_toFinset.mpr hsub))
      exact lt_irrefl _ (lt_of_lt_of_le hlt hle) ⟩

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
a : s = t.toFinset
⊢ False

Tactic:
subst a

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Set α
ht : G.IsClique t
fint : Fintype ↑t
M : G.IsMaximumClique t.toFinset
hsub : ↑t.toFinset ≤ t
hc : ¬t ≤ ↑t.toFinset
⊢ False

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
⊢ False

Tactic:
have ne : s ≠ t.toFinset := fun a ↦ by subst a; simp_all[Set.coe_toFinset, not_true_eq_false]

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
⊢ False

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
⊢ False

Tactic:
have fint : Fintype t := ofFinite ↑t

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
⊢ False

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
⊢ False

Tactic:
have hlt : #s < #t.toFinset :=
  card_lt_card (ssubset_of_ne_of_subset ne (Set.subset_toFinset.mpr hsub))

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
hlt : #s < #t.toFinset
⊢ False

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
⊢ t ≤ ↑s

Tactic:
by_contra hc

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
⊢ False

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
⊢ False

Tactic:
have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
⊢ False

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
hlt : #s < #t.toFinset
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_lt_of_le hlt hle)

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ≤ t
hc : ¬t ≤ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
⊢ G.IsClique ↑t.toFinset

Tactic:
simp [Set.coe_toFinset, ht]

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Set α
ht : G.IsClique t
fint : Fintype ↑t
M : G.IsMaximumClique t.toFinset
hsub : ↑t.toFinset ≤ t
hc : ¬t ≤ ↑t.toFinset
⊢ False

Tactic:
simp_all[Set.coe_toFinset, not_true_eq_false]

Result:
no goals