mathlib-initiative/mathlib-tactics huggingface dataset:
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
R R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ F.IsPrestackFor R ↔ F.IsPrestackFor R'

Tactic:
simp only [isPrestackFor_iff]
  obtain ⟨_, _, f, rfl⟩ := Presieve.exists_eq_ofArrows R
  obtain ⟨_, _, f', rfl⟩ := Presieve.exists_eq_ofArrows R'
  apply DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq
  simpa only [Sieve.ofArrows_category']

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 Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure ≤ Q

Tactic:
retractClosure_le_iff

Goal state after:
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 Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: case refine_1
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 c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLTLTToLT c b).app X) ≫
        (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
eTruncLTLTToLT_app,

Goal state after:
case refine_1
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 c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app X)) ≫
        (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Iio ↑(k + 1) = Iic ↑k

Tactic:
ext x

Goal state after:
case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ x ∈ Iio ↑(k + 1) ↔ x ∈ Iic ↑k
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case e'_7
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Iio (k + 1) = Iic k

Tactic:
ext x

Goal state after:
case e'_7
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : ℕ
⊢ x ∈ Iio (k + 1) ↔ x ∈ Iic k
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
n : ℕ∞
h : ∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
s : Subgroup G
hs : s ≠ ⊥
hs' : (↑s).Finite
a : G
has : a ∈ s
ha : a ≠ 1
⊢ n ≤ ↑(Nat.card ↥s)

Tactic:
exact
      (h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
        (WithTop.coe_le_coe.2 <| s.orderOf_le_card hs' has)

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c * g ∈ a⁻¹ • ↑s

pp: case refine_2
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c * g⁻¹ ∈ a⁻¹ • ↑s

Tactic:
· rw [← hsg, coe_smul_finset, smul_comm]
        exact Set.smul_mem_smul_set hc

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c * g⁻¹ ∈ a⁻¹ • ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set V
⊢ induceHom Hom.id ⋯ = Hom.id

Tactic:
ext x

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set V
x : ↑s
⊢ ↑((induceHom Hom.id ⋯) x) = ↑(Hom.id x)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ) t r
⊢ (induceHom ψ ψtr).comp (induceHom φ φst) = induceHom (ψ.comp φ) ⋯

Tactic:
ext x

Goal state after:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ) t r
x : ↑s
⊢ ↑(((induceHom ψ ψtr).comp (induceHom φ φst)) x) = ↑((induceHom (ψ.comp φ) ⋯) x)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
obtain ⟨d, hd, hcd⟩ := hQR hc

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hcd : c ≤ d
⊢ ∃ c ∈ R.parts, b ≤ c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
x₂ y₂ : α
hx₂ : x₂ ∈ P.parts
hy₂ : y₂ ∈ Q.parts
h : ¬x₂ ⊓ y₂ = x₁ ⊓ y₁
xdiff : x₁ ≠ x₂
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)

Tactic:
exact Disjoint.mono inf_le_left inf_le_left (P.disjoint hx₁ hx₂ xdiff)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ b ∈ (P.bind Q).parts ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
rw [bind_parts, mem_biUnion]
  constructor
  · rintro ⟨⟨A, hA⟩, -, h⟩
    exact ⟨A, hA, h⟩
  · rintro ⟨A, hA, h⟩
    exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case bot
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
n : ℤ
X : C
h : WithBotTop.coe n ≤ ⊥
⊢ t.IsGE ((t.eTruncGE.obj ⊥).obj X) n

Tactic:
simp at h

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case top
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
n : ℤ
X : C
h : ⊤ ≤ WithBotTop.coe (n + 1)
⊢ t.IsLE ((t.eTruncLT.obj ⊤).obj X) n

Tactic:
simp at h

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
⊢ a ∈ t → P.part a = t

Tactic:
intro hat
    apply P.eq_of_mem_parts (a := a) <;> simp [*, P.le ht hat]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.top
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
X : C
b : ℤ
h : ⊤ ≤ WithBotTop.coe b
⊢ IsIso ((t.eTruncGE.obj (WithBotTop.coe b)).map ((t.eTruncGEπ ⊤).app X))

Tactic:
simp at h

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.bot
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
X : C
a : ℤ
h : WithBotTop.coe a ≤ ⊥
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι ⊥).app X))

Tactic:
simp at h

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
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(#∅)
⊢ ε ≤ 0

Tactic:
simpa using hs

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

Goal state before:
pp: case inr.refine_1
𝕜 : 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 ≤ δ
hscard : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
htcard : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
h : 1 ≤ δ
⊢ 0 ≤ ↑(edgeDensity r s₂ t₂)

Tactic:
· exact mod_cast edgeDensity_nonneg r _ _

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

Goal state before:
pp: case inr.refine_2
𝕜 : 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 ≤ δ
hscard : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
htcard : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
h : 1 ≤ δ
⊢ 0 ≤ ↑(edgeDensity r s₁ t₁)

Tactic:
· exact mod_cast edgeDensity_nonneg r _ _

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
⊢ H.Adj w v ↔ H.Adj w x

Tactic:
hl.2

Goal state after:
case inl
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
⊢ H.Adj w x ↔ H.Adj w x
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
G' : G.Subgraph
hG' : G' ∈ s
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b

Tactic:
exact fun h => G'.adj_sub (h _ hG')

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ { Adj := fun v w ↦ if v = s then if w = s then False else G.Adj s w else if w = s then G.Adj v s else G.Adj v w,
          symm := ⋯, loopless := ⋯ }.Adj
      x✝¹ x✝ ↔
    G.Adj x✝¹ x✝

Tactic:
aesop (add simp or_iff_not_imp_left)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(equitabilise ⋯).parts = 4 ^ #P.parts

Tactic:
rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le]

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ Fintype.card α / #P.parts - m * 4 ^ #P.parts ≤ 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
h : nil.edges = (cons h✝ p✝).edges
⊢ nil = cons h✝ p✝

Tactic:
simp at h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
h : (cons h✝ p✝).edges = nil.edges
⊢ cons h✝ p✝ = nil

Tactic:
simp at h

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

Goal state before:
pp: case cons.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ u✝
ih : ∀ ⦃p' : G.Walk v✝ u✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
h : Walk.map f (cons h✝ p✝) = Walk.map f nil
⊢ cons h✝ p✝ = nil

Tactic:
simp at h

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

Goal state before:
pp: case cons.mp.nil
V : Type u_1
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p : G.Walk v✝ v
w✝ : G.Walk v u
h : nil = (nil.append (cons h✝ p)).append w✝
⊢ ∃ (hu : u = u) (hv : u = v), cons h✝ p = nil.copy hu hv

Tactic:
simp at h

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

Goal state before:
pp: case cons.mp.cons
V : Type u_1
G : SimpleGraph V
u v u' v✝¹ : V
h✝¹ : G.Adj u v✝¹
p : G.Walk v✝¹ v
v✝ : V
h✝ : G.Adj u' v✝
p✝ : G.Walk v✝ u
w✝ : G.Walk v u'
h : nil = ((cons h✝ p✝).append (cons h✝¹ p)).append w✝
⊢ ∃ (hu : u' = u) (hv : u' = v), cons h✝¹ p = nil.copy hu hv

Tactic:
simp at h

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
w✝² : V
w✝¹ : G.Walk u w✝²
w✝ : G.Adj w✝² v
hp : cons h p = w✝¹.concat w✝
⊢ (cons h p).support.dropLast ++ [v] = (cons h p).support

Tactic:
simp [hp]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he✝ : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.edge = s(t, u)
⊢ t ∈ p.support

Tactic:
rw [dart_edge_eq_mk'_iff'] at he

Goal state after:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he✝ : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t
⊢ t ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ u :: p.tail.support = p.support

Tactic:
simp [hp]

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

Goal state before:
pp: case refine_1
α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ A.Nonempty

pp: case refine_2
α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ x.Nonempty

pp: case refine_3
α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ B.Nonempty

pp: case refine_4
α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ y.Nonempty

Tactic:
exacts [⟨_, hx⟩, nonempty_of_mem_parts _ (hA hx), ⟨_, hy⟩, nonempty_of_mem_parts _ (hB hy)]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
⊢ p = q

Tactic:
refine ext_getVert_le_length (hpq.antisymm ?_) fun k _ ↦ h k

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
⊢ q.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique s ∧ ⇑f '' s = ↑t) → ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
rintro ⟨s, hs, hst⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : ⇑f '' s = ↑t
⊢ ∃ s, G.IsClique ↑s ∧ map f s = t
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp
α : 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}

Tactic:
rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, hab⟩

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
c d e : α
hcd : G.Adj c d
hce : G.Adj c e
hde : G.Adj d e
hab : a ∈ {c, d, e} ∧ b ∈ {c, d, e}
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, d, e} = {a, b, c_1}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inl.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, b, e} = {a, b, c}

Tactic:
exact ⟨c, by aesop⟩

Goal state after:
case mp.inl.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, b, e} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, d, b} = {a, b, c}

Tactic:
exact ⟨c, by aesop⟩

Goal state after:
case mp.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, d, b} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

Tactic:
exact ⟨c, by aesop⟩

Goal state after:
case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

Tactic:
exact ⟨c, by aesop⟩

Goal state after:
case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, a, b} = {a, b, c_1}

Tactic:
exact ⟨c, by aesop⟩

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

Goal state before:
pp: case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

Tactic:
exact ⟨c, by aesop⟩

Goal state after:
case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

Tactic:
exact ⟨c, by aesop⟩

Goal state after:
case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
exact ⟨c, by aesop⟩

Goal state after:
case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
exact ⟨c, by aesop⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ True

Tactic:
and_true,

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c