mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℤ
⊢ ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X)) ≫
          (commShiftIso F (-n)).inv.app ((shiftFunctor C n).obj (unop X)) ≫
            F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        (shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop (op ((shiftFunctor C n).obj (unop X)))))) ≫
          (shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op ≫
            (shiftFunctorOpIso D n (-n) ⋯).hom.app (op ((shiftFunctor D n).obj (F.obj (unop X)))) ≫
              ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op

Tactic:
op_comp_assoc,

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

Tactic:
op_comp_assoc,

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 ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app ((shiftFunctor C n).obj (unop X))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X))).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        (shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop (op ((shiftFunctor C n).obj (unop X)))))) ≫
          (shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op ≫
            (shiftFunctorOpIso D n (-n) ⋯).hom.app (op ((shiftFunctor D n).obj (F.obj (unop X)))) ≫
              ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝¹ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this✝ : Mono ((adj.homEquiv Z T.obj₃) h)
this : IsIso ((adj.homEquiv Z T.obj₃) h)
⊢ (Triangle.mk (G.map T.mor₁) f g).mor₃ ≫ (shiftFunctor C 1).map (Iso.refl (Triangle.mk (G.map T.mor₁) f g).obj₁).hom =
    (asIso ((adj.homEquiv Z T.obj₃) h)).hom ≫
      (Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁)).mor₃

Tactic:
· dsimp
      rw [Functor.map_id, comp_id, homEquiv_unit, assoc, ← G.map_comp_assoc, ← h₂,
        Functor.map_comp, Functor.map_comp, assoc, unit_naturality_assoc, assoc,
        Functor.commShiftIso_hom_naturality, ← adj.shift_unit_app_assoc,
        ← Functor.map_comp, right_triangle_components, Functor.map_id, comp_id]

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 α
⊢ ∃ X₁ i δ, Triangle.mk (ι.map i) (ι.map π) δ ∈ distinguishedTriangles

Tactic:
refine ⟨K, -ιK f₃ α, f₂ ≫ inv α, ?_⟩

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 α) ∈ distinguishedTriangles
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : α → Finset β
h₁ : s.Nonempty
h₂ : ∀ j ∈ s, 0 < #(f j)
k : ℕ := s.inf' h₁ fun j ↦ #(f j)
hk : k = s.inf' h₁ fun j ↦ #(f j)
h₃ : ∀ a ∈ s, ∀ x ∈ f a, #{j | j ∈ s ∧ x ∈ f j} ≤ k
⊢ ∑ _x ∈ s, k ≤ ∑ _x ∈ s.biUnion f, k

Tactic:
calc ∑ j ∈ s, k
    _ ≤ ∑ j ∈ s, #(f j) := by gcongr with i hi; exact inf'_le _ hi
    _ = ∑ x ∈ s.biUnion f, #{j | j ∈ s ∧ x ∈ f j} := by rw [sum_card_eq_sum_biUnion_card]
    _ ≤ ∑ x ∈ s.biUnion f, k := by gcongr; grind

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

Goal state before:
pp: 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)
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
set C := {F ∈ A.powerset | (SetLike.coe F).PairwiseDisjoint (· • B)}

Goal state after:
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 ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

Tactic:
rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
      · norm_num [le_sqrt_log hN]
      · norm_num1

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N

Tactic:
← log_rpow zero_lt_two,

Goal state after:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ ↑12) ≤ log ↑N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

pp: case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

pp: case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹

Tactic:
· rw [cast_pos]
    exact hN.trans_lt' (by norm_num1)

Goal state after:
case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B ^ (n + 1))) * ↑(#A) = ↑(#(B ^ n * A * B)) * ↑(#A)

Tactic:
by rw [pow_succ, mul_left_comm, mul_assoc]

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

Goal state before:
pp: case base
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
ε : Fin 3 → ℤ
hε : ∀ (i : Fin 3), |ε i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k ^ (3 - 2) * ↑(#A)

Tactic:
simpa using h ε hε

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
⊢ ⊥ ∈ P.parts

Tactic:
← le_bot_iff.1 ((le_sup hb).trans h.le)

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
⊢ id b ∈ P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ (SimpleGraph.map (⇑f) G).edgeSet = ⇑f.sym2Map '' G.edgeSet

Tactic:
exact G.edgeSet_map f

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ #Q.parts ≤ #P.parts

Tactic:
by
  have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
  choose f hP hf using this
  rw [← card_attach]
  refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_
  exact
    Subtype.coe_injective
      (Q.disjoint.elim b.2 c.2 fun H ↦
        P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)

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
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_1 ∈ P.parts, c.1 ⊓ c.2 ≤ c_1

Tactic:
exact ⟨c.1, hc.1, inf_le_left⟩

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε'

Tactic:
refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h

Goal state after:
case refine_1
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ ↑(#s) * ε ≤ ↑(#s) * ε'

case refine_2
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ ↑(#t) * ε ≤ ↑(#t) * ε'
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:
rw [Finset.card_empty, Nat.cast_zero] at hs₂
    simpa [edgeDensity, (nonpos_of_mul_nonpos_right hs₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h : (fun G' ↦ (G'.verts, G'.spanningCoe)) G₁ = (fun G' ↦ (G'.verts, G'.spanningCoe)) G₂
⊢ G₁ = G₂

Tactic:
Prod.ext_iff

Goal state after:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₁).1 = ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₂).1 ∧
    ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₁).2 = ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₂).2
⊢ G₁ = G₂
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
n✝ : ℕ
hi : (cons h✝ p✝).length ≤ n✝ + 1
⊢ (cons h✝ p✝).getVert (n✝ + 1) = w✝

Tactic:
exact ih (Nat.succ_le_succ_iff.1 hi)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝¹ : V
x✝ : x✝¹ ∈ Set.range p.support.get
n : Fin p.support.length
h✝ : p.support.get n = x✝¹
⊢ p.getVert ↑n = x✝¹

Tactic:
by grind [getVert_eq_support_getElem, length_support]

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

Goal state before:
pp: case h₂
α : 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
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 / ↑m ≤ 1 / (100 / ε ^ 5)

Tactic:
exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' w : V
p : G.Walk u v
h : G.Adj v w
p' : G.Walk u v'
h' : G.Adj v' w
he : p.concat h = p'.concat h'
⊢ ∃ (hv : v = v'), p.copy ⋯ hv = p'

Tactic:
induction p with
  | nil =>
    cases p'
    · exact ⟨rfl, rfl⟩
    · simp only [concat_nil, concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he).symm).elim
  | cons _ _ ih =>
    rw [concat_cons] at he
    cases p'
    · simp only [concat_nil, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he)).elim
    · rw [concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      obtain ⟨rfl, rfl⟩ := ih (heq_iff_eq.mp he)
      exact ⟨rfl, rfl⟩

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

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

Tactic:
have := congr_arg₂ (y := (p.takeUntil _ h).length) getVert (p.take_spec h) rfl

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
this :
  ((p.takeUntil u h).append (p.dropUntil u h)).getVert (p.takeUntil u h).length = p.getVert (p.takeUntil u h).length
⊢ p.getVert (p.takeUntil u h).length = u
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

Tactic:
simp [isTrail_def, and_comm]

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

Tactic:
List.drop_drop

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ List.drop (min n p.length + min m (p.length - n)) p.support = List.drop (min (n + m) p.length) p.support
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ s ∈ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} ↔ s ∈ {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}

Tactic:
simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq,
      mem_cliqueSet_iff, Set.mem_ofPred_eq,
      is3Clique_iff]

Goal state after:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s ↔
    G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
⊢ (G ⊔ edge v w).Adj x y

Tactic:
exact Or.inr ⟨by by_cases x = v <;> aesop, hxy⟩

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
t : Finset ↑s
n : ℕ
⊢ (induce s G).IsNClique n t ↔ G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)

Tactic:
by
  simp [isNClique_iff, isClique_induce_iff]

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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsCycle

Tactic:
· refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩
      exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset_edges hup he

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

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ {a, b, c} = {d, e, f}

Tactic:
refine hG (Sym2.mk_isDiag_iff.not.2 hgh) ⟨⟨a, b, c, ?_⟩, by simpa using And.intro hg₁ hh₁⟩
      ⟨⟨d, e, f, ?_⟩, by simpa using And.intro hg₂ hh₂⟩

Goal state after:
case mpr.refine_1
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

case mpr.refine_2
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj d e ∧ G.Adj d f ∧ G.Adj e f ∧ {d, e, f} = {d, e, f}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} 0 ↔ 1 < 0

Tactic:
simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

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

Goal state before:
pp: case succ.zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} (0 + 1) ↔ 1 < 0 + 1

Tactic:
simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

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

Goal state before:
pp: case succ.succ
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} (n + 1 + 1) ↔ 1 < n + 1 + 1

Tactic:
simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

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

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n < 2 * k * (n / k)

Tactic:
by
  rw [mul_assoc, two_mul, ← add_lt_add_iff_right (n % k), add_right_comm, add_assoc,
    mod_add_div n k, add_comm, add_lt_add_iff_right]
  apply (mod_lt n hk).trans_le
  simpa using Nat.mul_le_mul_left k ((Nat.one_le_div_iff hk).2 hn)

Goal state after:
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 γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ #((graph t).cliqueFinset 3) = #t

Tactic:
by
  rw [cliqueFinset_eq_map, card_map]

Goal state after: