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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
⊢ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x (P₁ ⊗ P₂) ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯ ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂) ⋯ ▷ Φ.presheafFiber.obj P₃ ≫
        (α_ (Φ.presheafFiber.obj P₁) (Φ.presheafFiber.obj P₂) (Φ.presheafFiber.obj P₃)).hom =
    Φ.presheafFiber.map (α_ P₁ P₂ P₃).hom ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x (P₂ ⊗ P₃)) ⋯ ≫
        Φ.presheafFiber.obj P₁ ◁ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯

Tactic:
ext X x

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
⊢ Φ.toPresheafFiber X x ((P₁ ⊗ P₂) ⊗ P₃) ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x (P₁ ⊗ P₂) ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯ ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂) ⋯ ▷
            Φ.presheafFiber.obj P₃ ≫
          (α_ (Φ.presheafFiber.obj P₁) (Φ.presheafFiber.obj P₂) (Φ.presheafFiber.obj P₃)).hom =
    Φ.toPresheafFiber X x ((P₁ ⊗ P₂) ⊗ P₃) ≫
      Φ.presheafFiber.map (α_ P₁ P₂ P₃).hom ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x (P₂ ⊗ P₃)) ⋯ ≫
          Φ.presheafFiber.obj P₁ ◁
            Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯
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
M N : ↑(F.obj { as := op S })
φ : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯)
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map (↑φ i₁) ≫ ((F.toDescentData f).obj N).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f).obj M).hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (↑φ i₂)

Tactic:
by
        have := φ.property i₁ i₂ (Over.mk q) (Over.homMk f₁) (Over.homMk f₂) (by cat_disch)
        simp_all [map_eq_pullHom]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ IsPullback ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
    (𝒞.χ₀ (underlying.obj ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject))) (𝒞.χ i) 𝒞.truth

Tactic:
refine (IsPullback.of_hasPullback 𝒞.truth (𝒞.χ i)).flip.of_iso
    (underlyingIso _).symm (Iso.refl _) (Iso.refl _) (Iso.refl _)
    ?_ (𝒞.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ (Iso.refl X).hom =
    (underlyingIso (pullback.snd ((MonoOver.forget 𝒞.Ω).obj (MonoOver.mk 𝒞.truth)).hom (𝒞.χ i))).symm.hom ≫
      ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case e
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
𝒞 : Subobject.Classifier C
⊢ (Subobject.presheaf C).RepresentableBy ?mp.Y

pp: case mp.Y
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
𝒞 : Subobject.Classifier C
⊢ C

Tactic:
exact 𝒞.representableBy

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
hχ' : IsPullback m ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F) χ' (truth C)
⊢ χ' = χ m

Tactic:
ext X x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
hχ' : IsPullback m ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F) χ' (truth C)
X : Cᵒᵖ
x : G.obj X
⊢ (ConcreteCategory.hom (χ'.app X)).toFun x = (ConcreteCategory.hom ((χ m).app X)).toFun x
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
h : (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤
⊢ ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a

Tactic:
obtain ⟨z, hz⟩ := h₃ _ _ h

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
h : (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤
z : F.obj (Opposite.op Y)
hz : (ConcreteCategory.hom (m.app (Opposite.op Y))) z = (ConcreteCategory.hom (G.map f.op)) x
⊢ ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
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
X Y : C
⊢ ∀ (x : Retract X Y), P.triangEnvelope Y → P.triangEnvelope X

Tactic:
r

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
X Y : C
r : Retract X Y
⊢ P.triangEnvelope Y → P.triangEnvelope X
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
ht : t.Nonempty
hb : ↑(#s) ≤ #t • b
⊢ ∃ y ∈ t, ↑(#({x ∈ s | f x = y})) ≤ b

Tactic:
simp_rw [cast_card] at hb ⊢
  refine
    exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb

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

Goal state before:
pp: n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ x_1, ↑(x x_1 ^ 2)) = √↑k

Tactic:
← cast_sum,

Goal state after:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √↑(∑ x_1, x x_1 ^ 2) = √↑k
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∈ F
⊢ a ∈ F * (B / B)

Tactic:
exact subset_mul_left _ hB.one_mem_div hau

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

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 ≤ log (↑N ^ (↑(nValue N))⁻¹ / 2)

pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹ / 2

Tactic:
log_div _ two_ne_zero,

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 ≤ log (↑N ^ (↑(nValue N))⁻¹) - log 2

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (↑(nValue N))⁻¹ ≠ 0

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹ / 2
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hd
N : ℕ
hN : 4096 ≤ N
⊢ 1 < ↑N

Tactic:
rw [one_lt_cast]

Goal state after:
case hd
N : ℕ
hN : 4096 ≤ N
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h₁
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
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N

Tactic:
rw [one_lt_cast]

Goal state after:
case h₁
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
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h₂
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
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N

Tactic:
rw [one_lt_cast]

Goal state after:
case h₂
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
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]

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

Goal state before:
pp: case refine_2
α : 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 : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c * g⁻¹ ∈ a⁻¹ • ↑s

Tactic:
· rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]

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 y : G
⊢ Set.RightInvOn (fun ab' ↦ x •> ab'.1) (fun z ↦ (x⁻¹ * z, z⁻¹ * y)) ↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x⁻¹ * y})

Tactic:
simp +contextual [Set.LeftInvOn, ← eq_mul_inv_iff_mul_eq, mul_assoc]

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
s x : G
⊢ (A <• s).convolution B x = A.convolution (s •> B) x

Tactic:
by
  nth_rw 1 [← inv_inv B, ← inv_inv (s • B), inv_smul_finset_distrib s B, ← card_inter_smul,
    ← card_inter_smul, smul_comm]
  simp [← card_smul_finset (op s) (A ∩ _), smul_finset_inter]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∀ {d : G.Dart} {u v : V}, d.edge = s(u, v) ↔ d.toProd.1 = u ∧ d.toProd.2 = v ∨ d.toProd.1 = v ∧ d.toProd.2 = u

Tactic:
rintro ⟨⟨a, b⟩, h⟩ u v
  rw [dart_edge_eq_mk'_iff]
  simp

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

Goal state before:
pp: case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A * A * A⁻¹)) ≤ K ^ 2 * ↑(#A)

pp: case h₂
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A ^ 2)) ≤ K * ↑(#A)

Tactic:
· exact small_pos_pos_neg_mul hA

Goal state after:
case h₂
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A ^ 2)) ≤ K * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case right
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ Sym2.map ⇑f s(a, b) = s(x✝, y✝)

Tactic:
Sym2.map_mk,

Goal state after:
case right
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ s(f a, f b) = s(x✝, y✝)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h.mpr.h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ y✝¹ : W
x✝ y✝ : V
hadj : s(x✝, y✝) ∈ G.edgeSet
he : Sym2.map ⇑f s(x✝, y✝) = s(x✝¹, y✝¹)
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹

Tactic:
Sym2.map_mk,

Goal state after:
case h.mpr.h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ y✝¹ : W
x✝ y✝ : V
hadj : s(x✝, y✝) ∈ G.edgeSet
he : s(f x✝, f y✝) = s(x✝¹, y✝¹)
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

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

Tactic:
hg,

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ Fintype.card ↑(G.commonNeighbors v w) < G.degree v

Tactic:
← Set.toFinset_card

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ #(G.commonNeighbors v w).toFinset < G.degree v
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
b : EInt
hab✝ : ⊥ ⟶ b
hab : ⊥ ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 ⊥ ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

Tactic:
induction b using WithBotTop.rec <;> simp at hab <;>
        dsimp [eTruncGE, eTruncLT] <;>
        simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: case coe
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
b : EInt
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ b
hab : WithBotTop.coe a✝ ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

Tactic:
induction b using WithBotTop.rec <;> simp at hab <;>
        dsimp [eTruncGE, eTruncLT] <;>
        simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ (↑(Finset.map { toFun := singleton, inj' := ⋯ } s)).PairwiseDisjoint id

Tactic:
by
        rw [Finset.coe_map]
        exact Finset.pairwiseDisjoint_range_singleton.subset (Set.image_subset_range _ _)

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 : Finset α
t : Finset β
⊢ #(interedges r s t) + #(interedges (fun x y ↦ ¬r x y) s t) = #s * #t

Tactic:
← card_product,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #(interedges r s t) + #(interedges (fun x y ↦ ¬r x y) s t) = #(s ×ˢ t)
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ ↑(#(interedges r ∅ t)) / (↑(#∅) * ↑(#t)) = 0

Tactic:
Finset.card_empty,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ ↑(#(interedges r ∅ t)) / (↑0 * ↑(#t)) = 0
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
⊢ ↑(#(interedges r s ∅)) / (↑(#s) * ↑(#∅)) = 0

Tactic:
Finset.card_empty,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
⊢ ↑(#(interedges r s ∅)) / (↑(#s) * ↑0) = 0
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#∅)
⊢ |↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

Tactic:
Finset.card_empty,

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑0
⊢ |↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#∅)
⊢ |↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

Tactic:
Finset.card_empty,

Goal state after:
case inr.inl
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑0
⊢ |↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
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 α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ⊥.nonUniforms G ε = ∅

Tactic:
eq_empty_iff_forall_notMem

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ∀ (x : Finset α × Finset α), x ∉ ⊥.nonUniforms G ε
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 α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ↑(#∅) ≤ ↑(#A * (#A - 1)) * ε

Tactic:
Finset.card_empty,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ↑0 ≤ ↑(#A * (#A - 1)) * ε
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t

Tactic:
← card_product,

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #(G.interedges s t) + #(Gᶜ.interedges s t) = #(s ×ˢ t)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case e_a
α : 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
⊢ #P.parts.attach = #P.parts

Tactic:
card_attach

Goal state after:
case e_a
α : 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
⊢ #P.parts = #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
h_notMem : x ∉ {x}ᶜ
⊢ Fintype.card ↑(induce {x}ᶜ (G.deleteIncidenceSet x)).edgeSet = Fintype.card ↑(G.deleteIncidenceSet x).edgeSet

Tactic:
← Set.toFinset_card

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ #(induce {x}ᶜ (G.deleteIncidenceSet x)).edgeSet.toFinset = #(G.deleteIncidenceSet x).edgeSet.toFinset
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: 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
⊢ G.minDegree ≤ H.minDegree

Tactic:
cases isEmpty_or_nonempty W

Goal state after:
case inl
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✝ : IsEmpty W
⊢ G.minDegree ≤ H.minDegree

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
⊢ G.minDegree ≤ H.minDegree