mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : IsTriangulated C
a b : EInt
hab : b ≤ a
⊢ IsIso (t.eTruncLTLTToLT a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

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
inst✝ : IsTriangulated C
a b : EInt
hab : b ≤ a
⊢ ∀ (X : C), IsIso ((t.eTruncLTLTToLT a b).app X)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ ∀ x ∈ ⊥.parts, #x = 0 ∨ #x = 0 + 1

Tactic:
by simp

Goal state after:
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
inst✝ : IsTriangulated C
a b : EInt
⊢ IsIso (t.eTruncLTGELTSelfToLTGE a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

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
inst✝ : IsTriangulated C
a b : EInt
⊢ ∀ (X : C), IsIso ((t.eTruncLTGELTSelfToLTGE a b).app X)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ t ⊂ ⊥,
    ∀ {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
P : Finpartition ⊥
⊢ ∀ x ∈ (Finpartition.empty (Finset α)).parts, #x = m ∨ #x = m + 1

Tactic:
by simp

Goal state after:
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
inst✝ : IsTriangulated C
a b✝ b : EInt
X : C
⊢ IsIso (t.eTruncLTGELTSelfToGELT a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

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
inst✝ : IsTriangulated C
a b✝ b : EInt
X : C
⊢ ∀ (X : C), IsIso ((t.eTruncLTGELTSelfToGELT a b).app X)
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
inst✝ : IsTriangulated C
a b✝ b : EInt
X✝ X : C
⊢ IsZero ((t.eTruncGE.obj ⊤).obj ((t.eTruncLT.obj b).obj X))

Tactic:
by simp

Goal state after:
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
inst✝ : IsTriangulated C
a b✝ b : EInt
X✝ X : C
⊢ IsZero ((t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊤).obj X)

Tactic:
by simp

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

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

Tactic:
by simp

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 : G.IsUniform 0 s t
⊢ ↑(#s) * 0 ≤ ↑(#∅)

Tactic:
by simp

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 : G.IsUniform 0 s t
⊢ ↑(#t) * 0 ≤ ↑(#∅)

Tactic:
by simp

Goal state after:
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₁) ≤ 0
⊢ |↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

Tactic:
simpa [edgeDensity, (nonpos_of_mul_nonpos_right hs₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'

Goal state after:
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
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ #(increment hP G ε).parts = stepBound #P.parts

Tactic:
have hPα' : stepBound #P.parts ≤ card α := by grw [← hPα, stepBound]; gcongr; simp

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
⊢ #(increment hP G ε).parts = stepBound #P.parts
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 α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
⊢ 1 ≤ 4

Tactic:
by simp

Goal state after:
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 α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
⊢ 16 > 0

Tactic:
by simp

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

Goal state before:
pp: case neg.refine_1
α : 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 α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ t ≤ #(increment hP₁ G ε).parts

Tactic:
card_increment hPα huniform

Goal state after:
case neg.refine_1
α : 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 α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ t ≤ stepBound #P.parts
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.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)) =
    ∑ x ∈ P.parts.offDiag,
      (↑(G.edgeDensity x.1 x.2) ^ 2 + ((if G.IsUniform ε x.1 x.2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25))

Tactic:
sum_add_distrib,

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.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      ∑ x ∈ P.parts.offDiag, ((if G.IsUniform ε x.1 x.2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25)
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.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 0 < 7

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ ∀ (x y : V), s(x, y) ∈ ⊥.edgeSet ↔ s(x, y) ∈ ∅

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
⊢ ∀ (x y : V), s(x, y) ∈ (H₁ ⊓ H₂).edgeSet ↔ s(x, y) ∈ H₁.edgeSet ∩ H₂.edgeSet

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
⊢ ∀ (x y : V), s(x, y) ∈ (H₁ ⊔ H₂).edgeSet ↔ s(x, y) ∈ H₁.edgeSet ∪ H₂.edgeSet

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
⊢ ∀ {v w : V}, ⊥ v w → G.Adj v w

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
⊢ ∀ {v_1 w : V}, ⊥ v_1 w → v_1 ∈ {v}

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ A'.coe ≃g (Subgraph.map f.toHom A').coe

Tactic:
use Equiv.Set.image f.toHom _ f.injective

Goal state after:
case map_rel_iff'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ ∀ {a b : ↑A'.verts},
    (Subgraph.map f.toHom A').coe.Adj ((Equiv.Set.image (⇑f.toHom) A'.verts ⋯) a)
        ((Equiv.Set.image (⇑f.toHom) A'.verts ⋯) b) ↔
      A'.coe.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ ∀ {a b : V},
    { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.coe.Adj ((Equiv.Set.univ V).symm a)
        ((Equiv.Set.univ V).symm b) ↔
      ⊥.Adj a b

Tactic:
by simp

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

Goal state before:
pp: case neg
α : 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
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
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
hR₂ : ∀ 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
h : ¬0 < a
⊢ #(insert t ({i ∈ R.parts | #i = m + 1})) = b

Tactic:
· rw [card_insert_of_notMem, hR₃, if_neg h, Nat.sub_add_cancel (hab.resolve_left h)]
    intro H; exact ht.ne_empty (le_sdiff_right.1 <| R.le <| filter_subset _ _ H)

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
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
⊢ (fun H ↦ { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ })
      ⟨(H.verts.toFinset, fun a b ↦ decide (H.Adj a b)), ⋯⟩ =
    H

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
⊢ G.replaceVertex s s = G

Tactic:
ext; unfold replaceVertex; aesop (add simp or_iff_not_imp_left)

Goal state after:
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
⊢ n - #s % n + #s % n = n

Tactic:
tsub_add_cancel_of_le (mod_lt _ hn).le

Goal state after:
α : 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
⊢ n = n
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : G.Adj v w
⊢ v ∈ (G.subgraphOfAdj hvw).verts

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : V
⊢ G ⊔ edge s s = G

Tactic:
by simp

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
s✝ s' s : Set V
h : s ⊆ G'.verts
⊢ ∀ {a b : ↑(G'.induce s).verts},
    (SimpleGraph.induce {v | ↑v ∈ s} G'.coe).Adj
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, hv⟩,
            left_inv := ⋯, right_inv := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, hv⟩,
            left_inv := ⋯, right_inv := ⋯ }
          b) ↔
      (G'.induce s).coe.Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G✝ : SimpleGraph V
u v w : V
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support ≠ []

Tactic:
by simp

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.Subgraph
s✝ s : Set V
⊢ ∀ {a b : ↑(G'.deleteVerts s).verts},
    (SimpleGraph.induce {v | ↑v ∉ s} G'.coe).Adj
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          b) ↔
      (G'.deleteVerts s).coe.Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ {w | w ∈ p.support}

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
⊢ u ∈ nil.support ↔ u = v

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
hadj : G.Adj u v
⊢ (cons hadj q).snd = v

Tactic:
by simp

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
h : ¬p.Nil
⊢ ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w), (cons h q).snd ∈ (cons h q).support.tail

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ¬p.Nil
⊢ ∀ {u_1 v w : V} (h : G.Adj u_1 v) (q : G.Walk v w) (x : G.Adj u u_1),
    (cons x (cons h q)).penultimate = (cons h q).penultimate

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ¬p.Nil
⊢ ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w), w ∈ (cons h q).support.tail

Tactic:
by simp

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' w✝ : V
p✝¹ : G.Walk u✝¹ v✝¹
u✝ v✝ : V
p✝ : G.Walk u✝ v✝
H : SimpleGraph V
u w v : V
h✝ : G.Adj u v
p : G.Walk v w
h : ∀ e ∈ (cons' u v w h✝ p).edges, e ∈ H.edgeSet
⊢ s(u, v) ∈ (cons' u v w h✝ p).edges

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
d : G.Dart
⊢ [d] ≠ []

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
d : G.Dart
⊢ List.IsChain G.DartAdj [d]

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p = (nil.append p).append nil

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
q : G.Walk u v
⊢ q = (nil.append nil).append q

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
q : G.Walk u v
⊢ q = (q.append nil).append nil

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ p = (nil.append (p.take n)).append (p.drop n)

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ p = ((p.take n).append (p.drop n)).append nil

Tactic:
by simp

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

Goal state before:
pp: case head
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
hx : ¬v = v
⊢ v ∈ p.support

pp: case tail
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
hx : ¬v = u
a✝ : List.Mem u p.support
⊢ u ∈ p.support

Tactic:
· exact (hx rfl).elim

Goal state after:
case tail
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
hx : ¬v = u
a✝ : List.Mem u p.support
⊢ u ∈ p.support
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 = (nil.append (p.takeUntil w h)).append (p.dropUntil w h)

Tactic:
by 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 = ((p.takeUntil w h).append (p.dropUntil w h)).append nil

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
⊢ u = p.support.head ⋯

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
⊢ v = p.support.getLast ⋯

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
d : G.Dart
p : G.Walk u v
⊢ d ∈ p.reverse.darts ↔ d.symm ∈ p.darts

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ u = (p.darts.head ⋯).toProd.1

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ v = (p.darts.getLast ⋯).toProd.2

Tactic:
by simp

Goal state after: