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₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂))
⊢ (F.map f₁.op.toLoc).toFunctor.map ((F.map (p' j₁).op.toLoc).toFunctor.map (φ.hom (α j₁))) ≫
      pullFunctorObjHom w D₂ (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj (α j₂)) ≫
          (F.map f₂.op.toLoc).toFunctor.map ((F.map (p' j₂).op.toLoc).toFunctor.map (φ.hom (α j₂)))

Tactic:
pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)

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₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂))
⊢ (F.map f₁.op.toLoc).toFunctor.map ((F.map (p' j₁).op.toLoc).toFunctor.map (φ.hom (α j₁))) ≫
      (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj (α j₁)) ≫
        D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj (α j₂)) ≫
          (F.map f₂.op.toLoc).toFunctor.map ((F.map (p' j₂).op.toLoc).toFunctor.map (φ.hom (α j₂)))
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (functorEnrichedHom A F G ⋙ coyoneda.obj (op M))

Tactic:
Presieve.isSheaf_iff_of_nat_equiv
    (functorEnrichedHomCoyonedaObjEquiv M F G)
    (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
⊢ ∀ {X_1 : Over X},
    ∀ R ∈ (J.over X) X_1,
      ∀ (x_1 : (FunctorToTypes.fromOverFunctor Φ.fiber x).obj X_1),
        ∃ Y f,
          ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f)) y = x_1

Tactic:
rintro U R hR ⟨u, hu⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
U : Over X
R : Sieve U
hR : R ∈ (J.over X) U
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f)) y = ⟨u, hu⟩
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S₀ : C
S : Over S₀
R : Sieve S
hF : F.IsPrestackFor ((Sieve.overEquiv S) R).arrows
M N : ↑(F.obj { as := op S₀ })
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows

Tactic:
rw [isPrestackFor_iff_isSheafFor'] at hF

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S₀ : C
S : Over S₀
R : Sieve S
hF :
  ∀ ⦃S₀_1 : C⦄ (M N : ↑(F.obj { as := op S₀_1 })) (a : S.left ⟶ S₀_1),
    Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm ((Sieve.overEquiv S) R)).arrows
M N : ↑(F.obj { as := op S₀ })
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
⊢ (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) (⋯.amalgamate a ⋯)

Tactic:
· refine (hG _ hf).ext fun Z f' hf' => ?_
    rw [← NatTrans.naturality_apply, (hF _ hf).valid_glue _ _ hf', ← (ha _ _ _),
      op_comp, Functor.map_comp_apply]

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

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι π
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
hQ : 𝟙 Q = 0
this : IsIso α
⊢ Triangle.mk (ι.map (-ιK f₃ α)) (ι.map π) (f₂ ≫ inv α) ∈ distinguishedTriangles

Tactic:
rw [rotate_distinguished_triangle]

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι π
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
hQ : 𝟙 Q = 0
this : IsIso α
⊢ (Triangle.mk (ι.map (-ιK f₃ α)) (ι.map π) (f₂ ≫ inv α)).rotate ∈ distinguishedTriangles
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Tactic:
coe_map

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ ThreeGPFree ↑(map (mulLeftEmbedding a) u)

Tactic:
coe_map

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

Tactic:
← rpow_natCast

Goal state after:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hd
N : ℕ
hN : 4096 ≤ N
⊢ 0 < √(log ↑N)

Tactic:
Real.sqrt_pos

Goal state after:
case hd
N : ℕ
hN : 4096 ≤ N
⊢ 0 < log ↑N
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case insert
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
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)

Tactic:
have h₀ : {x} * A' = {x} * A ∩ (C * A) := by
      rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]

Goal state after:
case insert
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)
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A * B⁻¹) * #(B / C)

Tactic:
← card_inv B,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B⁻¹ ≤ #(A * B⁻¹) * #(B / C)
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 : ℕ
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
have hA' : A ∈ A.powerset.erase ∅ := mem_erase_of_ne_of_mem hA.ne_empty (mem_powerset_self _)

Goal state after:
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 ∅
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : Disjoint t (g⁻¹ • t)
⊢ #s + #(g⁻¹ • t) ≤ #(s * t) + 1

Tactic:
grw [hst, ← card_union_of_disjoint hgt]

Goal state after:
case inr.inr.inr.inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : Disjoint t (g⁻¹ • t)
⊢ #(t ∪ g⁻¹ • t) ≤ #(s * t) + 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
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (#{w | Odd (G.degree w)} - 1)

Tactic:
refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩
    lia

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
⊢ G = ⊥

Tactic:
rw [eq_bot_iff_isIsolated]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
⊢ ∀ (v : V), G.IsIsolated v
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ #s / #P.parts + 1

Tactic:
rw [← P.sum_card_parts]
  exact Finset.EquitableOn.le_add_one hP ht

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
⊢ {e ∈ G.edgeFinset | e.toFinset ⊆ s} = G.edgeFinset ∩ s.sym2

Tactic:
simp [subset_iff, ← mem_sym2_iff, filter_mem_eq_inter]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ b

Tactic:
P.disjoint.eq_of_le hb hd (P.ne_bot hb) (hbc.trans hcd)

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ d
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
hb : b ∈ (if ha : a = ⊥ then (Finpartition.empty α).copy ⋯ else indiscrete ha).parts
⊢ b ∈ {a}

Tactic:
split_ifs at hb

Goal state after:
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : a = ⊥
hb : b ∈ ((Finpartition.empty α).copy ⋯).parts
⊢ b ∈ {a}

case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : ¬a = ⊥
hb : b ∈ (indiscrete h✝).parts
⊢ b ∈ {a}
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ (I.biUnion fun i ↦ (P i).parts).sup id = I.sup a

Tactic:
by
    rw [sup_biUnion]
    exact sup_congr rfl fun i _ => (P i).sup_parts

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₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 1 - edgeDensity (fun x y ↦ ¬r x y) s₁ t₁ - (1 - edgeDensity (fun x y ↦ ¬r x y) s₂ t₂) ≤
    1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))

Tactic:
sub_sub_sub_cancel_left

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₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity (fun x y ↦ ¬r x y) s₂ t₂ - edgeDensity (fun x y ↦ ¬r x y) s₁ t₁ ≤ 1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
rcases h2 with hl | hr

Goal state after:
case inl
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
⊢ H.Adj u v ↔ H.Adj w x

case inr
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
hv : ¬G.IsIsolated v
⊢ G.degree v ≤ (induce s G).maxDegree

Tactic:
grw [← degree_le_maxDegree _ ⟨v, h <| G.mem_support_iff_not_isIsolated.mpr hv⟩,
    degree_induce_of_neighborSet_subset <| G.neighborSet_subset_support v |>.trans h]

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

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

Tactic:
rw [← Subgraph.image_coe_edgeSet_coe] at this

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)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 V
he : e = hG'.some
this : e ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) G').coe.edgeSet
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (Subgraph.restrict (Subgraph.coeSubgraph G'')).Adj x✝¹ x✝ ↔ G''.Adj x✝¹ x✝

Tactic:
rw [restrict_adj, coeSubgraph_adj]

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (G'.Adj ↑x✝¹ ↑x✝ ∧ ∃ (hv : ↑x✝¹ ∈ G'.verts) (hw : ↑x✝ ∈ G'.verts), G''.Adj ⟨↑x✝¹, hv⟩ ⟨↑x✝, hw⟩) ↔ G''.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
n : ℕ
⊢ (Walk.map f p).getVert n = f (p.getVert n)

Tactic:
induction p generalizing n

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
n : ℕ
⊢ (Walk.map f nil).getVert n = f (nil.getVert n)

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (Walk.map f p✝).getVert n = f (p✝.getVert n)
n : ℕ
⊢ (Walk.map f (cons h✝ p✝)).getVert n = f ((cons h✝ p✝).getVert n)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
p' : G.Walk u✝ w✝
h : Walk.map f (cons h✝ p✝) = Walk.map f p'
⊢ cons h✝ p✝ = p'

Tactic:
cases p' with

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

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

Tactic:
simp [ih, Nat.succ_add, add_assoc]

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

Goal state before:
pp: case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
⊢ List.count u (if hx : u✝ = u then hx ▸ nil else cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
split_ifs with h' <;> rw [eq_comm] at h'

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : u✝ = u
h' : u = u✝
⊢ List.count u (h'✝ ▸ nil).support = 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1