awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
refine_1 : ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)
⊢ #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3
have refine_2 : ∀ b ∈ G.cliqueFinset 3, #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3
Tactic: refine card_mul_le_card_mul (fun e s ↦ e ∈ s.sym2) ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ b ∈ G.cliqueFinset 3, #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3
have refine_2 : ∀ (b : Finset α) (x x_1 x_2 : α),
  G.Adj x x_1 →
    G.Adj x x_2 →
      G.Adj x_1 x_2 →
        b = {x, x_1, x_2} → #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3
Tactic: simp only [mem_cliqueFinset_iff, is3Clique_iff, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ Finset.card (α := Sym2 α) {s(b, c)} + 1 = 2
have rw : HAdd.hAdd (α := ℕ) 1 1 = 2
Tactic: rw [card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset {a, b, c}) ≤ 3
have refine_2 : bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset {a, b, c} ⊆ {s(a, b), s(a, c), s(b, c)}
Tactic: calc
    _ ≤ #{s(a, b), s(a, c), s(b, c)} := card_le_card ?_
    _ ≤ 3 := (card_insert_le _ _).trans (succ_le_succ <| (card_insert_le _ _).trans_eq <| by
      rw [card_singleton])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset {a, b, c} ⊆ {s(a, b), s(a, c), s(b, c)}
have refine_2 : ∀ (x y : α),
  G.Adj x y → x = a ∨ x = b ∨ x = c → y = a ∨ y = b ∨ y = c → s(x, y) = s(a, b) ∨ s(x, y) = s(a, c) ∨ s(x, y) = s(b, c)
Tactic: simp only [subset_iff, Sym2.forall, mem_sym2_iff, mem_bipartiteBelow, mem_insert,
    mem_edgeFinset, mem_singleton, and_imp, mem_edgeSet, Sym2.mem_iff, forall_eq_or_imp,
    forall_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε δ : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
hε : G.FarFromTriangleFree ε
h : δ ≤ ε
⊢ δ * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜)
have ha : LE.le.{u_3} (α := 𝕜) 0 (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
⊢ #tris ≤ #G.edgeFinset - #H.edgeFinset
have rw : #tris.attach ≤ #(G.edgeFinset \ H.edgeFinset)
Tactic: rw [← card_sdiff_of_subset (edgeFinset_mono hHG), ← card_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
⊢ #tris.attach ≤ #(G.edgeFinset \ H.edgeFinset)
have by_contra! : ∀ (hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach), False
Tactic: by_contra! hG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
⊢ ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset
have by_contra! : ∀ (h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), s(x, y) ∉ G.edgeFinset \ H.edgeFinset), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), s(x, y) ∉ G.edgeFinset \ H.edgeFinset
⊢ False
have refine : H.IsNClique 3 t
Tactic: refine hH t ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), s(x, y) ∉ G.edgeFinset \ H.edgeFinset
⊢ H.IsNClique 3 t
have h₁ : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), G.Adj x y → H.Adj x y
Tactic: simp only [not_and, mem_sdiff, not_not, mem_edgeFinset, mem_edgeSet] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), G.Adj x y → H.Adj x y
⊢ H.IsNClique 3 t
have obtain : ∀ (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 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1)
      (_ : Membership.mem (γ := Finset α) {x, y, z} y_1) (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1),
  H.IsNClique 3 {x, y, z}
Tactic: obtain ⟨x, y, z, xy, xz, yz, rfl⟩ := is3Clique_iff.1 (mem_cliqueFinset_iff.1 <| htris ht)
Cleared hypotheses: t, ht, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).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 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ H.IsNClique 3 {x, y, z}
have rw : H.Adj x y ∧ H.Adj x z ∧ H.Adj y z
Tactic: rw [is3Clique_triple_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).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 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : 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
have refine_1 : Membership.mem (γ := Finset α) {x, y, z} x
Tactic: refine ⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).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 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
refine_1 : Membership.mem (γ := Finset α) {x, y, z} x
⊢ H.Adj x y ∧ H.Adj x z ∧ H.Adj y z
have refine_2 : Membership.mem (γ := Finset α) {x, y, z} y
Tactic: refine ⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).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 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
refine_1 : Membership.mem (γ := Finset α) {x, y, z} x
refine_2 : Membership.mem (γ := Finset α) {x, y, z} y
refine_3 : Membership.mem (γ := Finset α) {x, y, z} x
⊢ H.Adj x y ∧ H.Adj x z ∧ H.Adj y z
have refine_4 : Membership.mem (γ := Finset α) {x, y, z} z
Tactic: refine ⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
⊢ False
have this : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
this :
  ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset
⊢ False
have choose : ∀ (fx fy : ⦃t : Finset α⦄ → (ht : 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), False
Tactic: choose fx fy hfx hfy hfne fmem using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : 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 : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
⊢ False
have hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
Tactic: have hf (x) (_ : x ∈ tris.attach) : f x ∈ G.edgeFinset \ H.edgeFinset := fmem _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : 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 : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
⊢ False
have obtain : ∀ (t₁ : Finset α) (ht₁ : t₁ ∈ tris) (t₂ : Finset α) (ht₂ : t₂ ∈ tris)
  (tne :
    Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂)
  (t : s(fx sorry, fy sorry) = s(fx sorry, fy sorry)), False
Tactic: obtain ⟨⟨t₁, ht₁⟩, -, ⟨t₂, ht₂⟩, -, tne, t : s(_, _) = s(_, _)⟩ :=
    exists_ne_map_eq_of_card_lt_of_maps_to hG hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : 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 : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
⊢ False
have i : (fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton) t₁ t₂
Tactic: have i := pd ht₁ ht₂ (Subtype.val_injective.ne tne)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : 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 : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
i : (fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton) t₁ t₂
⊢ False
have t₃ : fx sorry = fx sorry ∧ fy sorry = fy sorry ∨ fx sorry = fy sorry ∧ fy sorry = fx sorry
Tactic: rw [Sym2.eq_iff] at t
Cleared hypotheses: t, i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : 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 : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
i : ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton
⊢ False
have inl : ∀ (t : fx sorry = fx sorry ∧ fy sorry = fy sorry), False
Tactic: obtain t | t := t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : 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 : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
i : ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton
inl : ∀ (t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯), False
⊢ False
have inr : ∀ (t : fx sorry = fy sorry ∧ fy sorry = fx sorry), False
Tactic: obtain t | t := t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#tris) : 𝕜)
⊢ G.FarFromTriangleFree ε
have rw : ∀ ⦃H : SimpleGraph α⦄ [inst_6 : DecidableRel H.Adj],
  H ≤ G →
    H.CliqueFree 3 →
      ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤
        HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
Tactic: rw [farFromTriangleFree_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#tris) : 𝕜)
H : SimpleGraph α
inst_6 : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
⊢ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
have rw : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#G.edgeFinset - #H.edgeFinset) : 𝕜)
Tactic: rw [← Nat.cast_sub (card_le_card <| edgeFinset_mono hG)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ε < 2⁻¹
have refine : ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 < 2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2
Tactic: refine lt_of_mul_lt_mul_right (α := 𝕜) (a := Fintype.card α ^ 2) ?_ (by positivity)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ LE.le.{u_3} (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑((Fintype.card α).choose 2) : 𝕜)
have a : #G.edgeFinset ≤ (Fintype.card α).choose 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 <
    2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2
have ε₁ : ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 ≤ (↑(#G.edgeFinset) : 𝕜)
Tactic: calc
        ε * Fintype.card α ^ 2
    _ ≤ #G.edgeFinset := by simpa using hε.le_card_edgeFinset (by simp)
    _ ≤ (Fintype.card α).choose 2 := by gcongr; exact card_edgeFinset_le_card_choose_two
    _ < 2⁻¹ * Fintype.card α ^ 2 := by
      simpa [← div_eq_inv_mul] using Nat.choose_lt_pow_div (by positivity) le_rfl