mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ a ⊔ b = c

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ a ⊔ b = c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b✝ c : α
P : Finpartition a
b : α
⊢ a \ b = a \ b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d ≤ b ↔ ¬d ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ #P.parts * (4 * 4) ^ #P.parts ≤ Fintype.card α

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ #P.parts * (4 * 4) ^ #P.parts ≤ Fintype.card α
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts - Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 1 ≤ 4 ^ #P.parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts - Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 1 ≤ 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts ≤ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 4 ^ #P.parts - 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts ≤ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 4 ^ #P.parts - 1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ id a → a_1 ∉ id b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ id a → a_1 ∉ id b
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hucard : #u = m * 4 ^ #P.parts + a
⊢ m * 4 ^ #P.parts + a = m * 4 ^ #P.parts + a

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts ≤ Fintype.card α / #P.parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ Fintype.card α / #P.parts
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ Fintype.card α / #P.parts
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #P.parts * (#s / #P.parts) + #s % #P.parts

Tactic:
]

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #P.parts * (#s / #P.parts) + #s % #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ Fintype.card α / #P.parts
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ Fintype.card α / #P.parts + 1 = Fintype.card α / #P.parts + 1

Tactic:
]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a e : α
p : Finset α
mp : p ∈ P.parts
f : α
mf : f ∈ p
⊢ e ∈ p ↔ e ∈ p

Tactic:
]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = ∑ u ∈ P.parts, #(id u)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = ∑ u ∈ P.parts, #(id u)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ (⇑{ toFun := singleton, inj' := ⋯ } '' ↑s).PairwiseDisjoint id

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ (⇑{ toFun := singleton, inj' := ⋯ } '' ↑s).PairwiseDisjoint id
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P✝ : Finpartition s✝
a : α
s : Finset α
P : Finpartition s
t : Finset α
ht : ∃ a ∈ s, {a} = t
⊢ ∃ c ∈ P.parts, t ⊆ c

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P✝ : Finpartition s✝
a : α
s : Finset α
P : Finpartition s
t : Finset α
ht : ∃ a ∈ s, {a} = t
⊢ ∃ c ∈ P.parts, t ⊆ c
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * (Fintype.card α / #P.parts / 4 ^ #P.parts) ≤ #u

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * (Fintype.card α / #P.parts / 4 ^ #P.parts) ≤ #u
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #P.parts ≤ #⊥.parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #P.parts ≤ #⊥.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % 0 ≤ 0

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % 0 ≤ 0
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ #s % 0 ≤ 0

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ #s % 0 ≤ 0
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ 0 % 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < max (↑7) (max ↑l ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5

Tactic:
]

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < max (↑7) (max ↑l ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = x
y : Finset α
hy : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = y
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
⊢ x = y

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = x
y : Finset α
hy : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = y
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
⊢ x = y
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
a b : ↥s
this : NeZero #P.parts
e : (f a).snd.1 = (f b).snd.1 ∧ (f a).fst = (f b).fst
⊢ #↑(f b).fst = #↑(f b).fst

Tactic:
]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ Q
⊢ i ∈ Q

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ Q
⊢ i ∈ Q
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ R
⊢ i ∈ R

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ R
⊢ i ∈ R
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t
⊢ id t ⊆ s

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t
⊢ id t ⊆ s
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ ∃ i ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset, a ∈ id i

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ ∃ i ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset, a ∈ id i
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ F ∧ a ∈ t ↔ a ∈ t

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ F ∧ a ∈ t ↔ a ∈ t
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
⊢ x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|

Tactic:
]

Goal state after:
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
⊢ x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ b ∈ t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ b ∈ t
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a : EInt
X : C
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a : EInt
X : C
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ a ∈ t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ a ∈ t
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ 2 ^ (#F - 1) ≤ 2 ^ (#F - 1)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} →
      x ∈ image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} →
      x ∈ image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2 ≤ ((∑ x ∈ s, f x) / ↑(#s) - (∑ j ∈ t, f j) / ↑(#t)) ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
⊢ ∀ (X : C), IsIso ((t.eTruncGEToGEGE a b).app X)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
⊢ ∀ (X : C), IsIso ((t.eTruncGEToGEGE a b).app X)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
]

Goal state after:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : b ≤ a
⊢ ∀ (X : C), IsIso ((t.eTruncLTLTToLT a b).app X)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : b ≤ a
⊢ ∀ (X : C), IsIso ((t.eTruncLTLTToLT a b).app X)
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ {s}.EquitableOn Finset.card

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ {s}.EquitableOn Finset.card