mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

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

Tactic:
exact 0

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

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

Tactic:
exact 0

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

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

Tactic:
exact 0

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

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

Tactic:
exact 0

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

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
⊢ Nonempty (Abelian.AbelianStruct f₁)

Tactic:
obtain ⟨X₃, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map f₁)

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
⊢ Nonempty (Abelian.AbelianStruct f₁)
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree ↑{a}

Tactic:
coe_singleton

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree {a}
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
⊢ ThreeAPFree ↑(sphere n d k)

Tactic:
by
  set f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
    { toFun := fun f => toLp 2 (((↑) : ℕ → ℝ) ∘ f)
      map_zero' := PiLp.ext fun _ => cast_zero
      map_add' := fun _ _ => PiLp.ext fun _ => cast_add _ _ }
  refine ThreeAPFree.of_image (AddHomClass.isAddFreimanHom f (Set.mapsTo_image _ _))
    ((toLp_injective 2).comp_injOn cast_injective.comp_left.injOn) (Set.subset_univ _) ?_
  refine (threeAPFree_sphere 0 (√↑k)).mono (Set.image_subset_iff.2 fun x => ?_)
  rw [Set.mem_preimage, mem_sphere_zero_iff_norm]
  exact norm_of_mem_sphere

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
⊢ ↑(#F) * ↑(#B) ≤ K * ↑(#B)

Tactic:
calc
      (#F * #B : ℝ) = #(F * B) := by
        rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
      _ ≤ #(A * B) := by gcongr
      _ ≤ K * #B := hK

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N

Tactic:
apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans

Goal state after:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
⊢ (↑N ^ (↑(nValue N))⁻¹) ^ ↑(nValue N) ≤ ↑N
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case bot.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 0

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

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

Tactic:
exact 0

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

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

Tactic:
exact 0

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

Goal state before:
pp: case top.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 0

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

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

Tactic:
exact 0

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
⊢ #(A <• s ∩ x •> B⁻¹) = #(A ∩ x •> B⁻¹ <• s⁻¹)

Tactic:
simp [← card_smul_finset (op s) (A ∩ _), smul_finset_inter]

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

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

Tactic:
by
  rw [← card_inv]
  simpa [mul_assoc] using small_pos_neg_neg_mul (A := A) (K := K) (by simpa)

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

Goal state before:
pp: case h.mpr
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)) → ∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝

Tactic:
· intro ⟨e, hadj, he⟩
    induction e
    rw [Embedding.sym2Map_apply, Sym2.map_mk, Sym2.eq_iff] at he
    exact he.elim (fun ⟨h, h'⟩ ↦ ⟨_, _, hadj, h, h'⟩) (fun ⟨h', h⟩ ↦ ⟨_, _, hadj.symm, h, h'⟩)

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
⊢ #univ = 2 * #G.edgeFinset

Tactic:
rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h =>
      by rw [mem_coe, mem_edgeFinset]; apply Dart.edge_mem]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, #{a | a.edge = b} = 2 * #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.minDegree = Fintype.card V - 1

Tactic:
exact IsRegularOfDegree.top.minDegree_eq

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

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).sup id = a

Tactic:
sup_image,

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (P.parts ×ˢ Q.parts).sup (id ∘ fun bc ↦ bc.1 ⊓ bc.2) = a
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b✝ c : α
P : Finpartition a
b : α
⊢ (image (fun x ↦ x \ b) P.parts).sup id = a \ b

Tactic:
sup_image,

Goal state after:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b✝ c : α
P : Finpartition a
b : α
⊢ P.parts.sup (id ∘ fun x ↦ x \ b) = a \ b
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:
rw [(hP.card_parts_eq_average hu).resolve_left hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
    Nat.sub_add_cancel a_add_one_le_four_pow_parts_card, ← add_assoc, mul_comm,
    Nat.add_sub_of_le this, card_univ]

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 : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ a ∈ (image (fun a ↦ {b ∈ x | s a b}) x).sup id ↔ a ∈ x

Tactic:
sup_image,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ a ∈ x.sup (id ∘ fun a ↦ {b ∈ x | s a b}) ↔ a ∈ x
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 : t ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset
⊢ id t ⊆ s

Tactic:
rw [mem_image] at ht
        obtain ⟨A, _, rfl⟩ := ht
        exact s.filter_subset _

Goal state after:
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)
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
have htcard : (0 : 𝕜) < #t := hscard.trans_le (Nat.cast_le.2 (card_le_card hst))

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)
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)
Module: Mathlib.Order.Partition.Equipartition

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

Tactic:
coe_singleton

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ {s}.EquitableOn Finset.card
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
obtain rfl | m_pos := m.eq_zero_or_pos

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = 0 ∨ #x = 0 + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ 0) ∧ #({i ∈ Q.parts | #i = 0 + 1}) = b

case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
m_pos : m > 0
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a ∈ P.parts, #(interedges r a t) = ∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)

Tactic:
congr

Goal state after:
case e_f
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ (fun a ↦ #(interedges r a t)) = fun x ↦ ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : (U, V) ∈ P.sparsePairs G ε
⊢ ↑(#(G.interedges (U, V).1 (U, V).2)) ≤ ε * (↑(#(U, V).1) * ↑(#(U, V).2))

Tactic:
simp only [mk_mem_sparsePairs, ne_eq, ← card_interedges_div_card, Rat.cast_div,
      Rat.cast_natCast, Rat.cast_mul] at hUV

Goal state after:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V ∧ ↑(#(G.interedges U V)) / (↑(#U) * ↑(#V)) < ε
⊢ ↑(#(G.interedges (U, V).1 (U, V).2)) ≤ ε * (↑(#(U, V).1) * ↑(#(U, V).2))
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)}) +
        #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)})) *
      4 ^ #P.parts =
    stepBound #P.parts

Tactic:
congr

Goal state after:
case e_a
α : 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)}) +
      #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) =
    #P.parts
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
⊢ #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - G.degree x

Tactic:
by
  simp_rw [← card_incidenceFinset_eq_degree, ← card_sdiff_of_subset (G.incidenceFinset_subset x),
    edgeFinset_deleteIncidenceSet_eq_sdiff]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ #{G' | Nonempty (H ≃g G'.coe)} = #(image Copy.toSubgraph univ)

Tactic:
congr

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ {G' | Nonempty (H ≃g G'.coe)} = image Copy.toSubgraph univ
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
G' : G.Subgraph
inst✝ : Fintype ↑G'.verts
h : G'.IsSpanning
⊢ Finset.univ.card = Fintype.card V

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(equitabilise h).parts = a + b

Tactic:
← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #({x ∈ (equitabilise h).parts | #x = m ∨ #x = m + 1}) = a + b
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅

Tactic:
by
  ext
  simp [hv.symm, hw.symm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj h).support ↔ x✝ ∈ {u, v}

Tactic:
rw [Subgraph.mem_support]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, (G.subgraphOfAdj h).Adj x✝ w) ↔ x✝ ∈ {u, v}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s

Tactic:
intro h' hs
    exact h' _ hs rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
⊢ p.append ((cons h nil).append q) = p.append (cons h q)

Tactic:
cons_nil_append

Goal state after:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
⊢ p.append (cons h q) = p.append (cons h q)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl,

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert (p.length + 1 - i)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat (p.concat h).reverse ≍ concatRecAux Hnil Hconcat (cons ⋯ p.reverse)

Tactic:
congr

Goal state after:
case e_8
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).reverse = cons ⋯ p.reverse
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ Hconcat p.reverse.reverse ⋯ (concatRecAux Hnil Hconcat p.reverse) ≍
    Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)

Tactic:
congr

Goal state after:
case e_4
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ p.reverse.reverse = p

case e_6
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat p.reverse ≍ ⋯ ▸ concatRecAux Hnil Hconcat p.reverse
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
· rw [concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      obtain ⟨rfl, rfl⟩ := ih (heq_iff_eq.mp he)
      exact ⟨rfl, rfl⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.support.reverse

Tactic:
← support_reverse

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.reverse.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝ : V
h✝¹ : G.Adj v v✝
h✝ : G.Adj v✝ v
hp : (cons h✝¹ (cons h✝ nil)).IsCircuit
⊢ 3 ≤ (cons h✝¹ (cons h✝ nil)).length

Tactic:
simpa using hp.isTrail

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ (cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges

Tactic:
by
  simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons,
    support_cons, List.tail_cons]
  have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup
  tauto

Goal state after: