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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₀ (a, b, c).1)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₀ (a, b, c).1)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c

Tactic:
;

Goal state after:
case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₂ (a, b, c).2.2)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₂ (a, b, c).2.2)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, ?b, (a, b, c).2.2) ∈ t

pp: case b
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ β

Tactic:
;

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, ?b, (a, b, c).2.2) ∈ t

case b
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ β
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a

Tactic:
;

Goal state after:
case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : ε / 4 ≤ 1
⊢ 0 ≤ 1 - 2 * (ε / 8)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : ε / 4 ≤ 1
⊢ 0 ≤ 1 - 2 * (ε / 8)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₀ (a, b, c).1)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₀ (a, b, c).1)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c

Tactic:
;

Goal state after:
case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₂ (a, b, c).2.2)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₂ (a, b, c).2.2)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (?a, (a, b, c).2.1, (a, b, c).2.2) ∈ t

pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ α

Tactic:
;

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (?a, (a, b, c).2.1, (a, b, c).2.2) ∈ t

case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ α
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b

Tactic:
;

Goal state after:
case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₁ (a, b, c).2.1)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₁ (a, b, c).2.1)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case hbc
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ triangleRemovalBound ε ≤ (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3

Tactic:
;

Goal state after:
case hbc
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ triangleRemovalBound ε ≤ (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3431, in₁ ?m.3434, in₂ ?m.3437} ↔ a✝ ∈ {in₀ a✝⁵, in₁ b✝¹, in₂ c✝}

Tactic:
;

Goal state after:
α : 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
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3431, in₁ ?m.3434, in₂ ?m.3437} ↔ a✝ ∈ {in₀ a✝⁵, in₁ b✝¹, in₂ c✝}
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3431 ∨ a✝ = in₁ ?m.3434 ∨ a✝ = in₂ ?m.3437 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝

Tactic:
;

Goal state after:
α : 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
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3431 ∨ a✝ = in₁ ?m.3434 ∨ a✝ = in₂ ?m.3437 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3588, in₁ ?m.3591, in₂ ?m.3594} ↔ a✝ ∈ {in₁ b✝¹, in₀ a✝⁵, in₂ c✝}

Tactic:
;

Goal state after:
α : 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
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3588, in₁ ?m.3591, in₂ ?m.3594} ↔ a✝ ∈ {in₁ b✝¹, in₀ a✝⁵, in₂ c✝}
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3588 ∨ a✝ = in₁ ?m.3591 ∨ a✝ = in₂ ?m.3594 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝

Tactic:
;

Goal state after:
α : 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
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3588 ∨ a✝ = in₁ ?m.3591 ∨ a✝ = in₂ ?m.3594 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case hbc
α : 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ε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
⊢ ↑(G.edgeDensity U V) ≤ 1

Tactic:
;

Goal state after:
case hbc
α : 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ε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
⊢ ↑(G.edgeDensity U V) ≤ 1
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3745, in₁ ?m.3748, in₂ ?m.3751} ↔ a✝ ∈ {in₀ a✝⁵, in₂ c✝¹, in₁ b✝}

Tactic:
;

Goal state after:
α : 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
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3745, in₁ ?m.3748, in₂ ?m.3751} ↔ a✝ ∈ {in₀ a✝⁵, in₂ c✝¹, in₁ b✝}
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3745 ∨ a✝ = in₁ ?m.3748 ∨ a✝ = in₂ ?m.3751 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝

Tactic:
;

Goal state after:
α : 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
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3745 ∨ a✝ = in₁ ?m.3748 ∨ a✝ = in₂ ?m.3751 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3902, in₁ ?m.3905, in₂ ?m.3908} ↔ a✝ ∈ {in₂ c✝¹, in₀ a✝⁵, in₁ b✝}

Tactic:
;

Goal state after:
α : 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
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3902, in₁ ?m.3905, in₂ ?m.3908} ↔ a✝ ∈ {in₂ c✝¹, in₀ a✝⁵, in₁ b✝}
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3902 ∨ a✝ = in₁ ?m.3905 ∨ a✝ = in₂ ?m.3908 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝

Tactic:
;

Goal state after:
α : 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
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3902 ∨ a✝ = in₁ ?m.3905 ∨ a✝ = in₂ ?m.3908 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝³, b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.4059, in₁ ?m.4062, in₂ ?m.4065} ↔ a✝ ∈ {in₁ b✝¹, in₂ c✝¹, in₀ a✝³}

Tactic:
;

Goal state after:
α : 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
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝³, b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.4059, in₁ ?m.4062, in₂ ?m.4065} ↔ a✝ ∈ {in₁ b✝¹, in₂ c✝¹, in₀ a✝³}
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝³, b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4059 ∨ a✝ = in₁ ?m.4062 ∨ a✝ = in₂ ?m.4065 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝³

Tactic:
;

Goal state after:
α : 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
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝³, b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4059 ∨ a✝ = in₁ ?m.4062 ∨ a✝ = in₂ ?m.4065 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝³
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.4216, in₁ ?m.4219, in₂ ?m.4222} ↔ a✝ ∈ {in₂ c✝¹, in₁ b✝¹, in₀ a✝³}

Tactic:
;

Goal state after:
α : 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
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.4216, in₁ ?m.4219, in₂ ?m.4222} ↔ a✝ ∈ {in₂ c✝¹, in₁ b✝¹, in₀ a✝³}
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 γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4216 ∨ a✝ = in₁ ?m.4219 ∨ a✝ = in₂ ?m.4222 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝³

Tactic:
;

Goal state after:
α : 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
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4216 ∨ a✝ = in₁ ?m.4219 ∨ a✝ = in₂ ?m.4222 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝³
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hst : Disjoint s t
hsu : Disjoint s u
htu : Disjoint t u
x₁ x₂ y₁ y₂ z₁ z₂ : α
h : {x₁, y₁, z₁} = {x₂, y₂, z₂}
hx₁ : x₁ ∈ s
hx₂ : x₂ ∈ s
hy₁ : y₁ ∈ t
hy₂ : y₂ ∈ t
hz₁ : z₁ ∈ u
hz₂ : z₂ ∈ u
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)

Tactic:
simp only [Finset.Subset.antisymm_iff, subset_iff, mem_insert, mem_singleton, forall_eq_or_imp,
    forall_eq] at h

Goal state after:
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hst : Disjoint s t
hsu : Disjoint s u
htu : Disjoint t u
x₁ x₂ y₁ y₂ z₁ z₂ : α
hx₁ : x₁ ∈ s
hx₂ : x₂ ∈ s
hy₁ : y₁ ∈ t
hy₂ : y₂ ∈ t
hz₁ : z₁ ∈ u
hz₂ : z₂ ∈ u
h :
  ((x₁ = x₂ ∨ x₁ = y₂ ∨ x₁ = z₂) ∧ (y₁ = x₂ ∨ y₁ = y₂ ∨ y₁ = z₂) ∧ (z₁ = x₂ ∨ z₁ = y₂ ∨ z₁ = z₂)) ∧
    (x₂ = x₁ ∨ x₂ = y₁ ∨ x₂ = z₁) ∧ (y₂ = x₁ ∨ y₂ = y₁ ∨ y₂ = z₁) ∧ (z₂ = x₁ ∨ z₂ = y₁ ∨ z₂ = z₁)
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case a
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ {x ∈ univ ×ˢ univ |
      match x with
      | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y} ⊆
    A ∪ B ∪ C

Tactic:
;

Goal state after:
case a
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ {x ∈ univ ×ˢ univ |
      match x with
      | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y} ⊆
    A ∪ B ∪ C
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#(A ∪ B)) ≤ ↑(#A) + ↑(#B)

Tactic:
;

Goal state after:
case h₁
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#(A ∪ B)) ≤ ↑(#A) + ↑(#B)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case bc
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#A) < 4 * (ε / 8) * ↑(Fintype.card α) ^ 2

Tactic:
;

Goal state after:
case bc
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#A) < 4 * (ε / 8) * ↑(Fintype.card α) ^ 2
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
A✝ : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
A : Finset (G × G)
x₁ x₂ : G
⊢ (x₁, x₂) = (x₁, x₂)

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
A✝ : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
A : Finset (G × G)
x₁ x₂ : G
⊢ (x₁, x₂) = (x₁, x₂)