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
X : C
x : Φ.fiber.obj X
| Φ.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₃) ⋯

Tactic:
simp only [toPresheafFiber_naturality_assoc, toPresheafFiber_presheafFiberDesc_assoc,
        tensorHom_def_assoc, ← MonoidalCategory.whiskerLeft_comp,
        toPresheafFiber_presheafFiberDesc]

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
| (α_ P₁ P₂ P₃).hom.app (Opposite.op X) ≫
    Φ.toPresheafFiber X x P₁ ▷ (P₂.obj (Opposite.op X) ⊗ P₃.obj (Opposite.op X)) ≫
      Φ.presheafFiber.obj P₁ ◁ (Φ.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
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
X✝ Y✝ : ↑(F.obj { as := op S })
f : X✝ ⟶ Y✝
⊢ (F.toDescentData f✝ ⋙ pullFunctor F w).map f ≫
      (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app Y✝) ⋯).hom =
    (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app X✝) ⋯).hom ≫
      ((F.map p.op.toLoc).toFunctor ⋙ F.toDescentData f').map f

Tactic:
ext i
      exact (F.isoMapOfCommSq (CommSq.mk (w i)).op.toLoc).inv.toNatTrans.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
X : C
⊢ ∀ R ∈ K.coverings X, Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor R

Tactic:
R

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
X : C
R : Presieve X
⊢ R ∈ K.coverings X → Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor R
Module: Mathlib.CategoryTheory.Subobject.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Subobject (Opposite.unop X✝)
⊢ (ConcreteCategory.hom (↾(pullback (x✝² ≫ x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (↾(pullback x✝².unop).obj ≫ ↾(pullback x✝¹.unop).obj)).toFun x✝

Tactic:
simp [pullback_comp]

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
S : C
w✝³ : Type (max u v)
w✝² : w✝³ → C
f : (i : w✝³) → w✝² i ⟶ S
w✝¹ : Type (max u v)
w✝ : w✝¹ → C
f' : (i : w✝¹) → w✝ i ⟶ S
h : Sieve.generate (Presieve.ofArrows w✝² f) = Sieve.generate (Presieve.ofArrows w✝ f')
⊢ (Sieve.ofArrows (fun f_1 ↦ f_1.obj.left) fun f_1 ↦ f_1.obj.hom) =
    Sieve.ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom

Tactic:
simpa only [Sieve.ofArrows_category']

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X✝ X'✝ : C
x✝¹ : X✝ ⟶ X'✝
x✝ : X'✝ ⟶ 𝒞.Ω
⊢ { toFun := fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject, invFun := fun x ↦ 𝒞.χ (arrow x), left_inv := ⋯,
        right_inv := ⋯ }
      (x✝¹ ≫ x✝) =
    (ConcreteCategory.hom ((Subobject.presheaf C).map x✝¹.op))
      ({ toFun := fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject, invFun := fun x ↦ 𝒞.χ (arrow x), left_inv := ⋯,
          right_inv := ⋯ }
        x✝)

Tactic:
simp [pullback_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: case h₁
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
X✝ Y✝ : (A ⊕ A') ⊕ T ⥤ B
f✝ : X✝ ⟶ Y✝
x✝ : A
⊢ f✝.app (Sum.inl (Sum.inl x✝)) ≫
      𝟙 (Y✝.obj (Sum.inl (Sum.inl x✝))) ≫
        Y✝.map ((sum.inlCompInverseAssociator A A' T).hom.app x✝) ≫ 𝟙 (Y✝.obj (Sum.inl (Sum.inl x✝))) =
    (𝟙 (X✝.obj (Sum.inl (Sum.inl x✝))) ≫
        X✝.map ((sum.inlCompInverseAssociator A A' T).hom.app x✝) ≫ 𝟙 (X✝.obj (Sum.inl (Sum.inl x✝)))) ≫
      f✝.app (Sum.inl (Sum.inl x✝))

Tactic:
simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: case h₂.h₁
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
X✝ Y✝ : (A ⊕ A') ⊕ T ⥤ B
f✝ : X✝ ⟶ Y✝
x✝ : A'
⊢ f✝.app (Sum.inl (Sum.inr x✝)) ≫
      𝟙 (Y✝.obj (Sum.inl (Sum.inr x✝))) ≫
        𝟙 (Y✝.obj (Sum.inl (Sum.inr x✝))) ≫
          Y✝.map ((sum.inlCompInrCompInverseAssociator A A' T).hom.app x✝) ≫ 𝟙 (Y✝.obj (Sum.inl (Sum.inr x✝))) =
    (𝟙 (X✝.obj (Sum.inl (Sum.inr x✝))) ≫
        𝟙 (X✝.obj (Sum.inl (Sum.inr x✝))) ≫
          X✝.map ((sum.inlCompInrCompInverseAssociator A A' T).hom.app x✝) ≫ 𝟙 (X✝.obj (Sum.inl (Sum.inr x✝)))) ≫
      f✝.app (Sum.inl (Sum.inr x✝))

Tactic:
simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: case h₂
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
X✝ Y✝ : (A ⊕ A') ⊕ T ⥤ B
f✝ : X✝ ⟶ Y✝
x✝ : T
⊢ f✝.app (Sum.inr x✝) ≫
      𝟙 (Y✝.obj (Sum.inr x✝)) ≫
        𝟙 (Y✝.obj (Sum.inr x✝)) ≫ Y✝.map ((sum.inrCompInrCompInverseAssociator A A' T).hom.app x✝) =
    (𝟙 (X✝.obj (Sum.inr x✝)) ≫
        𝟙 (X✝.obj (Sum.inr x✝)) ≫ X✝.map ((sum.inrCompInrCompInverseAssociator A A' T).hom.app x✝)) ≫
      f✝.app (Sum.inr x✝)

Tactic:
simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

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

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback ((sheafToPresheaf J (Type (max u v))).map m)
    ((sheafToPresheaf J (Type (max u v))).map ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    ((sheafToPresheaf J (Type (max u v))).map (χ m)) ((sheafToPresheaf J (Type (max u v))).map (truth J))

Tactic:
simp only [ObjectProperty.ι_obj, terminal_obj, Ω_obj, ObjectProperty.ι_map, χ_hom, truth_hom]
    apply IsPullback.of_right _
      ((cancel_mono ((closedSieves J).ι)).mp (by simpa using Presheaf.comp_χ_eq _))
      (.of_horiz_isIso_mono ⟨_⟩ : IsPullback (𝟙 _) _ (Presheaf.χ m.hom) (closedSieves J).ι)
    · simp only [Category.comp_id]
      exact Presheaf.isPullback_χ_truth m.hom
    · simp_all

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
n : ℕ
⊢ P.triangEnvelopeIter 0 ≤ P.triangEnvelopeIter n

Tactic:
exact P.monotone'_triangEnvelopeIter (Nat.zero_le n)

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

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

Tactic:
triangEnvelopeIter_add' P rfl

Goal state after:
case h
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
m : ℕ
hm : P.triangEnvelopeIter m T.obj₃
⊢ ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m)).retractClosure T.obj₂
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
⊢ ThreeGPFree (insert a s) ↔
    ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a

Tactic:
by
  refine ⟨fun hs ↦ ⟨hs.mono (subset_insert _ _),
    fun b hb c hc ↦ hs (Or.inl rfl) (Or.inr hb) (Or.inr hc),
    fun b hb c hc ↦ hs (Or.inr hb) (Or.inl rfl) (Or.inr hc)⟩, ?_⟩
  rintro ⟨hs, ha, ha'⟩ b hb c hc d hd h
  rw [mem_insert_iff] at hb hc hd
  obtain rfl | hb := hb <;> obtain rfl | hc := hc
  · rfl
  all_goals obtain rfl | hd := hd
  · exact (ha' hc hc h.symm).symm
  · exact ha hc hd h
  · exact mul_right_cancel h
  · exact ha' hb hd h
  · obtain rfl := ha hc hb ((mul_comm _ _).trans h)
    exact ha' hb hc h
  · exact hs hb hc hd h

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

Goal state before:
pp: k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
x : ℕ
hx : x ≤ k
⊢ ↑x ∈ Iic ↑k ∧ ↑↑x = x

Tactic:
simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn, hx.trans_lt]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hK : ↑(#K) ≤ 1
hKA : A ^ 2 ⊆ ↑K • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
simp only [Nat.cast_le_one, Finset.card_le_one_iff_subset_singleton,
        Finset.subset_singleton_iff] at hK

Goal state after:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hKA : A ^ 2 ⊆ ↑K • A
hK : ∃ x, K = ∅ ∨ K = {x}
⊢ ∃ x, A * A ⊆ x • A
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ G.edgeSet
⊢ #{d | d.edge = e} = 2

Tactic:
obtain ⟨v, w⟩ := e

Goal state after:
case mk
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
⊢ #{d | d.edge = Quot.mk (Sym2.Rel V) (v, w)} = 2
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
⊢ G.maxDegree ≤ k

Tactic:
cases isEmpty_or_nonempty V
  · simp
  · obtain ⟨_, hv⟩ := G.exists_maximal_degree_vertex
    exact hv ▸ h _

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree

Tactic:
exact he.elim fun v ↦ (minDegree_le_degree _ v).trans (degree_le_maxDegree _ v)

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb : b ∈ ⊤.parts
⊢ b ∈ {a}

Tactic:
have hb : b ∈ Finpartition.parts (dite _ _ _) := hb

Goal state after:
α : 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}
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Disjoint (id b) a

Tactic:
disjoint_comm

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Disjoint a (id b)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ id b ⊔ a = c

Tactic:
id,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ b ⊔ a = c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
x✝ : a ∈ x
⊢ ∃ i ∈ x, a ∈ x ∧ s i a

Tactic:
use a

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 α
F : Finset (Finset α)
x : Finset α
hx : x ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset
y : Finset α
hy : y ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
⊢ x = y

Tactic:
mem_image

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = x
y : Finset α
hy : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = y
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
⊢ x = y
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R

Tactic:
id,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : t ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset
⊢ id t ⊆ s

Tactic:
mem_image

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t
⊢ id t ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 1 / (ε / 4) ≤ ↑(#P.parts)

pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 0 < ε / 4

Tactic:
one_div_div

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 4 / ε ≤ ↑(#P.parts)

case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 0 < ε / 4
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
obtain hα | hα := le_total (card α) (bound ε l)

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : (a ∈ s(v, w)) = (a ∈ s(a, b))
⊢ a ∈ {v, w}

Tactic:
simp only [Sym2.mem_iff, true_or, eq_iff_iff, iff_true] at h

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : a = v ∨ a = w
⊢ a ∈ {v, w}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ (G.singletonSubgraph v).verts ⊆ H.verts

Tactic:
singletonSubgraph_verts,

Goal state after:
case left
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ {v} ⊆ H.verts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
⊢ #(equitabilise this).parts = n

Tactic:
rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 / (ε ^ 5 / (50 * 2)) ≤ ↑m + 1

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 0 < ε ^ 5 / (50 * 2)

Tactic:
one_div_div

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 50 * 2 / ε ^ 5 ≤ ↑m + 1

α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 0 < ε ^ 5 / (50 * 2)
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), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝

Tactic:
· simp! only
      split_ifs with h' <;> subst_vars <;> simp [*]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
⊢ s(u', v') ∈ p.edges

Tactic:
have := h.elim adj_of_infix_support (adj_of_infix_support · |>.symm)

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
this : G.Adj u' v'
⊢ s(u', v') ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.edges.Nodup
h : (cons h✝ p').support.Nodup
⊢ (cons h✝ p').edges.Nodup

Tactic:
simp only [support_cons, List.nodup_cons, edges_cons] at h ⊢
    exact ⟨(h.1 <| fst_mem_support_of_mem_edges p' ·), ih h.2⟩

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
n m : ℕ
⊢ (p.drop n).getVert m = p.getVert (n + m)

Tactic:
induction p generalizing n <;> cases n <;> simp [*, drop, add_right_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeFinset

Tactic:
refine mem_edgeFinset.mpr ?_

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (SimpleGraph.map (⇑f) G).EdgeDisjointTriangles

Tactic:
by
  rw [EdgeDisjointTriangles, cliqueSet_map (by simp : 3 ≠ 1),
    (Finset.map_injective f).injOn.pairwise_image]
  classical
  rintro s hs t ht hst
  dsimp [Function.onFun]
  rw [← coe_inter, ← map_inter, coe_map, coe_inter]
  exact (hG hs ht hst).image _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(u, w) ∈ p.edges
hnil : ¬p.Nil
⊢ w = p.snd

Tactic:
← cons_tail_eq _ hnil,

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : s(u, w) ∈ (cons ⋯ p.tail).edges
⊢ w = p.snd
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₂⟩ ↦ ?_⟩
  cases p with
  | nil => simp_all
  | cons h' p =>
    simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
    refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
    have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
    have := p.isPath_iff_injective_get_support.mp h₁ this
    lia

Goal state after: