mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ (map d) x₁ % d = x₂ 0

Tactic:
← mod_eq_of_lt (hx₂ _),

Goal state after:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ (map d) x₁ % d = x₂ 0 % d
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A / B) * #(C / B)

Tactic:
rw [← card_product (A / B), ← mul_one #((A / B) ×ˢ (C / B))]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 4096 < rexp 16

Tactic:
by
  rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by simp), show (4096 : ℝ) = 2 ^ 12 by norm_cast,
    ← rpow_natCast, log_rpow zero_lt_two, cast_ofNat]
  linarith [log_two_lt_d9]

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

Goal state before:
pp: case bot.bot
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
f : ⊥ ⟶ ⊥
⊢ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥

Tactic:
exact 𝟙 _

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

Goal state before:
pp: case top.top
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
f : ⊤ ⟶ ⊤
⊢ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤

Tactic:
exact 𝟙 _

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(A * C)) ≤ ↑(#(B * A)) / ↑(#B) * ↑(#(B * C))

Tactic:
card_le_card_mul_left hU.1,

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(U * (A * C))) ≤ ↑(#(B * A)) / ↑(#B) * ↑(#(B * C))
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B⁻¹ ≤ #(A * B⁻¹) * #(B⁻¹ * C)

Tactic:
exact ruzsa_triangle_inequality_mul_mul_mul _ _ _

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(B * C⁻¹)

Tactic:
exact ruzsa_triangle_inequality_mul_mul_mul _ _ _

Goal state after:
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ #(x⁻¹ •> s •> A ∩ B⁻¹) = #((x⁻¹ * s⁻¹⁻¹) •> A ∩ B⁻¹)

Tactic:
inv_inv,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ #(x⁻¹ •> s •> A ∩ B⁻¹) = #((x⁻¹ * s) •> A ∩ B⁻¹)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A ^ 2)) ≤ K * ↑(#A)

Tactic:
calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case h₂
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A ^ 2)) ≤ K * ↑(#A)

Tactic:
calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d : G.Dart
⊢ G.dartOfNeighborSet d.toProd.1 ⟨d.toProd.2, ⋯⟩ = d

Tactic:
by ext <;> rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
⊢ ∀ ⦃v₂ : ↑u⦄, v₂ ∈ u ↓∩ t → (SimpleGraph.induce u G).Adj v₁✝ v₂

Tactic:
_

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
v₂✝ : ↑u
⊢ v₂✝ ∈ u ↓∩ t → (SimpleGraph.induce u G).Adj v₁✝ v₂✝
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
⊢ (⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f

Tactic:
by
  rintro a ha b hb hab
  simp_rw [Set.mem_iUnion] at ha hb
  obtain ⟨c, hc, ha⟩ := ha
  obtain ⟨d, hd, hb⟩ := hb
  obtain hcd | hcd := eq_or_ne (g c) (g d)
  · exact hg d hd (by rwa [hcd] at ha) hb hab
  · exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
⊢ (↑e).symm x✝¹ ∉ Finset.map (↑e).symm.toEmbedding u

Tactic:
simp [hbu]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr.inl
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
h✝ : Nonempty V
inst✝ : DecidablePred fun x ↦ x ∈ ∅
h : G.support ⊆ ∅
⊢ G.minDegree ≤ (induce ∅ G).minDegree

pp: case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
⊢ G.minDegree ≤ (induce s G).minDegree

Tactic:
· simp [minDegree_eq_zero_iff_support_ne, Set.subset_empty_iff.mp h, Set.empty_ne_univ]

Goal state after:
case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
⊢ G.minDegree ≤ (induce s G).minDegree
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
hx : x✝ ∈ ↑P.parts
⊢ ∀ ⦃y : α⦄, y ∈ ↑P.parts → x✝ ≠ y → (Disjoint on f) x✝ y

Tactic:
_

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
hx : x✝ ∈ ↑P.parts
y✝ : α
⊢ y✝ ∈ ↑P.parts → x✝ ≠ y✝ → (Disjoint on f) x✝ y✝
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∑ p ∈ parts.erase ⊥, f p = ∑ p ∈ parts, f p

Tactic:
← erase_union_eq ⊥ parts hbot,

Goal state after:
case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∑ p ∈ (parts.erase ⊥ ∪ {⊥}).erase ⊥, f p = ∑ p ∈ parts.erase ⊥ ∪ {⊥}, f p
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝ : α
⊢ a✝ ∈ x → ∀ a ∈ x, ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝ x_3 → x_3 ∈ x → s a x_3 → (s a✝ x_1 ↔ s a x_1)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝¹ : α
a✝ : a✝¹ ∈ x
⊢ ∀ a ∈ x, ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝¹ x_3 → x_3 ∈ x → s a x_3 → (s a✝¹ x_1 ↔ s a x_1)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝¹ : α
a✝ : a✝¹ ∈ x
⊢ ∀ a ∈ x, ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝¹ x_3 → x_3 ∈ x → s a x_3 → (s a✝¹ x_1 ↔ s a x_1)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝² : α
a✝¹ : a✝² ∈ x
a✝ : α
⊢ a✝ ∈ x → ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝² x_3 → x_3 ∈ x → s a✝ x_3 → (s a✝² x_1 ↔ s a✝ x_1)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝² : α
a✝¹ : a✝² ∈ x
a✝ : α
⊢ a✝ ∈ x → ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝² x_3 → x_3 ∈ x → s a✝ x_3 → (s a✝² x_1 ↔ s a✝ x_1)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
⊢ ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝³ x_3 → x_3 ∈ x → s a✝¹ x_3 → (s a✝³ x_1 ↔ s a✝¹ x_1)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
⊢ ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝³ x_3 → x_3 ∈ x → s a✝¹ x_3 → (s a✝³ x_1 ↔ s a✝¹ x_1)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝ : α
⊢ x✝ ∈ x → ∀ x_2 ∈ x, s a✝³ x_2 → x_2 ∈ x → s a✝¹ x_2 → (s a✝³ x✝ ↔ s a✝¹ x✝)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝ : α
⊢ x✝ ∈ x → ∀ x_2 ∈ x, s a✝³ x_2 → x_2 ∈ x → s a✝¹ x_2 → (s a✝³ x✝ ↔ s a✝¹ x✝)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝¹ : α
x✝ : x✝¹ ∈ x
⊢ ∀ x_1 ∈ x, s a✝³ x_1 → x_1 ∈ x → s a✝¹ x_1 → (s a✝³ x✝¹ ↔ s a✝¹ x✝¹)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝¹ : α
x✝ : x✝¹ ∈ x
⊢ ∀ x_1 ∈ x, s a✝³ x_1 → x_1 ∈ x → s a✝¹ x_1 → (s a✝³ x✝¹ ↔ s a✝¹ x✝¹)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝² : α
x✝¹ : x✝² ∈ x
x✝ : α
⊢ x✝ ∈ x → s a✝³ x✝ → x✝ ∈ x → s a✝¹ x✝ → (s a✝³ x✝² ↔ s a✝¹ x✝²)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝² : α
x✝¹ : x✝² ∈ x
x✝ : α
⊢ x✝ ∈ x → s a✝³ x✝ → x✝ ∈ x → s a✝¹ x✝ → (s a✝³ x✝² ↔ s a✝¹ x✝²)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝³ : α
x✝² : x✝³ ∈ x
x✝¹ : α
x✝ : x✝¹ ∈ x
⊢ s a✝³ x✝¹ → x✝¹ ∈ x → s a✝¹ x✝¹ → (s a✝³ x✝³ ↔ s a✝¹ x✝³)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝³ : α
x✝² : x✝³ ∈ x
x✝¹ : α
x✝ : x✝¹ ∈ x
ha : s a✝³ x✝¹
⊢ x✝¹ ∈ x → s a✝¹ x✝¹ → (s a✝³ x✝³ ↔ s a✝¹ x✝³)

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝³ : α
a✝² : a✝³ ∈ x
a✝¹ : α
a✝ : a✝¹ ∈ x
x✝⁴ : α
x✝³ : x✝⁴ ∈ x
x✝² : α
x✝¹ : x✝² ∈ x
ha : s a✝³ x✝²
x✝ : x✝² ∈ x
⊢ s a✝¹ x✝² → (s a✝³ x✝⁴ ↔ s a✝¹ x✝⁴)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x✝ : Finset α
inst✝ : DecidableRel ⇑s
x : α
⊢ x ∈ x✝ → ∃ x₂ ∈ x✝, s x x₂

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x✝ : Finset α
inst✝ : DecidableRel ⇑s
x : α
a✝ : x ∈ x✝
⊢ ∃ x₂ ∈ x✝, s x x₂
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case h
α : 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, ⋯⟩
bij : Function.Bijective z'
a b : ↥s
⊢ (f a).fst = (f b).fst ↔ ↑(g (f a).fst) = ↑(g (f b).fst)

Tactic:
Fin.val_eq_val,

Goal state after:
case h
α : 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, ⋯⟩
bij : Function.Bijective z'
a b : ↥s
⊢ (f a).fst = (f b).fst ↔ g (f a).fst = g (f b).fst
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case top
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✝ b : EInt
X✝ X : C
⊢ IsIso ((t.eTruncLTGELTSelfToGELT ⊤ b).app X)

Tactic:
exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _,
      IsZero.eq_of_src (by simp) _ _⟩

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
obtain ⟨U, hU, hx⟩ := P.exists_mem hx

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ #({x ∈ P.parts.attach | #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) * ?m.162 +
      #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) * ?m.168 =
    stepBound #P.parts

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∀ x ∈ univ, #(equitabilise ⋯).parts = ?m.168

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ℕ

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∀ x ∈ univ, #(equitabilise ⋯).parts = ?m.162

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ℕ

Tactic:
any_goals exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ #({x ∈ P.parts.attach | #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) *
        (4 ^ #P.parts - (Fintype.card α / #P.parts - m * 4 ^ #P.parts) +
          (Fintype.card α / #P.parts - m * 4 ^ #P.parts)) +
      #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) *
        (4 ^ #P.parts - (Fintype.card α / #P.parts - m * 4 ^ #P.parts + 1) +
          (Fintype.card α / #P.parts - m * 4 ^ #P.parts + 1)) =
    stepBound #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr.inr.succ
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))

Tactic:
by_cases huniform : P.IsUniform G ε

Goal state after:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
huniform : P.IsUniform G ε
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))

case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
huniform : ¬P.IsUniform G ε
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : ↑s
⊢ (induce s (G.deleteIncidenceSet x)).Adj v₁ v₂ ↔ (induce s G).Adj v₁ v₂

Tactic:
simp_rw [comap_adj, Function.Embedding.coe_subtype, deleteIncidenceSet_adj, and_iff_left_iff_imp]

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : ↑s
⊢ G.Adj ↑v₁ ↑v₂ → ↑v₁ ≠ x ∧ ↑v₂ ≠ x
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1

Tactic:
simp_rw [← Set.card_singleton x, ← Set.toFinset_card, ← card_sdiff_of_subset hx,
    ← Set.toFinset_sdiff]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ #(G.deleteIncidenceSet x).support.toFinset ≤ #(G.support \ {x}).toFinset
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
⊢ ∀ {v w : W}, Relation.Map H.Adj (⇑f) (⇑f) v w → v ∈ ⇑f '' H.verts

Tactic:
rintro _ _ ⟨u, v, h, rfl, rfl⟩
    exact Set.mem_image_of_mem _ (H.edge_vert h)

Goal state after: