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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom ((S.map (↾fun x ↦ PUnit.unit).op ≫ S.map g₁.op) ≫ S.map g.op))
      (f ((ConcreteCategory.hom f₁) (Classical.choose hf₁))) =
    (ConcreteCategory.hom ((S.map (↾fun x ↦ PUnit.unit).op ≫ S.map g₂.op) ≫ S.map g.op))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))

Tactic:
← Functor.map_comp,

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map (((↾fun x ↦ PUnit.unit).op ≫ g₁.op) ≫ g.op)))
      (f ((ConcreteCategory.hom f₁) (Classical.choose hf₁))) =
    (ConcreteCategory.hom (S.map (((↾fun x ↦ PUnit.unit).op ≫ g₂.op) ≫ g.op)))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (↾fun x ↦ (ConcreteCategory.hom (S.map f.op ≫ S.map (↾fun x_1 ↦ x).op)) s)) x =
    (ConcreteCategory.hom (f ≫ ↾fun x ↦ (ConcreteCategory.hom (S.map (↾fun x_1 ↦ x).op)) s)) x

Tactic:
← Functor.map_comp,

Goal state after:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (↾fun x ↦ (ConcreteCategory.hom (S.map (f.op ≫ (↾fun x_1 ↦ x).op))) s)) x =
    (ConcreteCategory.hom (f ≫ ↾fun x ↦ (ConcreteCategory.hom (S.map (↾fun x_1 ↦ x).op)) s)) x
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: α : Type u
S : Sieve α
⊢ S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α ↔ S ∈ typesGrothendieckTopology α

Tactic:
refine ⟨fun hs x => ?_, fun hs β f => Presieve.isSheaf_yoneda' _ fun y => hs (f y)⟩

Goal state after:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
⊢ S.arrows (↾fun x_1 ↦ x)
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ G.IsGeneratedBy fun i' ↦ x (e i')

Tactic:
rw [isGeneratedBy_iff, ← h.iSup_eq]
  exact Equiv.iSup_congr e (congrFun rfl)

Goal state after:
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
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ (presheafToSheaf J D).map (pullback.fst f f).hom ≫ (presheafToSheaf J D).map p =
    (presheafToSheaf J D).map (pullback.snd f f).hom ≫ (presheafToSheaf J D).map p

Tactic:
← Functor.map_comp,

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
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ (presheafToSheaf J D).map ((pullback.fst f f).hom ≫ p) =
    (presheafToSheaf J D).map (pullback.snd f f).hom ≫ (presheafToSheaf J D).map p
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ A ≤ B →
    { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B

Tactic:
· intro h
      exact leOfHom (((equivalenceMonoOver F).trans
        (ThinSkeleton.equivalence _).symm).functor.map (homOfLE h))

Goal state after:
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
n : ℕ
⊢ ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter (n + 1)).retractClosure =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure

Tactic:
extensionProductIter_succ',

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
n : ℕ
⊢ (((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).extensionProduct
        (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure
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 Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
⊢ P.triangEnvelope ≤ Q ↔ P ≤ Q

Tactic:
refine ⟨fun h ↦ le_trans P.le_triangEnvelope h, fun h ↦ ?_⟩
  rw [triangEnvelope, iSup_le_iff]
  intro n
  rw [triangEnvelopeIter, retractClosure_le_iff]
  apply extensionProductIter_le_of_isTriangulatedClosed₂
  rwa [retractClosure_le_iff, binaryProductsClosure_le_iff, shiftClosure_le_iff]

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
⊢ ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).obj (op T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
exact F.op.map_distinguished _ (op_distinguished _ dT)

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

Goal state before:
pp: case refine_1
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 c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app X)) ≫
        (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
← Functor.map_comp,

Goal state after:
case refine_1
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 c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app X) ≫ (t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case refine_3
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝¹ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this✝ : Mono ((adj.homEquiv Z T.obj₃) h)
this : IsIso ((adj.homEquiv Z T.obj₃) h)
⊢ g = g ≫ (shiftFunctor C 1).map (adj.unit.app (G.obj T.obj₁)) ≫ (shiftFunctor C 1).map (G.map (adj.counit.app T.obj₁))

Tactic:
← Functor.map_comp,

Goal state after:
case refine_3
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝¹ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this✝ : Mono ((adj.homEquiv Z T.obj₃) h)
this : IsIso ((adj.homEquiv Z T.obj₃) h)
⊢ g = g ≫ (shiftFunctor C 1).map (adj.unit.app (G.obj T.obj₁) ≫ G.map (adj.counit.app T.obj₁))
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ mulRothNumber {a} = 1

Tactic:
refine ThreeGPFree.mulRothNumber_eq ?_

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

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
h : Set.BijOn Nat.cast ↑(range ↑k) ↑(Iio k)
⊢ addRothNumber (Iio k) ≤ rothNumberNat ↑k

Tactic:
by
    exact (AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h

Goal state after:
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 L : ℝ
A B : Set X
hKL : K ≤ L
⊢ CovBySMul M K A B → CovBySMul M L A B

Tactic:
rintro ⟨F, hF, hFAB⟩

Goal state after:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K L : ℝ
A B : Set X
hKL : K ≤ L
F : Finset M
hF : ↑(#F) ≤ K
hFAB : A ⊆ ↑F • B
⊢ CovBySMul M L A B
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ #univ • (d - 1) ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
rw [Finset.card_fin, smul_eq_mul]

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

Goal state before:
pp: case inr.inr.ha
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n

Tactic:
rwa [one_le_cast]

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

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

Tactic:
← log_le_log_iff (mul_pos (cast_pos.2 (zero_lt_two.trans_le hN)) (exp_pos _)) zero_lt_one,

Goal state after:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ log (↑N * rexp (-4 * √(log ↑N))) ≤ log 1
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f : G ↪g G'
v w₁ : V
h₁ : w₁ ∈ G.neighborSet v
w₂ : V
h₂ : w₂ ∈ G.neighborSet v
h : f ↑⟨w₁, h₁⟩ = f ↑⟨w₂, h₂⟩
⊢ w₁ = w₂

Tactic:
exact f.inj' h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : ¬a = ⊥
⊢ Nonempty (Finpartition a)

Tactic:
· exact ⟨Finpartition.indiscrete h⟩

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
⊢ P.parts.sup id ⊓ Q.parts.sup id = a

Tactic:
rw [P.sup_parts, Q.sup_parts, inf_idem]

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

Goal state before:
pp: case refine_2.refine_1
α : 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₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ ↑(#s₂) / ↑(#s₁) ≤ 1

pp: case refine_2.refine_2
α : 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₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₂) / ↑(#t₁)

pp: case refine_2.refine_3
α : 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₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ ↑(#t₂) / ↑(#t₁) ≤ 1

Tactic:
· exact div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card hs)) (Nat.cast_nonneg _)

Goal state after:
case refine_2.refine_2
α : 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₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₂) / ↑(#t₁)

case refine_2.refine_3
α : 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₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ ↑(#t₂) / ↑(#t₁) ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #((P.nonUniforms G ε).biUnion fun x ↦
        match x with
        | (U, V) => U ×ˢ V) ≤
    ∑ x ∈ P.nonUniforms G ε, #x.1 * #x.2

Tactic:
simp_rw [← card_product]

Goal state after:
α : 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #((P.nonUniforms G ε).biUnion fun x ↦ x.1 ×ˢ x.2) ≤ ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H H' → Disjoint H.verts H'.verts

Tactic:
intro hdisj

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
⊢ Disjoint H.verts H'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
hf : Surjective ⇑f
h✝ : Nonempty W
v : V
⊢ G.minDegree ≤ G.degree v

Tactic:
← minDegree_le_degree

Goal state after:
case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
hf : Surjective ⇑f
h✝ : Nonempty W
v : V
⊢ G.minDegree ≤ G.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case refine_1
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Function.Injective fun H ↦
    { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

Tactic:
rintro ⟨⟨_, _⟩, -⟩ ⟨⟨_, _⟩, -⟩
    simp [funext_iff]

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

Goal state before:

Tactic:
_ = #G.edgeFinset - card {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} := ?_
    _ ≤ #G.edgeFinset - #(univ.image f) := Nat.sub_le_sub_left card_image_le _
    _ = #G.edgeFinset - #(Set.range f).toFinset := by rw [Set.toFinset_range]
    _ ≤ #(G.edgeFinset \ (Set.range f).toFinset) := le_card_sdiff ..
    _ = #(G.killCopies H).edgeFinset := ?_

Goal state after:
case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - G.copyCount H = #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }

case inr.calc_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #(G.edgeFinset \ (Set.range f).toFinset) = #(G.killCopies H).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
⊢ G'.degree v = 0

Tactic:
by_cases hv : v ∈ G'.verts
  · rw [← G'.coe_degree ⟨v, hv⟩]
    have := (Set.subsingleton_coe _).mpr hG
    exact G'.coe.degree_eq_zero_of_subsingleton ⟨v, hv⟩
  · exact degree_of_notMem_verts hv

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w x u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk w✝ w) (r : G.Walk v✝ x), (p✝.append q).reverseAux r = q.reverseAux (p✝.reverseAux r)
q : G.Walk w✝ w
r : G.Walk u✝ x
⊢ ((cons h p✝).append q).reverseAux r = q.reverseAux ((cons h p✝).reverseAux r)

Tactic:
exact ih q (cons h.symm r)

Goal state after:
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
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
⊢ (∃ k,
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]) ↔
    ∃ k,
      p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]

Tactic:
refine ⟨fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩,
    fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k]? = some p₁.darts[i]

case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
⊢ (p.takeUntil u h).length < p.length

Tactic:
rw [(p.length_takeUntil_le_length h).lt_iff_ne]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
⊢ (p.takeUntil u h).length ≠ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ (p.take n).Nil ↔ p.Nil ∨ n = 0

Tactic:
cases p <;> cases n <;> simp [take]

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
⊢ p.reverse.penultimate = p.snd

Tactic:
cases p <;> simp [snd, getVert_append]

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
hp : ¬p.Nil
⊢ cons ⋯ p.tail = p

Tactic:
cases p <;> simp at hp ⊢

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.tail.Nil

Tactic:
cases p <;> simp at hp ⊢

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.dropLast.Nil

Tactic:
cases p <;> simp at hp ⊢

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = w ↔ i = p.length

Tactic:
have := hp.reverse.getVert_eq_start_iff (by lia : p.reverse.length - i ≤ p.reverse.length)

Goal state after:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
⊢ p.getVert i = w ↔ i = p.length