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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₂) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₂) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₃) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₃) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₂₄) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₂₄) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv)

pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₃₄) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv)

Tactic:
all_goals
    ext x
    simp [Adjunction.homEquiv, yonedaEquiv_naturality]

Goal state after:
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})
⊢ ⇑(ConcreteCategory.hom (eval S α (typesGlue S hs α f))) = f

Tactic:
funext x
  apply (IsSheafFor.valid_glue _ _ _ <| ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩).trans
  convert! ConcreteCategory.congr_hom (S.map_id _) _

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
⊢ (pullFunctor F w).map
        (((pullFunctorIdIso F S).symm ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ (pullFunctorCompIso F w w' (𝟙 S) ⋯ ⋯).symm).hom.app
          D) ≫
      (pullFunctorCompIso F w' w (𝟙 S') ⋯ ⋯ ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ pullFunctorIdIso F S').hom.app
        ((pullFunctor F w).obj D) =
    𝟙 ((pullFunctor F w).obj D)

Tactic:
by
    ext j
    dsimp
    simp only [Category.id_comp, Functor.map_comp, Category.assoc]
    rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ (p' _ ≫ f _) (p' _ ≫ q' _ ≫ p' _) (p' _) (by simp)
        (by simp [w', reassoc_of% w]),
      map_eq_pullHom_assoc _ (p' j) (p' j) (p' _ ≫ q' _ ≫ p' _) (by simp) (by simp),
      D.pullHom_hom _ _ (p' j ≫ f _) (by simp) _ _ (by simp)
        (by simp [w, reassoc_of% w']) _ _ (by simp) rfl]
    dsimp
    rw [← F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc _ _ _ _ _ _ rfl rfl (by simp),
      mapComp'_comp_id_hom_app, mapComp'_id_comp_inv_app_assoc, ← Functor.map_comp_assoc,
      Cat.Hom.inv_hom_id_toNatTrans_app]
    simp [D.hom_self _ _ rfl]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ (Sieve.ofArrows X f).arrows (f' i')

Tactic:
by
      rw [h]; apply Sieve.ofArrows_mk

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 ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map ((opShiftFunctorEquivalence C n).unitIso.inv.app X).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
        (commShiftIso F n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X))

Tactic:
← cancel_mono (F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop),

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map ((opShiftFunctorEquivalence C n).unitIso.inv.app X).unop ≫
      F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop =
    (((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
          (commShiftIso F n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X))) ≫
      F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x

Tactic:
rw [← le_sub_iff_add_le', ← sub_one_mul]

Goal state after:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ (1.38 - 1) * x
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)

Tactic:
add_add_add_comm,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ #(mulETransformLeft e x).1 + #(mulETransformRight e x).1 +
      (#(mulETransformLeft e x).2 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
⊢ minOrder (ZMod n) = ↑n.minFac

Tactic:
have : Fact (1 < n) := ⟨one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn, hn₁⟩⟩
  have : (↑(n / n.minFac) : ZMod n) ≠ 0 := by
    rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]
    exact
      not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
        (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)
  refine ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
    le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_
  · rw [Nat.card_zmultiples, ZMod.addOrderOf_coe _ hn,
      gcd_eq_right (div_dvd_of_dvd n.minFac_dvd), Nat.div_div_self n.minFac_dvd hn]
  · have : Nontrivial s := s.bot_or_nontrivial.resolve_left hs
    exact WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <|
      (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd

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

Goal state before:
pp: case inr.inr.inr
α : 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)
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
replace aux2 := card_mono <| mulETransformRight.fst_mul_snd_subset g (s, t)

Goal state after:
case inr.inr.inr
α : 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)
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : Nonempty V
inst✝ : DecidableRel G.Adj
d : ℕ
h : G.IsRegularOfDegree d
⊢ G.maxDegree = d

Tactic:
simp [maxDegree, h.degree_eq, Finset.image_const]

Goal state after:
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 ↔ #t ≠ #s / #P.parts + 1

Tactic:
by
  have a := hP.card_parts_eq_average ht
  lia

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 fun i ↦ Q.parts.sup fun i' ↦ (i, i').1 ⊓ (i, i').2) = P.parts.sup id ⊓ Q.parts.sup id

Tactic:
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left]

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (P.parts.sup fun i ↦ Q.parts.sup fun i' ↦ i ⊓ i') = P.parts.sup fun i ↦ Q.parts.sup fun i_1 ↦ id i ⊓ id i_1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (↑P.parts.attach).PairwiseDisjoint fun i ↦ ((fun i ↦ Q ↑i ⋯) i).parts

Tactic:
rintro ⟨b, hb⟩ - ⟨c, hc⟩ - hbc

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ (Disjoint on fun i ↦ ((fun i ↦ Q ↑i ⋯) i).parts) ⟨b, hb⟩ ⟨c, hc⟩
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ a ∈ P.part a ↔ a ∈ s

Tactic:
simp [part, ha, choose_property (p := fun s => a ∈ s) P.parts (P.existsUnique_mem ha)]

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 α
P : Finpartition s
t : Finset α
ht : t ∈ ⊥.parts
⊢ ∃ c ∈ P.parts, t ⊆ c

Tactic:
rw [mem_bot_iff] at ht

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P✝ : Finpartition s✝
a : α
s : Finset α
P : Finpartition s
t : Finset α
ht : ∃ a ∈ s, {a} = t
⊢ ∃ c ∈ P.parts, t ⊆ c
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
bij : Function.Bijective z'
a b : ↥s
⊢ P.part ↑a = P.part ↑b ↔
    (#P.parts * ↑(f a).snd + ↑(g (f a).fst)) % #P.parts = (#P.parts * ↑(f b).snd + ↑(g (f b).fst)) % #P.parts

Tactic:
hf a b,

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
bij : Function.Bijective z'
a b : ↥s
⊢ (f a).fst = (f b).fst ↔
    (#P.parts * ↑(f a).snd + ↑(g (f a).fst)) % #P.parts = (#P.parts * ↑(f b).snd + ↑(g (f b).fst)) % #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Density

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

Tactic:
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]

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

Goal state before:
pp: case pos.refine_1
α : 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
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
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
left✝ : ∀ 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 ∈ (R.extend ⋯ ⋯ ⋯).parts, #x = m ∨ #x = m + 1

Tactic:
simp only [extend_parts, mem_insert, forall_eq_or_imp, and_iff_left hR₁, htn, hn]
      exact ite_eq_or_eq _ _ _

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v

Tactic:
nonUniforms,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ (u, v) ∈
      {x ∈ P.parts.offDiag |
        match x with
        | (u, v) => ¬G.IsUniform ε u v} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ ∃ b, ∀ a ∈ ↑(increment hP G ε).parts, #a = b ∨ #a = b + 1

Tactic:
refine ⟨m, fun A hA => ?_⟩

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : A ∈ ↑(increment hP G ε).parts
⊢ #A = m ∨ #A = m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
⊢ e ∈ Set.range (Sym2.map Subtype.val)

Tactic:
induction e using Sym2.ind with | h a b =>
  rw [Subgraph.mem_edgeSet] at he
  exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_mk ..⟩

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
⊢ ∀ {v w : W}, Relation.Map H.Adj (⇑f) (⇑f) v w → v ∈ ⇑f '' H.verts

Tactic:
by
    rintro _ _ ⟨u, v, h, rfl, rfl⟩
    exact Set.mem_image_of_mem _ (H.edge_vert 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
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ G.copyCount H = #(image Copy.toSubgraph univ)

Tactic:
rw [copyCount]
  congr
  refine Finset.coe_injective ?_
  simpa [-Copy.range_toSubgraph] using Copy.range_toSubgraph.symm

Goal state after:
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)
h : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
by
  rw [degree, Fintype.card_eq_zero_iff, isEmpty_subtype]
  intro w
  by_contra hw
  exact h hw.fst_mem

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Subgraph.coeSubgraph (Subgraph.restrict H') = H ⊓ H'

Tactic:
ext
  · simp
  · simp_rw [coeSubgraph_adj, restrict_adj]
    simp only [exists_and_left, exists_prop, inf_adj, and_congr_right_iff]
    intro h
    simp [H.edge_vert h, H.edge_vert h.symm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : p.darts ≠ []
⊢ p.darts.getLast hnil = p.lastDart ⋯

Tactic:
by
  grind [lastDart_eq, not_nil_iff_lt_length]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ p.lastDart hnil = p.darts.getLast ⋯

Tactic:
by
  grind [lastDart_eq, not_nil_iff_lt_length]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
⊢ p = q

Tactic:
refine darts_injective (Dart.toProd_injective.list_map (List.rightInverse_unzip_zip.injective ?_))

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
⊢ (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
⊢ p = q

Tactic:
refine darts_injective (Dart.toProd_injective.list_map (List.rightInverse_unzip_zip.injective ?_))
  have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl
  have : Prod.snd ∘ Dart.toProd = fun d : G.Dart ↦ d.snd := rfl
  grind [map_fst_darts, map_snd_darts]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsTrail
⊢ p₁.IsTrail

Tactic:
by
  obtain ⟨_, _, h⟩ := h
  rw [h] at h₂
  exact h₂.of_append_left.of_append_right

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsPath
⊢ p₁.IsPath

Tactic:
by
  obtain ⟨_, _, h⟩ := h
  rw [h] at h₂
  exact h₂.of_append_left.of_append_right

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
⊢ n = m

Tactic:
by_cases hn0 : n = 0

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
⊢ n = m

case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (↑(Finset.map f s) ∩ ↑(Finset.map f t)).Subsingleton

Tactic:
rw [← coe_inter, ← map_inter, coe_map, coe_inter]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (⇑f '' (↑s ∩ ↑t)).Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length

Tactic:
refine ⟨fun h ↦ ⟨h.isPath_tail, h.three_le_length⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
x✝ : p.tail.IsPath ∧ 3 ≤ p.length
h₁ : p.tail.IsPath
h₂ : 3 ≤ p.length
⊢ p.IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, ↑(#({y ∈ t | G.Adj x y})) ≤ #(G.badVertices ε s t) • (↑(#t) * (↑(G.edgeDensity s t) - ε))

Tactic:
mul_comm (#t : ℝ)

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, ↑(#({y ∈ t | G.Adj x y})) ≤ #(G.badVertices ε s t) • ((↑(G.edgeDensity s t) - ε) * ↑(#t))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁴ : α
b✝¹ : β
c✝¹ : γ
a✝³ : (a✝⁴, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝² : (a✝⁴, b✝, c✝) ∈ t
a✝¹ : α
a✝ : (a✝¹, b✝¹, c✝) ∈ t
⊢ {in₀ ?m.3431, in₁ ?m.3434, in₂ ?m.3437} = {in₀ a✝⁴, in₁ b✝¹, in₂ c✝}

Tactic:
by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3 * ↑(Fintype.card α) ^ 3 =
    (1 - 2 * (ε / 8)) * (ε / 8) ^ 3 * (↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) *
        (↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) *
      (↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)))

Tactic:
by
      ring

Goal state after: