mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map ((F.mapId { as := op (X i₁) }).hom.toNatTrans.app (D.obj i₁)) ≫ D.hom q f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom ⋯ D (f₁ ≫ f i₁) f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map ((F.mapId { as := op (X i₂) }).hom.toNatTrans.app (D.obj i₂))

Tactic:
pullFunctorObjHom_eq_assoc _ _ _ _ _ q f₁ f₂ rfl

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map ((F.mapId { as := op (X i₁) }).hom.toNatTrans.app (D.obj i₁)) ≫ D.hom q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (𝟙 (X i₁)).op.toLoc f₁.op.toLoc f₁.op.toLoc ⋯).inv.toNatTrans.app (D.obj i₁) ≫
      D.hom q f₁ f₂ ⋯ ⋯ ≫
        (F.mapComp' (𝟙 (X i₂)).op.toLoc f₂.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (D.obj i₂) ≫
          (F.map f₂.op.toLoc).toFunctor.map ((F.mapId { as := op (X i₂) }).hom.toNatTrans.app (D.obj i₂))
Module: Mathlib.CategoryTheory.Sites.PreservesLimits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : J.Subcanonical
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
F : K ⥤ C
inst✝ : ∀ (X : Sheaf J (Type (max v v'))), PreservesLimit F.op X.obj
c : Cocone F
hc : IsColimit c
⊢ IsColimit ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c)

Tactic:
suffices IsLimit (coyoneda.mapCone (J.uliftYoneda.mapCocone c).op) from
      isColimitOfOp (isLimitOfReflects _ this)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : J.Subcanonical
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
F : K ⥤ C
inst✝ : ∀ (X : Sheaf J (Type (max v v'))), PreservesLimit F.op X.obj
c : Cocone F
hc : IsColimit c
⊢ IsLimit (coyoneda.mapCone ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c).op)
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x : F.obj (Opposite.op X)
hx : K.SubsheafClosure 𝒮 X x
⊢ ∃ i, Witness.eval hF ι t i = some x

Tactic:
induction hx with
    | base ha => exact ⟨.base _ (equivShrink _ ⟨_, ha⟩), by grind [Witness.eval]⟩
    | restrict f ha ih =>
      obtain ⟨i, hi⟩ := ih
      use .restrict f i
      grind [Witness.eval]
    | amalgamate hR hy hmem ht ih =>
      choose x hx using ih
      exact ⟨.amalgamate hR x, by simp [Witness.eval, hx]; grind⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : C ⥤ MonCat
S : SubmonoidFunctor M
U V : C
f : U ⟶ V
⊢ Submonoid.map (MonCat.Hom.hom (M.map f)) (S.obj U) ≤ S.obj V

Tactic:
by
  grw [Submonoid.map_le_iff_le_comap, S.map f]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow

Tactic:
fapply (Subobject.isPullback (h.χ m) h.Ω₀).flip.of_iso
    (((MonoOver.forget _ ⋙ Over.forget _).mapIso (h.iso m)).symm) (Iso.refl _)
    (Iso.refl _) (Iso.refl _)

Goal state after:
case commfst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ (Iso.refl X).hom =
    ((MonoOver.forget X ⋙ Over.forget X).mapIso (h.iso m)).symm.hom ≫ m

case commsnd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ pullbackπ (h.χ m) h.Ω₀ ≫ (Iso.refl (underlying.obj h.Ω₀)).hom =
    ((MonoOver.forget X ⋙ Over.forget X).mapIso (h.iso m)).symm.hom ≫ h.π m

case commf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ h.χ m ≫ (Iso.refl Ω).hom = (Iso.refl X).hom ≫ h.χ m

case commg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ h.Ω₀.arrow ≫ (Iso.refl Ω).hom = (Iso.refl (underlying.obj h.Ω₀)).hom ≫ h.Ω₀.arrow
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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
⊢ HasKernel f₁

Tactic:
exact hasKernel hι hT hT'

Goal state after:
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : α → Finset β
h₁ : s.Nonempty
h₂ : ∀ j ∈ s, 0 < #(f j)
k : ℕ := s.inf' h₁ fun j ↦ #(f j)
hk : k = s.inf' h₁ fun j ↦ #(f j)
h₃ : ∀ a ∈ s, ∀ x ∈ f a, #{j | j ∈ s ∧ x ∈ f j} ≤ k
⊢ #s ≤ #(s.biUnion f)

Tactic:
suffices #s • k ≤ #(s.biUnion f) • k by simp_all

Goal state after:
α : Type u
β : Type v
inst✝² : DecidableEq β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : α → Finset β
h₁ : s.Nonempty
h₂ : ∀ j ∈ s, 0 < #(f j)
k : ℕ := s.inf' h₁ fun j ↦ #(f j)
hk : k = s.inf' h₁ fun j ↦ #(f j)
h₃ : ∀ a ∈ s, ∀ x ∈ f a, #{j | j ∈ s ∧ x ∈ f j} ≤ k
⊢ #s • k ≤ #(s.biUnion f) • k
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ log ↑N - 4 * √(log ↑N) ≤ 0

Tactic:
sub_nonpos,

Goal state after:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ log ↑N ≤ 4 * √(log ↑N)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑∅ • A
⊢ ∃ x, A * A ⊆ x • A

pp: case inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑{x} • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
· simp [hA.nonempty.ne_empty] at hKA

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑{x} • A
⊢ ∃ x, A * A ⊆ x • A
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V → W
⊢ Monotone (SimpleGraph.map f)

Tactic:
rintro G G' h z1 z2 ⟨huv, u, v, ha, rfl, rfl⟩

Goal state after:
V : Type u_1
W : Type u_2
f : V → W
G G' : SimpleGraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
huv : f u ≠ f v
⊢ (SimpleGraph.map f G').Adj (f u) (f v)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ =
    #{x |
        match x with
        | (x, y) => G.Adj x y}

Tactic:
refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ a ∈ univ,
    (a.toProd.1, a.toProd.2) ∈
      {x |
        match x with
        | (x, y) => G.Adj x y}

case refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a : V × V)
    (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
    { toProd := a, adj := ⋯ } ∈ univ

case refine_3
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a : G.Dart) (ha : a ∈ univ), { fst := a.toProd.1, snd := a.toProd.2, adj := ⋯ } = a

case refine_4
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a : V × V)
    (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
    ({ toProd := a, adj := ⋯ }.toProd.1, { toProd := a, adj := ⋯ }.toProd.2) = a
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ Even #{v | Odd (G.degree v)}

Tactic:
rw [sum_congr (g := fun _v ↦ (1 : ZMod 2)) rfl] at h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ _v with ↑(G.degree _v) ≠ 0, 1 = 0
⊢ Even #{v | Odd (G.degree v)}

V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < 2 * k
⊢ 0 < k

Tactic:
mul_pos_iff_of_pos_left

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < k
⊢ 0 < k

V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < 2 * k
⊢ 0 < 2
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
p : α
⊢ p ∈ (P i).parts → p ∉ (P j).parts

Tactic:
hpi

Goal state after:
α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
p : α
hpi : p ∈ (P i).parts
⊢ p ∉ (P j).parts
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
⊢ parts.sup id = s

Tactic:
ext i
    simp only [mem_sup, id_eq]
    constructor
    · rintro ⟨j, hj, hj'⟩
      exact h j hj hj'
    · rintro hi
      exact (h' i hi).exists

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∀ (a b : ↥s),
    P.part ↑a = P.part ↑b ↔
      ((P.equivSigmaParts.trans ((Equiv.refl ↥P.parts).sigmaCongr fun t ↦ (↑t).equivFin)) a).fst =
        ((P.equivSigmaParts.trans ((Equiv.refl ↥P.parts).sigmaCongr fun t ↦ (↑t).equivFin)) b).fst

Tactic:
simp [equivSigmaParts, Equiv.sigmaCongr, Equiv.sigmaCongrLeft]

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
⊢ 4 ^ #P.parts * ↑m ≤ ↑(#u)

Tactic:
by
  norm_cast
  rw [stepBound, ← Nat.div_div_eq_div_mul]
  exact (Nat.mul_div_le _ _).trans (hP.average_le_card_part hu)

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
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
⊢ t ∈ Q

Tactic:
hau.2 _ ht

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.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t|

Tactic:
by
  unfold nonuniformWitness
  rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)
  · rw [if_pos lt, if_neg (asymm lt)]
    exact G.nonuniformWitnesses_spec h₂
  · cases h₁ rfl
  · rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]
    apply G.nonuniformWitnesses_spec fun i => h₂ i.symm

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝³ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ↑(P.energy G) = (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#P.parts) ^ 2

Tactic:
rw [energy]

Goal state after:
α : Type u_1
inst✝⁴ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝³ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ↑((∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2) / ↑(#P.parts) ^ 2) =
    (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ 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
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
left✝ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
ha : ¬0 < a
⊢ t ∉ {i ∈ R.parts | #i = m + 1}

Tactic:
intro H; exact ht.ne_empty (le_sdiff_right.1 <| R.le <| filter_subset _ _ H)

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ #⊥.parts ∧ #⊥.parts ≤ bound ε l ∧ ⊥.IsUniform G ε

Tactic:
rw [card_bot, card_univ]

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ ⊥.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges ↑s)
⊢ r ≤ ↑(#s)

Tactic:
· classical
    simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 2 ^ #P.parts * (2 ^ #P.parts * ↑m / ↑(#U)) = (2 * 2) ^ #P.parts * ↑m / ↑(#U)

Tactic:
rw [mul_pow, ← mul_div_assoc, mul_assoc]

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

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (G'.induce s).verts ⊆ (G''.induce s').verts

pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w

Tactic:
· simp [hs]

Goal state after:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (⊤.induce {v, w}).Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
simp only [induce_adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h

Goal state after:
case Adj.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (x✝¹ = v ∨ x✝¹ = w) ∧ (x✝ = v ∨ x✝ = w) ∧ G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x ↦ x.toProd.2) p.darts = p.support.tail

Tactic:
simpa using congr_arg List.tail (cons_map_snd_darts p)

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
h : w ∈ nil.support
⊢ (nil.takeUntil w h).support = ((nil.take (List.idxOf w nil.support)).copy ⋯ ⋯).support

Tactic:
simp only [takeUntil, eq_mpr_eq_cast, support_nil, getVert_nil, take, support_copy]

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
h : w ∈ nil.support
⊢ (cast ⋯ nil).support = [u✝]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : w = v✝ ∧ nil ≍ p✝.concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝

Tactic:
obtain ⟨rfl, he⟩ := he

Goal state after:
case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h h✝ : G.Adj u✝ w
p✝ : G.Walk w v'
he : nil ≍ p✝.concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case 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
p' : G.Walk u✝ v'
he : (cons h✝ p✝).concat h = p'.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = p'

Tactic:
concat_cons

Goal state after:
case 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
p' : G.Walk u✝ v'
he : cons h✝ (p✝.concat h) = p'.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = p'
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : 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
h✝ : G.Adj v' v✝
he : v✝ = w ∧ p✝.concat h ≍ nil
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil

Tactic:
obtain ⟨rfl, he⟩ := he

Goal state after:
case cons.nil
V : Type u
G : SimpleGraph V
u v v' v✝ w✝ : V
p✝ : G.Walk v✝ w✝
h✝ h' : G.Adj v' v✝
ih : ∀ {h : G.Adj w✝ v✝} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ v✝
he : p✝.concat h ≍ nil
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil
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 : v✝¹ = v✝ ∧ p✝¹.concat h ≍ p✝.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
obtain ⟨rfl, he⟩ := he

Goal state after:
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
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : p✝¹.concat h ≍ p✝.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ ↑p.support + ↑p'.support.tail = ↑p.support + ↑p'.support - {v}

Tactic:
coe_support,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + ({v} + ↑p'.support.tail) - {v}
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ Set.InjOn p.getVert {i | i ≤ p.length}

Tactic:
intro n hn m hm hnm

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
n : ℕ
hn : n ∈ {i | i ≤ p.length}
m : ℕ
hm : m ∈ {i | i ≤ p.length}
hnm : p.getVert n = p.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ ↔ G.IsClique s

Tactic:
isClique_iff

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ ↔ s.Pairwise G.Adj