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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
⊢ (F.toDescentData f).IsEquivalence

Tactic:
have := (F.fullyFaithfulToDescentData _ (J.superset_covering h₂ h₁)).faithful

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this : (F.toDescentData f).Faithful
⊢ (F.toDescentData f).IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst✝³ : HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
⊢ F.IsStack J.toGrothendieck

Tactic:
refine ⟨fun {S} R hR ↦ IsStackFor.essSurj ?_⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst✝³ : HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
S : C
R : Sieve S
hR : R ∈ J.toGrothendieck S
⊢ F.IsStackFor R.arrows
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ (F.map (Over.Hom.left φ).op ≫ app hG x hx Y₂.hom) ≫ G.map Z.hom.op =
    (app hG x hx Y₁.hom ≫ G.map (Over.Hom.left φ).op) ≫ G.map Z.hom.op

Tactic:
rw [assoc, assoc, app_cond hG x hx Y₂.hom Z.hom hZ, ← G.map_comp, ← op_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ F.map (Over.Hom.left φ).op ≫ F.map Z.hom.op ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    app hG x hx Y₁.hom ≫ G.map (Z.hom ≫ Over.Hom.left φ).op
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g ≫ G.map (𝟙 Y).op = F.map (𝟙 Y).op ≫ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
rw [op_id, G.map_id, comp_id, F.map_id, id_comp] at H

Goal state after:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ ∃ e, Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

Tactic:
have h₁ (i' : ι') : ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i' := by
    obtain ⟨_, _, _, ⟨i⟩, fac⟩ : Sieve.ofArrows X f (f' i') := by
      rw [h]; apply Sieve.ofArrows_mk
    exact ⟨i, _, fac⟩
  have h₂ (i : ι) : ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i := by
    obtain ⟨_, _, _, ⟨i'⟩, fac⟩ : Sieve.ofArrows X' f' (f i) := by
      rw [← h]; apply Sieve.ofArrows_mk
    exact ⟨i', _, fac⟩
  choose α p' w using h₁
  choose β q' w' using h₂
  exact ⟨pullFunctorEquivalence (p' := p') (q' := q') F (Iso.refl _)
    (by cat_disch) (by cat_disch), ⟨toDescentDataCompPullFunctorIso _ _ ≪≫
    Functor.isoWhiskerRight (Cat.Hom.toNatIso (F.mapId _)) _ ≪≫ Functor.leftUnitor _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ χ'.hom = (χ m).hom

Tactic:
← cancel_mono (closedSieves J).ι,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ χ'.hom ≫ (closedSieves J).ι = (χ m).hom ≫ (closedSieves J).ι
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
map_opShiftFunctorEquivalence_counitIso_hom_app_unop

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op).unop ≫
          ((commShiftIso F.op n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.IsTriangulated
T : Triangle Cᵒᵖ
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ F.op.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles

Tactic:
rw [mem_distTriang_op_iff]
    exact Pretriangulated.isomorphic_distinguished _
      ((F.map_distinguished _ (unop_distinguished _ dT))) _
      (((opMapTriangleCompTriangleOpEquivalenceInverse F).symm.app T).unop)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
    Pretriangulated.distinguishedTriangles

Tactic:
Functor.comp_obj,

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ unop ((triangleOpEquivalence D).inverse.obj ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T)))) ∈
    Pretriangulated.distinguishedTriangles
Module: Mathlib.Combinatorics.Additive.CovBySMul

Goal state before:
pp: M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A B₁ B₂ : Set X
hB : B₁ ⊆ B₂
hAB : CovBySMul M K A B₁
⊢ CovBySMul M K A B₂

Tactic:
simpa using hAB.trans (.of_subset (M := M) hB)

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N) + -2 * √(log ↑N))

Tactic:
← add_mul

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log ↑N)) = rexp ((-2 + -2) * √(log ↑N))
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ ↑(#(Finset.image (⇑f) F)) ≤ K

pp: case refine_2
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ (⇑f '' A) ^ 2 ⊆ ↑(Finset.image (⇑f) F) • ⇑f '' A

Tactic:
· calc
        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
        _ ≤ K := hF

Goal state after:
case refine_2
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ (⇑f '' A) ^ 2 ⊆ ↑(Finset.image (⇑f) F) • ⇑f '' A
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
⊢ b ≠ ⊥

Tactic:
intro h
  refine P.bot_notMem (?_)
  rw [h] at hb
  exact hb

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
⊢ Disjoint (x₁ ⊓ y₁) (x₁ ⊓ y₂)

Tactic:
refine Disjoint.mono inf_le_right inf_le_right (Q.disjoint hy₁ hy₂ ?_)

Goal state after:
case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
⊢ y₁ ≠ y₂
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case mp
α : 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
i : α
⊢ (∃ i_1 ∈ parts, i ∈ i_1) → i ∈ s

Tactic:
rintro ⟨j, hj, hj'⟩
      exact h j hj hj'

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
⊢ a ∈ t → P.part a = t

Tactic:
intro hat

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a = t
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
b : α
⊢ b ∈ (ofSetSetoid s x).part a ↔ a ∈ x ∧ b ∈ x ∧ s a b

Tactic:
by
  suffices (∃ a₁ ∈ x, (b ∈ x ∧ s a₁ b) ∧ a ∈ x ∧ s a₁ a) ↔ a ∈ x ∧ b ∈ x ∧ s a b by
    simpa [mem_part_iff_exists, ofSetSetoid_parts]
  exact ⟨
    fun ⟨c, _, ⟨hb, hcb⟩, ⟨ha, hca⟩⟩ ↦ ⟨ha, hb, s.trans' (s.symm' hca) hcb⟩,
    fun h ↦ ⟨a, ⟨h.1, ⟨⟨h.2.1, h.2.2⟩, ⟨h.1, s.refl _⟩⟩⟩⟩
  ⟩

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

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

Tactic:
simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X)))

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

Goal state before:
pp: case calc_1
α : 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 ≤ ε
⊢ ∑ UV ∈ P.sparsePairs G ε, ↑(#(G.interedges UV.1 UV.2)) ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (↑(#UV.1) * ↑(#UV.2))

pp: case calc_2
α : 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 ≤ ε
⊢ ε * ∑ UV ∈ P.parts.offDiag, ↑(#UV.1) * ↑(#UV.2) ≤ ε * (↑(#A) + ↑(#P.parts)) ^ 2

Tactic:
· gcongr with ⟨U, V⟩ hUV
    simp only [mk_mem_sparsePairs, ne_eq, ← card_interedges_div_card, Rat.cast_div,
      Rat.cast_natCast, Rat.cast_mul] at hUV
    refine ((div_lt_iff₀ ?_).1 hUV.2.2.2).le
    exact mul_pos (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.1).card_pos)
      (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.2.1).card_pos)

Goal state after:
case calc_2
α : 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 ≤ ε
⊢ ε * ∑ UV ∈ P.parts.offDiag, ↑(#UV.1) * ↑(#UV.2) ≤ ε * (↑(#A) + ↑(#P.parts)) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts) ≤ ε / 2 * ↑(#A) ^ 2

Tactic:
div_le_iff₀ (Nat.cast_pos.2 (P.parts_nonempty hA.ne_empty).card_pos)

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)
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)}) * 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:
← add_mul

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)}) +
        #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)})) *
      4 ^ #P.parts =
    stepBound #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
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ (G.deleteIncidenceSet x).support.toFinset ⊆ (G.support \ {x}).toFinset

Tactic:
Set.toFinset_subset_toFinset

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 ⊆ G.support \ {x}
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
⊢ (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty

Tactic:
Subgraph.edgeSet_map

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' G'.edgeSet).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ #s % n + n * (#s / n) = #s

Tactic:
mod_add_div

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ #s = #s
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp
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
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ Sym2.Rel V (v', w') (v, w) → s(⟨v', hv'⟩, ⟨w', hw'⟩) ∉ s

Tactic:
rintro (_ | _) <;> simpa only [Sym2.eq_swap]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.reverse.getVert i = p.getVert (p.length - i)

Tactic:
by
  induction p with
  | nil => rfl
  | cons h p ih =>
    simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]
    split_ifs
    next hi => simp [Nat.succ_sub hi.le]
    next hi =>
      obtain rfl | hi' := eq_or_gt_of_not_lt hi
      · simp
      · rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
        simp

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 V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
rw [sub_mul, one_mul, sub_le_sub_iff_left]

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ ε ^ 5 / 50 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 50
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:
rw [concat_cons] at he

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.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝¹ : G.Adj u' v'
h✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts

Tactic:
refine h.imp (fun h ↦ ?_) (fun h ↦ ?_)

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ { fst := u', snd := v', adj := h✝² } ∈ p.darts

case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := v', snd := u', adj := ⋯ } ∈ p.darts