mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ PreservesLimit F (GrothendieckTopology.uliftYoneda.{v', v, u} J)

Tactic:
have : PreservesLimitsOfShape K (uliftYoneda J ⋙ sheafToPresheaf J (Type max v v')) :=
      preservesLimitsOfShape_of_natIso (uliftYonedaCompSheafToPresheaf J).symm

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
this : PreservesLimitsOfShape K (GrothendieckTopology.uliftYoneda.{v', v, u} J ⋙ sheafToPresheaf J (Type (max v v')))
⊢ PreservesLimit F (GrothendieckTopology.uliftYoneda.{v', v, u} J)
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
⊢ Epi ((presheafToSheaf J D).map f.hom)

Tactic:
h₁

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
⊢ Epi ((sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G))
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
p : G.obj X
⊢ { arrows := fun Y f ↦ ∃ a, (ConcreteCategory.hom (G.map f.op)) p = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
        downward_closed := ⋯ } =
      ⊤ →
    ∃ x₁, (ConcreteCategory.hom (m.app X)) x₁ = p

Tactic:
hp

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
p : G.obj X
hp :
  { arrows := fun Y f ↦ ∃ a, (ConcreteCategory.hom (G.map f.op)) p = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
      downward_closed := ⋯ } =
    ⊤
⊢ ∃ x₁, (ConcreteCategory.hom (m.app X)) x₁ = p
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 ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
x✝ : Dᵒᵖ
⊢ adj.op.unit.app x✝ =
    (PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)).unit.app x✝

Tactic:
dsimp [PullbackShift.adjunction, NatTrans.PullbackShift.natIsoId,
      NatTrans.PullbackShift.natIsoComp, PullbackShift.functor, PullbackShift.natTrans,
      OppositeShift.adjunction, OppositeShift.natTrans, NatTrans.OppositeShift.natIsoId,
      NatTrans.OppositeShift.natIsoComp, OppositeShift.functor]

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 ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
x✝ : Dᵒᵖ
⊢ (adj.counit.app (unop x✝)).op =
    𝟙 x✝ ≫ (𝟙 x✝ ≫ (adj.counit.app (unop x✝)).op ≫ 𝟙 (op (F.obj (G.obj (unop x✝))))) ≫ 𝟙 (op (F.obj (G.obj (unop x✝))))
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ P.triangEnvelope T.obj₁ → P.triangEnvelope T.obj₃ → P.triangEnvelope T.obj₂

Tactic:
h₁

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : P.triangEnvelope T.obj₁
⊢ P.triangEnvelope T.obj₃ → P.triangEnvelope T.obj₂
Module: Mathlib.CategoryTheory.Triangulated.WeakKernels

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ Nonempty (WeakLimitCone (parallelPair f 0))

Tactic:
by
    obtain ⟨K, i, p, h⟩ := distinguished_cocone_triangle₁ f
    exact ⟨_, isWeakLimitKernelForkOfDistTriangle _ h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : HasShift D ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
E : C ≌ D
inst✝² : E.functor.CommShift ℤ
inst✝¹ : E.inverse.CommShift ℤ
inst✝ : E.CommShift ℤ
⊢ Equivalence.refl.IsTriangulated

Tactic:
dsimp [Equivalence.IsTriangulated]

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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : HasShift D ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
E : C ≌ D
inst✝² : E.functor.CommShift ℤ
inst✝¹ : E.inverse.CommShift ℤ
inst✝ : E.CommShift ℤ
⊢ Equivalence.refl.toAdjunction.IsTriangulated
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝²³ : HasZeroObject C
inst✝²² : HasZeroObject D
inst✝²¹ : Preadditive C
inst✝²⁰ : Preadditive D
inst✝¹⁹ : HasShift C ℤ
inst✝¹⁸ : HasShift D ℤ
inst✝¹⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁵ : Pretriangulated C
inst✝¹⁴ : Pretriangulated D
E : C ≌ D
inst✝¹³ : E.functor.CommShift ℤ
inst✝¹² : E.inverse.CommShift ℤ
inst✝¹¹ : E.CommShift ℤ
D' : Type u_3
inst✝¹⁰ : Category.{v_3, u_3} D'
inst✝⁹ : HasZeroObject D'
inst✝⁸ : Preadditive D'
inst✝⁷ : HasShift D' ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D' n).Additive
inst✝⁵ : Pretriangulated D'
E' : D ≌ D'
inst✝⁴ : E'.functor.CommShift ℤ
inst✝³ : E'.inverse.CommShift ℤ
inst✝² : E'.CommShift ℤ
inst✝¹ : E.IsTriangulated
inst✝ : E'.IsTriangulated
⊢ (E.trans E').IsTriangulated

Tactic:
dsimp [Equivalence.IsTriangulated]

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✝²³ : HasZeroObject C
inst✝²² : HasZeroObject D
inst✝²¹ : Preadditive C
inst✝²⁰ : Preadditive D
inst✝¹⁹ : HasShift C ℤ
inst✝¹⁸ : HasShift D ℤ
inst✝¹⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁵ : Pretriangulated C
inst✝¹⁴ : Pretriangulated D
E : C ≌ D
inst✝¹³ : E.functor.CommShift ℤ
inst✝¹² : E.inverse.CommShift ℤ
inst✝¹¹ : E.CommShift ℤ
D' : Type u_3
inst✝¹⁰ : Category.{v_3, u_3} D'
inst✝⁹ : HasZeroObject D'
inst✝⁸ : Preadditive D'
inst✝⁷ : HasShift D' ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D' n).Additive
inst✝⁵ : Pretriangulated D'
E' : D ≌ D'
inst✝⁴ : E'.functor.CommShift ℤ
inst✝³ : E'.inverse.CommShift ℤ
inst✝² : E'.CommShift ℤ
inst✝¹ : E.IsTriangulated
inst✝ : E'.IsTriangulated
⊢ (E.trans E').toAdjunction.IsTriangulated
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: M N : ℕ
⊢ addRothNumber (range (M + N)) ≤ addRothNumber (range M) + addRothNumber (range N)

Tactic:
range_add_eq_union,

Goal state after:
M N : ℕ
⊢ addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤ addRothNumber (range M) + addRothNumber (range N)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
⊢ 0 < dValue N

Tactic:
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < dValue N
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:
simpa using ruzsa_triangle_inequality_div_div_div A B⁻¹ C

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

Goal state before:
pp: case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := ⋯
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := ⋯
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C' * A * B) ≤ #(C * A * B) + #(A * B) - #(A' * B)

Tactic:
h₁

Goal state after:
case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)) ≤ #(C * A * B) + #(A * B) - #(A' * B)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)) ≤ #(C * A * B) + #(A * B) - #(A' * B)

Tactic:
refine (card_union_le _ _).trans_eq ?_

Goal state after:
case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
hC : C.Nonempty
hCA : C ⊆ A
⊢ (↑(#(C * B)) / ↑(#C)) ^ (m + n) * ↑(#C) * ↑(#C) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A) * ↑(#C)

Tactic:
gcongr (?_ ^ _) * #?_ * _; exact hCmin _ hA'

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
x : G
⊢ A.convolution B x ≤ #B

Tactic:
rw [← inv_inv B, ← inv_inv x, ← card_smul_inter, card_inv]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹
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).convolution B x = A.convolution (s •> B) x

Tactic:
nth_rw 1 [← inv_inv B, ← inv_inv (s • B), inv_smul_finset_distrib s B, ← card_inter_smul,
    ← card_inter_smul, smul_comm]

Goal state after:
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⁻¹)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m
ih :
  ∀ (ε : Fin m → ℤ),
    (∀ (i : Fin m), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ k ^ (m - 2) * ↑(#A)
ε : Fin (m + 1) → ℤ
hε : ∀ (i : Fin (m + 1)), |ε i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)

Tactic:
obtain _ | m := m
    · simp at hm
    have hm₀ : m ≠ 0 := by simp at hm; positivity
    have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i
    obtain rfl | hA := A.eq_empty_or_nonempty
    · simp [hε₀]
    have hk : 0 ≤ k :=
      nonneg_of_mul_nonneg_left ((h 1 (by simp)).trans' (by positivity)) (by positivity)
    let π {n} (δ : Fin n → ℤ) : Finset G := ((finRange _).map fun i ↦ A ^ δ i).prod
    let V : Finset G := π ![-ε 1, -ε 0]
    let W : Finset G := π <| tail <| tail ε
    refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)
    calc
      (#A * #(π ε) : ℝ)
        = #A * #(V⁻¹ * W) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def, mul_assoc]
      _ ≤ #(A * V) * #(A * W) := by norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul ..
      _ = #(π ![1, -ε 1, -ε 0]) * #(π <| Fin.cons 1 <| tail <| tail ε) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def]
      _ ≤ (k * #A) * (k ^ (m - 1) * #A) := by
        gcongr
        · exact h ![1, -ε 1, -ε 0] fun i ↦ by fin_cases i <;> simp [hε]
        · exact ih (Fin.cons 1 <| tail <| tail ε) <| Fin.cons (by simp) (by simp [hε, Fin.tail])
      _ = #A * (k ^ m * #A) := by rw [← pow_sub_one_mul hm₀]; ring

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
v : V
⊢ (f.symm.toHom.comp f.toHom) v = Hom.id v

Tactic:
simp only [RelHom.comp_apply, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding,
    RelIso.symm_apply_apply, RelHom.id_apply]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card V = Fintype.card W

Tactic:
rw [← Fintype.ofEquiv_card f.toEquiv]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card W = Fintype.card W
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
⊢ p ∈ P.parts → p ∈ s.powerset

Tactic:
hp

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ∈ s.powerset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ #Q.parts ≤ #P.parts

Tactic:
have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
  choose f hP hf using this
  rw [← card_attach]
  refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_
  exact
    Subtype.coe_injective
      (Q.disjoint.elim b.2 c.2 fun H ↦
        P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)

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

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

Tactic:
rw [h]
    rw [Finset.card_eq_zero, parts_eq_empty_iff, bot_eq_empty, ← Finset.card_eq_zero] at h
    rw [h]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁

Tactic:
mem_interedges_iff

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s' t
⊢ False

Tactic:
mem_interedges_iff

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
hy : a✝.1 ∈ s' ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
⊢ False
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 t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s t'
⊢ False

Tactic:
mem_interedges_iff

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
hy : a✝.1 ∈ s ∧ a✝.2 ∈ t' ∧ r a✝.1 a✝.2
⊢ False
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 α
a b : α
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(#t) * ε ≤ ↑(#t')
hs : ↑(#s) * ε ≤ ↑(#s')
⊢ |↑(G.edgeDensity t' s') - ↑(G.edgeDensity t s)| < ε

Tactic:
by
    rw [edgeDensity_comm _ t', edgeDensity_comm _ t]
    exact h hs' ht' hs ht

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s (P.parts.biUnion id)) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
interedges_biUnion_right,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(P.parts.biUnion fun b ↦ interedges r s (id b)) = ∑ b ∈ P.parts, #(interedges r s b)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts = ∅
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Tactic:
· simp [h]

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : 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
⊢ 0 < Fintype.card α

Tactic:
exact (bound_pos _ _).trans_le hα

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

Goal state before:
pp: case neg.refine_2
α : 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
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
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
hR₂ : ∀ 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
⊢ ∀ x ∈ P.parts, #(x \ {y ∈ (R.extend ⋯ ⋯ ⋯).parts | y ⊆ x}.biUnion id) ≤ m

Tactic:
conv in _ ∈ _ => rw [← insert_erase hu₁]
    simp only [mem_insert, forall_eq_or_imp, extend_parts]
    refine ⟨?_, fun x hx => (card_le_card ?_).trans <| hR₂ x ?_⟩
    · simp only [filter_insert, if_pos htu, biUnion_insert, id]
      obtain rfl | hut := eq_or_ne u t
      · rw [sdiff_eq_empty_iff_subset.2 subset_union_left]
        exact bot_le
      refine
        (card_le_card fun i => ?_).trans
          (hR₂ (u \ t) <| P.mem_avoid.2 ⟨u, hu₁, fun i => hut <| i.antisymm htu, rfl⟩)
      simpa using fun hi₁ hi₂ hi₃ =>
        ⟨⟨hi₁, hi₂⟩, fun x hx hx' => hi₃ _ hx <| hx'.trans sdiff_subset⟩
    · apply sdiff_subset_sdiff Subset.rfl (biUnion_subset_biUnion_of_subset_left _ _)
      exact filter_subset_filter _ (subset_insert _ _)
    simp only [avoid, ofErase, mem_erase, mem_image, bot_eq_empty]
    exact
      ⟨(nonempty_of_mem_parts _ <| mem_of_mem_erase hx).ne_empty, _, mem_of_mem_erase hx,
        (disjoint_of_subset_right htu <|
            P.disjoint (mem_of_mem_erase hx) hu₁ <| ne_of_mem_erase hx).sdiff_eq_left⟩

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
⊢ S ⊆ H'.verts → S ⊆ ⊥

Tactic:
h₁

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
⊢ S ⊆ ⊥