mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case right
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)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
hα₀ : α ≫ G.map T.mor₃ = 0
⊢ ∃ a, (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) a = φ

Tactic:
suffices ∃ (β : Y ⟶ Z), β ≫ adj.homEquiv _ _ h = α by
          obtain ⟨β, hβ⟩ := this
          refine ⟨ψ + β, ?_⟩
          dsimp
          rw [add_comp, hβ, hα, add_sub_cancel]

Goal state after:
case right
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)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
hα₀ : α ≫ G.map T.mor₃ = 0
⊢ ∃ β, β ≫ (adj.homEquiv Z T.obj₃) h = α
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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
W'✝ : A
x₁ : W'✝ ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
m : W'✝ ⟶ K
hm : m ≫ ιK f₃ α = x₁
⊢ m = ⋯.choose

Tactic:
by
      have := mono_ιK hι hT hT'
      rw [← cancel_mono (ιK f₃ α), (exists_lift_ιK hι hT hT' x₁ hx₁).choose_spec, hm]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
n : ℕ
b : β
hb : b ∈ B
s t : Multiset α
x✝² : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
x✝¹ : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
x✝ : s.prod = t.prod
⊢ (map (fun x ↦ b) s).prod = (map (fun x ↦ b) t).prod

Tactic:
simp only [map_const', hs, prod_replicate, ht]

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

Goal state before:
pp: n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1

Tactic:
rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]

Goal state after:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ ((a + b) i + 1).succ ≤ d + d
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

Tactic:
← le_div_iff₀'

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

N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 0 < 2
Module: Mathlib.Combinatorics.Additive.ETransform

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

Tactic:
by
  dsimp
  rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
⊢ G.incidenceFinset v = {e ∈ G.edgeFinset | v ∈ e}

Tactic:
ext ⟨⟨⟩⟩

Goal state after:
case mk
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
a✝ : Sym2 V
fst✝ snd✝ : V
⊢ Quot.mk (Sym2.Rel V) (fst✝, snd✝) ∈ G.incidenceFinset v ↔
    Quot.mk (Sym2.Rel V) (fst✝, snd✝) ∈ {e ∈ G.edgeFinset | v ∈ e}
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

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

Tactic:
replace hab := leOfHom hab

Goal state after:
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
a b : EInt
hab✝ : a ⟶ b
hab : a ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 a ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c

Tactic:
obtain ⟨d, hd, hbd⟩ := hPR hb

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hbd : b ≤ d
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #({u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}) ≤ 2 ^ (#F - 1)

Tactic:
by
    refine (card_le_card h).trans (card_image_le.trans ?_)
    rw [card_powerset, card_erase_of_mem ht]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(P.energy G) + ε ^ 5 / 4 ≤ ↑((increment hP G ε).energy G)

Tactic:
calc
    _ = (∑ x ∈ P.parts.offDiag, (G.edgeDensity x.1 x.2 : ℝ) ^ 2 +
          #P.parts ^ 2 * (ε ^ 5 / 4) : ℝ) / #P.parts ^ 2 := by
        rw [coe_energy, add_div, mul_div_cancel_left₀]; positivity
    _ ≤ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x,
          G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ #P.parts) / #P.parts ^ 2 := ?_
    _ = (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x,
          G.edgeDensity i.1 i.2 ^ 2 : ℝ) / #(increment hP G ε).parts ^ 2 := by
        rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm,
          div_mul_eq_div_div_swap, ← sum_div]; norm_num
    _ ≤ _ := by
        rw [coe_energy]
        gcongr
        rw [← sum_biUnion pairwiseDisjoint_distinctPairs]
        exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4)) / ↑(#P.parts) ^ 2 ≤
    (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ G.Adj v₁ v₂ ∧ s(v₁, v₂) ∉ G.incidenceSet x ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x

Tactic:
mk'_mem_incidenceSet_iff

Goal state after:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
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
⊢ (G.deleteIncidenceSet x).edgeFinset = {x_1 ∈ G.edgeFinset | x ∉ x_1}

Tactic:
rw [edgeFinset_deleteIncidenceSet_eq_sdiff, sdiff_eq_filter]
  apply filter_congr
  intro _ h
  rw [incidenceFinset, Set.mem_toFinset, incidenceSet,
    Set.mem_ofPred_eq, not_and, Classical.imp_iff_right_iff]
  left
  rwa [mem_edgeFinset] at h

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x✝ : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
⊢ r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
exact this hH

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

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝ : V
⊢ x✝ ∈ (Subgraph.comap f ⊤).verts ↔ x✝ ∈ ⊤.verts

Tactic:
simp +contextual [f.map_adj]

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

Goal state before:
pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝¹ x✝ : V
⊢ (Subgraph.comap f ⊤).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
simp +contextual [f.map_adj]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ G.killCopies H = G ↔ H.Free G

Tactic:
simp only [killCopies_of_ne_bot hH, Set.disjoint_left, isContained_iff_exists_iso_subgraph,
    @forall_comm _ G.Subgraph, deleteEdges_eq_self, Set.mem_iUnion,
    not_exists, not_nonempty_iff, Nonempty.forall, Free]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ (∀ (b : G.Subgraph), ∀ a ∈ G.edgeSet, ∀ (a_2 : H ≃g b.coe), a ∉ {⋯.some}) ↔ ∀ (x : G.Subgraph), IsEmpty (H ≃g x.coe)
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ t ∉ e

Tactic:
rw [mem_sdiff, mem_incidenceFinset] at he

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset ∧ e ∉ G.incidenceSet t
⊢ t ∉ e
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset - #(G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) =
    #G.edgeFinset + G.degree s - G.degree t

Tactic:
← Nat.sub_add_comm <| card_le_card inc,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #(G.incidenceFinset t) =
    #G.edgeFinset + G.degree s - G.degree t
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {v}

Tactic:
subgraphOfAdj_symm hvw.symm

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj ⋯).neighborSet w = {v}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset - #(G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
← Nat.sub_add_comm <| card_le_card inc,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #(G.incidenceFinset t) - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
refine ⟨fun h ↦ .inr <| h (by simp_all [edge_adj]), fun hadj v' w' hvw' ↦ ?_⟩

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
hadj : v = w ∨ G.Adj v w
v' w' : V
hvw' : (edge v w).Adj v' w'
⊢ G.Adj v' w'
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : G'.Adj v w
⊢ v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
exact ⟨hs hv, hs hw, hg.2 ha⟩

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
hp : p.edges ≠ []
⊢ p.edges.head hp = s(v, p.snd)

Tactic:
simp [p.edge_firstDart, Walk.edges]

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
        simp

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 u v
h : w ∈ p.support
⊢ (p.dropUntil w h).length = p.length - List.idxOf w p.support

Tactic:
simp [dropUntil_eq_drop]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts ↔ s(u', v') ∈ p.edges

Tactic:
edges,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts ↔
    s(u', v') ∈ List.map Dart.edge p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

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

Tactic:
contrapose hsu

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
hsu : ¬1 ≤ (p.takeUntil w h).length
⊢ w = u
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ (p.concat h).penultimate = v

Tactic:
by simp [concat_eq_append, getVert_append]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ∧ #t = n ↔ ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
isClique_map_finset_iff,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (#t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n ↔ ∃ s, G.IsNClique n s ∧ map f s = t
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp
α : 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}}
⊢ G.EdgeDisjointTriangles → ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

Tactic:
rw [Sym2.forall]

Goal state after:
case mp
α : 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}}
⊢ G.EdgeDisjointTriangles → ∀ (x y : α), ¬s(x, y).IsDiag → {s | s ∈ G.cliqueSet 3 ∧ s(x, y) ∈ s.sym2}.Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg.refine_2
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∀ w ∈ p.support, w ∈ q.support → w ≠ u → w = v
⊢ 1 < p.length ∨ 1 < q.reverse.length

Tactic:
grind [length_reverse, eq_of_length_le_one]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
⊢ Injective (Path.map f hinj)

Tactic:
rintro ⟨p, hp⟩ ⟨p', hp'⟩ h
  simp only [Path.map, Subtype.mk.injEq] at h
  simp [Walk.map_injective_of_injective hinj u v h]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ε * ↑(Fintype.card α) ^ 2 ≤ ↑(#G.edgeFinset)

Tactic:
by simpa using hε.le_card_edgeFinset (by simp)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
⊢ 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

Tactic:
have hm : (0 : ℝ) ≤ 1 - (↑m)⁻¹ := sub_nonneg_of_le (inv_le_one_of_one_le₀ <| one_le_m_coe hPα)

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
⊢ 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
hx : x ∈ t
⊢ (∃ c, (x.1, x.2.1, c) ∈ t) ∧ (∃ b, (x.1, b, x.2.2) ∈ t) ∧ ∃ a, (a, x.2.1, x.2.2) ∈ t

Tactic:
exact ⟨⟨_, hx⟩, ⟨_, hx⟩, _, hx⟩

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ε * (↑(Fintype.card G) * ↑(Fintype.card G)) ≤ ↑(Fintype.card G) * ↑(Fintype.card G)
⊢ ε ≤ 1

Tactic:
mul_le_iff_le_one_left

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ε ≤ 1
⊢ ε ≤ 1

G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ε * (↑(Fintype.card G) * ↑(Fintype.card G)) ≤ ↑(Fintype.card G) * ↑(Fintype.card G)
⊢ 0 < ↑(Fintype.card G) * ↑(Fintype.card G)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A, B⁻¹] = σₘ[A, B]

Tactic:
rw [mulConst, divConst, div_inv_eq_mul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
by_contra! +distrib rfl | rfl <;> simp at h

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: n : ℕ
⊢ n.bitIndices.SortedLT

Tactic:
by
  induction n using binaryRec with
  | zero => simp [sortedLT_iff_pairwise]
  | bit b n hs =>
    suffices List.Pairwise (fun a b ↦ a < b) n.bitIndices by
      cases b <;> simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]
    exact List.Pairwise.imp (by simp) hs.pairwise

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∉ ofColex (toColex s)

Tactic:
simpa [mem_symmDiff, h hst] using max'_mem _ <| symmDiff_nonempty.2 hst

Goal state after: