-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
private lemma farFromTriangleFree_of_disjoint_triangles_aux {tris : Finset (Finset α)}
    (htris : tris ⊆ G.cliqueFinset 3)
    (pd : (tris : Set (Finset α)).Pairwise fun x y ↦ (x ∩ y : Set α).Subsingleton) (hHG : H ≤ G)
    (hH : H.CliqueFree 3) : #tris ≤ #G.edgeFinset - #H.edgeFinset

Proof state:
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
⊢ False

Tactic:
have ⦃t⦄ (ht : t ∈ tris) :
  ∃ x y, x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset := by
  by_contra! h
  refine hH t ?_
  simp only [not_and, mem_sdiff, not_not, mem_edgeFinset, mem_edgeSet] at h
  obtain ⟨x, y, z, xy, xz, yz, rfl⟩ := is3Clique_iff.1 (mem_cliqueFinset_iff.1 <| htris ht)
  rw [is3Clique_triple_iff]
  refine ⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩ <;> simp

Result:
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
this : ∀ ⦃t : Finset α⦄, t ∈ tris → ∃ x y, x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset
⊢ False

Proof state:
case intro.mk.intro.intro.mk.intro.intro
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
i : (fun x y => (↑x ∩ ↑y).Subsingleton) t₁ t₂
⊢ False

Tactic:
rw [Sym2.eq_iff] at t

Result:
case intro.mk.intro.intro.mk.intro.intro
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
i : (↑t₁ ∩ ↑t₂).Subsingleton
⊢ False

Proof state:
case intro.mk.intro.intro.mk.intro.intro.inr
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
i : (↑t₁ ∩ ↑t₂).Subsingleton
t : fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
⊢ False

Tactic:
exact hfne _ (i ⟨hfx ht₁, t.1.symm ▸ hfy ht₂⟩ ⟨hfy ht₁, t.2.symm ▸ hfx ht₂⟩)

Result:
no goals

Proof state:
case intro.mk.intro.intro.mk.intro.intro
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
⊢ False

Tactic:
have i := pd ht₁ ht₂ (Subtype.val_injective.ne tne)

Result:
case intro.mk.intro.intro.mk.intro.intro
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
i : (fun x y => (↑x ∩ ↑y).Subsingleton) t₁ t₂
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ H.Adj x y ∧ H.Adj x z ∧ H.Adj y z

Tactic:
refine ⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩ <;> simp

Result:
no goals