mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ s(g, h) ∈ {a, b, c}.sym2

Tactic:
simpa using

Goal state after:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ (g = a ∨ g = b ∨ g = c) ∧ (h = a ∨ h = b ∨ h = c)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ s(g, h) ∈ {d, e, f}.sym2

Tactic:
simpa using

Goal state after:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ (g = d ∨ g = e ∨ g = f) ∧ (h = d ∨ h = e ∨ h = f)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G = ⊥

pp: case mpr
α : Type u_1
G : SimpleGraph α
⊢ G = ⊥ → G.CliqueFree 2

Tactic:
· simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]
    exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
⊢ G = ⊥ → G.CliqueFree 2
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (insert x ((t.erase y).erase x)) ∧ G.IsNClique n (t.erase x)

Tactic:
insert_erase <| mem_erase_of_ne_of_mem hne h1

Goal state after:
case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ #(bipartiteBelow (fun s e ↦ e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ ∀ (a : Finset α), G.IsNClique 3 a → e ∈ a.sym2 → ∀ (b : Finset α), G.IsNClique 3 b → e ∈ b.sym2 → a = b
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun e s ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ (x y : α), G.Adj x y → ∃ x_1, G.IsNClique 3 x_1 ∧ x ∈ x_1 ∧ y ∈ x_1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Tactic:
simpa using

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
s : Finset α
⊢ s ∈ G.cliqueFinset n → s ∈ powersetCard n univ

Tactic:
simpa using

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
s : Finset α
⊢ G.IsNClique n s → #s = n
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.bypass.length ≤ p.length

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.bypass.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
h : p.length ≤ p.bypass.length
⊢ p.support.length ≤ p.bypass.support.length

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
h : p.length ≤ p.bypass.length
⊢ p.length ≤ p.bypass.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
w : G.Walk v v
⊢ w.cycleBypass.length ≤ w.length

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
w : G.Walk v v
⊢ w.cycleBypass.length ≤ w.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ (cons hvv' w.bypass).support.tail.Nodup

Tactic:
simpa using

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ w.bypass.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ G.indepNum

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ sSup {n | ∃ s, Gᶜ.IsNClique n s}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
⊢ ∃ s, G.IsNIndepSet G.indepNum s

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Goal state after:
α : Type u_3
G : SimpleGraph α
⊢ ∃ s, Gᶜ.IsNClique (sSup {n | ∃ s, Gᶜ.IsNClique n s}) s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : G.IsMaximumIndepSet t
⊢ #t = G.indepNum

Tactic:
rw [← isMaximumClique_compl] at tmc

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = G.indepNum
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = G.indepNum

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = sSup {n | ∃ s, Gᶜ.IsNClique n s}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ k ≤ k * (n / k)

Tactic:
simpa using

Goal state after:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ k ≤ k * (n / k)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ε * ↑(Fintype.card α) ^ 2 ≤ ↑(#G.edgeFinset)

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ε * ↑(Fintype.card α) ^ 2 ≤ ↑(#G.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ↑((Fintype.card α).choose 2) < 2⁻¹ * ↑(Fintype.card α) ^ 2

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ↑((Fintype.card α).choose 2) < ↑(Fintype.card α) ^ 2 / 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case inl.refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ 0 ≤ ↑(G.edgeDensity U V)

pp: case inl.refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ↑(G.edgeDensity U V) ≤ 1

pp: case inl.refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ε ^ 5 / 50 ≤ ε ^ 5 / 25

Tactic:
· exact mod_cast G.edgeDensity_nonneg _ _

Goal state after:
case inl.refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ↑(G.edgeDensity U V) ≤ 1

case inl.refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ε ^ 5 / 50 ≤ ε ^ 5 / 25
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
x y z : α ⊕ β ⊕ γ
⊢ (graph t).Adj x y →
    (graph t).Adj x z →
      (graph t).Adj y z →
        ∃ a b c,
          {in₀ a, in₁ b, in₂ c} = {x, y, z} ∧
            (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

Tactic:
rintro (_ | _ | _) (_ | _ | _) (_ | _ | _) <;>
    refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
      ?_, ?_, ?_⟩ <;> constructor <;> assumption

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝ a'✝ : α
b✝ b'✝ : β
c✝ c'✝ : γ
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
x✝¹ x✝ : α × β × γ
a : α
b : β
c : γ
a' : α
b' : β
c' : γ
⊢ (fun x ↦ {in₀ x.1, in₁ x.2.1, in₂ x.2.2}) (a, b, c) = (fun x ↦ {in₀ x.1, in₁ x.2.1, in₂ x.2.2}) (a', b', c') →
    (a, b, c) = (a', b', c')

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝ a'✝ : α
b✝ b'✝ : β
c✝ c'✝ : γ
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
x✝¹ x✝ : α × β × γ
a : α
b : β
c : γ
a' : α
b' : β
c' : γ
⊢ (a = a' ∧ b = b' ∧ c = c') ∧ a' = a ∧ b' = b ∧ c' = c → a = a' ∧ b = b' ∧ c = c'
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * (1 - (↑m)⁻¹) ≤ ↑m

Tactic:
← one_div,

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * (1 - 1 / ↑m) ≤ ↑m
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ 1 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ ¬G.CliqueFree 3
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
intro G'

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
G' : SimpleGraph α
⊢ ∀ [inst : DecidableRel G'.Adj],
    G' ≤ G → G'.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#G'.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
    (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
t : ℝ := ↑(G.edgeDensity U V)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ ε ^ 5 / 49
hqt : |q - t| ≤ ε ^ 5 / 49
⊢ ε ^ 5 ≤ ε

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
    (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
t : ℝ := ↑(G.edgeDensity U V)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ ε ^ 5 / 49
hqt : |q - t| ≤ ε ^ 5 / 49
⊢ ε ^ 5 ≤ ε
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : ExplicitDisjoint t
ε : 𝕜
ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑(#t)
x : α × β × γ
hx : x ∈ t
⊢ x ∈ ((graph t).cliqueFinset 3).preimage ⇑toTriangle ⋯

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : ExplicitDisjoint t
ε : 𝕜
ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑(#t)
x : α × β × γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 {Sum.inl x.1, Sum.inr (Sum.inl x.2.1), Sum.inr (Sum.inr x.2.2)}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : ExplicitDisjoint t
ε : 𝕜
ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑(#t)
⊢ ε * ↑(Fintype.card (α ⊕ β ⊕ γ) ^ 2) ≤ ↑(#(map toTriangle t))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : ExplicitDisjoint t
ε : 𝕜
ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑(#t)
⊢ ε * (↑(Fintype.card α) + (↑(Fintype.card β) + ↑(Fintype.card γ))) ^ 2 ≤ ↑(#t)
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
⊢ ∃ x₁ y₁ x₂ y₂, y₁ - x₁ ∈ A ∧ y₂ - x₁ ∈ A ∧ y₁ - x₂ ∈ A ∧ x₁ + y₂ = x₂ + y₁ ∧ x₁ ≠ x₂

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
⊢ ∃ x₁ y₁ x₂ y₂, y₁ - x₁ ∈ A ∧ y₂ - x₁ ∈ A ∧ y₁ - x₂ ∈ A ∧ x₁ + y₂ = x₂ + y₁ ∧ ¬x₁ = x₂
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this✝ : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
this : y₁ - x₂ = y₁ - x₁
⊢ x₁ = x₂

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this✝ : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
this : y₁ - x₂ = y₁ - x₁
⊢ x₁ = x₂
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2 ≤ #u * ∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2 ≤ #u * ∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝ : ↑A = Fin.val '' Nat.cast '' ↑A
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ
hx : x ∈ Set.Iio n
⊢ x < n

Tactic:
simpa using

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝ : ↑A = Fin.val '' Nat.cast '' ↑A
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ
hx : x ∈ Set.Iio n
⊢ x < n