mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case ha
α : 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(A.sup id)

pp: case hb
α : 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(B.sup id)

Tactic:
<;>

Goal state after:
case ha
α : 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(A.sup id)

case hb
α : 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(B.sup id)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} 0 ↔ 1 < 0

pp: case succ.zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} (0 + 1) ↔ 1 < 0 + 1

pp: case succ.succ
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} (n + 1 + 1) ↔ 1 < n + 1 + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} 0 ↔ 1 < 0

case succ.zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} (0 + 1) ↔ 1 < 0 + 1

case succ.succ
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} (n + 1 + 1) ↔ 1 < n + 1 + 1
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.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ s(a, b) ≠ s(a, c)

pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ s(a, b) ≠ s(b, c)

pp: case refine_3
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ s(a, c) ≠ s(b, c)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ s(a, b) ≠ s(a, c)

case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ s(a, b) ≠ s(b, c)

case refine_3
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ s(a, c) ≠ s(b, c)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ a ∈ ↑{a, b}

pp: case refine_2.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ b ∈ ↑{a, b}

Tactic:
<;>

Goal state after:
case refine_2.refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ a ∈ ↑{a, b}

case refine_2.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ b ∈ ↑{a, b}
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
⊢ (if hs : u✝ ∈ p'.bypass.support then p'.bypass.dropUntil u✝ hs else cons h✝ p'.bypass).IsPath

Tactic:
split_ifs with hs

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u✝ hs).IsPath

case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∉ p'.bypass.support
⊢ (cons h✝ p'.bypass).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
hp : Walk.nil.IsPath
⊢ Walk.nil.bypass = Walk.nil

pp: case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.IsPath → p✝.bypass = p✝
hp : (cons h✝ p✝).IsPath
⊢ (cons h✝ p✝).bypass = cons h✝ p✝

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
hp : Walk.nil.IsPath
⊢ Walk.nil.bypass = Walk.nil

case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.IsPath → p✝.bypass = p✝
hp : (cons h✝ p✝).IsPath
⊢ (cons h✝ p✝).bypass = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : ε ≤ 0
⊢ min (2 * ↑0 ^ 3)⁻¹ ((1 - min 1 ε / 4) * (ε / (16 * ↑(bound (ε / 8) 0))) ^ 3) ≤ 0

pp: ε : ℝ
hε : ε ≤ 0
⊢ 0 ≤ 4

Tactic:
<;>

Goal state after:
ε : ℝ
hε : ε ≤ 0
⊢ min (2 * ↑0 ^ 3)⁻¹ ((1 - min 1 ε / 4) * (ε / (16 * ↑(bound (ε / 8) 0))) ^ 3) ≤ 0

ε : ℝ
hε : ε ≤ 0
⊢ 0 ≤ 4
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₁ b✝) (in₀ a✝¹)

pp: case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₀ a✝¹) (in₁ b✝)

pp: case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₂ c✝) (in₀ a✝¹)

pp: case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₀ a✝¹) (in₂ c✝)

pp: case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₂ c✝) (in₁ b✝)

pp: case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₁ b✝) (in₂ c✝)

Tactic:
<;>

Goal state after:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₁ b✝) (in₀ a✝¹)

case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₀ a✝¹) (in₁ b✝)

case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₂ c✝) (in₀ a✝¹)

case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₀ a✝¹) (in₂ c✝)

case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₂ c✝) (in₁ b✝)

case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₁ b✝) (in₂ c✝)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₀ a✝¹ ∈ toTriangle z ∧ in₁ b✝ ∈ toTriangle z

pp: case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₁ b✝ ∈ toTriangle z ∧ in₀ a✝¹ ∈ toTriangle z

pp: case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₀ a✝¹ ∈ toTriangle z ∧ in₂ c✝ ∈ toTriangle z

pp: case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₂ c✝ ∈ toTriangle z ∧ in₀ a✝¹ ∈ toTriangle z

pp: case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₁ b✝ ∈ toTriangle z ∧ in₂ c✝ ∈ toTriangle z

pp: case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₂ c✝ ∈ toTriangle z ∧ in₁ b✝ ∈ toTriangle z

Tactic:
<;>

Goal state after:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₀ a✝¹ ∈ toTriangle z ∧ in₁ b✝ ∈ toTriangle z

case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₁ b✝ ∈ toTriangle z ∧ in₀ a✝¹ ∈ toTriangle z

case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₀ a✝¹ ∈ toTriangle z ∧ in₂ c✝ ∈ toTriangle z

case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₂ c✝ ∈ toTriangle z ∧ in₀ a✝¹ ∈ toTriangle z

case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₁ b✝ ∈ toTriangle z ∧ in₂ c✝ ∈ toTriangle z

case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ ∃ z ∈ t, in₂ c✝ ∈ toTriangle z ∧ in₁ b✝ ∈ toTriangle z
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: case inj₀
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c a' : G⦄, (a, b, c) ∈ triangleIndices A → (a', b, c) ∈ triangleIndices A → a = a'

pp: case inj₁
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c b' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b', c) ∈ triangleIndices A → b = b'

pp: case inj₂
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c c' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b, c') ∈ triangleIndices A → c = c'

Tactic:
<;>

Goal state after:
case inj₀
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c a' : G⦄, (a, b, c) ∈ triangleIndices A → (a', b, c) ∈ triangleIndices A → a = a'

case inj₁
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c b' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b', c) ∈ triangleIndices A → b = b'

case inj₂
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c c' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b, c') ∈ triangleIndices A → c = c'
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ ↑(#(G.cliqueFinset 3))

pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ ↑(Fintype.card α) ^ 3

Tactic:
<;>

Goal state after:
case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ ↑(#(G.cliqueFinset 3))

α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ ↑(Fintype.card α) ^ 3
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: case e'_3
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 =
    triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3

pp: case e'_4
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ 1 * ↑(Fintype.card G) ^ 2 = ↑(Fintype.card (G × G))

Tactic:
<;>

Goal state after:
case e'_3
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 =
    triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3

case e'_4
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ 1 * ↑(Fintype.card G) ^ 2 = ↑(Fintype.card (G × G))
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: case e'_3
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 =
    triangleRemovalBound (ε / 9) * (↑(Fintype.card G) + (↑(Fintype.card G) + ↑(Fintype.card G))) ^ 3

pp: case e'_4
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ ↑(Fintype.card G) ^ 2 = ↑(Fintype.card G) * ↑(Fintype.card G)

Tactic:
<;>

Goal state after:
case e'_3
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 =
    triangleRemovalBound (ε / 9) * (↑(Fintype.card G) + (↑(Fintype.card G) + ↑(Fintype.card G))) ^ 3

case e'_4
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ ↑(Fintype.card G) ^ 2 = ↑(Fintype.card G) * ↑(Fintype.card G)
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑(t \ u) ⊆ s

pp: case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑(u \ t) ⊆ s

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑(t \ u) ⊆ s

case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑(u \ t) ⊆ s
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑t \ ↑u ⊆ s

pp: case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑u \ ↑t ⊆ s

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑t \ ↑u ⊆ s

case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑u \ ↑t ⊆ s
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
⊢ Pi.single a 1 a = -1 ∨ Pi.single a 1 a = 0 ∨ Pi.single a 1 a = 1

pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
hab : a ≠ b
⊢ Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
⊢ Pi.single a 1 a = -1 ∨ Pi.single a 1 a = 0 ∨ Pi.single a 1 a = 1

case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
hab : a ≠ b
⊢ Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝ : a ∈ t
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

pp: case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝ : a ∉ t
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝ : a ∈ t
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝ : a ∉ t
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1