mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)
⊢ (a ⊔ u) \ v = (a ⊔ u) \ v

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ a = a

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
hℬ : s ∈ upperClosure ↑ℬ
⊢ #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #⊥ + #(ℬ.truncatedInf s)

Tactic:
truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
hℬ : s ∈ upperClosure ↑ℬ
⊢ #(ℬ.truncatedInf s) + #⊥ = #⊥ + #(ℬ.truncatedInf s)
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ #u + (k + 1) = #u + k + 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #t + k + 1 = #t + (k + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ

Tactic:
simp only [mem_shadow_iff, mem_upShadow_iff, mem_compls]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ

Tactic:
simp only [mem_shadow_iff, mem_upShadow_iff, mem_compls]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : ¬(Disjoint u a ∧ v ⊆ a)
⊢ #a = #a

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ v = ∅ → u = ∅

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
x : α
hx : x ∈ s
hxc : x ∈ map { toFun := compl, inj' := ⋯ } s
⊢ False

Tactic:
obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc

Goal state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
x : α
hx' : x ∈ s
hx : { toFun := compl, inj' := ⋯ } x ∈ s
hxc : { toFun := compl, inj' := ⋯ } x ∈ map { toFun := compl, inj' := ⋯ } s
⊢ False
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
hs : a ∉ s
⊢ t.erase a = s ↔ t = s ∨ t = insert a s

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›) rfl
        (insert_inter_distrib _ _ _).symm,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤
    (f₃ (s ∩ t) + f₃ (insert a s ∩ insert a t)) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) → (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)
    · exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
    refine ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, ?_⟩
    rw [card_erase_of_mem ha, hs]
    rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #{∅} ≤ #{∅}.shatterer

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
⊢ ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x | r x z}
hx : x ∈ c
hy : y ∈ c
⊢ r x y

Tactic:
subst c

Goal state after:
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
z : α
hx : x ∈ {x | r x z}
hy : y ∈ {x | r x z}
⊢ r x y
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp.nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Relation.ReflTransGen G.Adj u✝ u✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr.refl
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u u

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case inr
V : Type u
u v : V
huv : u ≠ v
⊢ (completeGraph V).Reachable u v

Tactic:
· exact ⟨.cons huv .nil⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mk
V : Type u
G : SimpleGraph V
x✝ : G.ConnectedComponent
v : V
⊢ refl.connectedComponentEquiv (Quot.mk G.Reachable v) = (Equiv.refl G.ConnectedComponent) (Quot.mk G.Reachable v)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
x✝ : G'.ConnectedComponent
a✝ : V'
⊢ φ.symm.connectedComponentEquiv (Quot.mk G'.Reachable a✝) = φ.connectedComponentEquiv.symm (Quot.mk G'.Reachable a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
x✝ : G.ConnectedComponent
a✝ : V
⊢ (connectedComponentEquiv (RelIso.trans φ φ')) (Quot.mk G.Reachable a✝) =
    (φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv) (Quot.mk G.Reachable a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
C : Partitions α
⊢ Partitions.toSet ((fun r ↦ ⟨r.classes, ⋯⟩) ((fun C ↦ mkClasses ↑C ⋯) C)) = (mkClasses C.toSet ⋯).classes

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } r ≤
      { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } s ↔
    mkClasses r.classes ⋯ ≤ mkClasses s.classes ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h :
  ∃ a,
    ∃ (b : a ∈ C),
      ∃ a_1,
        ∃ (b_1 : a_1 ∈ C),
          C.toSimpleGraph.Adj ⟨a, b⟩ ⟨a_1, b_1⟩ ∧
            (Embedding.subtype fun x ↦ x ∈ ↑C) ⟨a, b⟩ = v ∧ (Embedding.subtype fun x ↦ x ∈ ↑C) ⟨a_1, b_1⟩ = w
⊢ G.connectedComponentMk v = C ∧ G.Adj v w

Tactic:
obtain ⟨_, a, _, _, h₁, rfl, rfl⟩ := h

Goal state after:
case mp
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
w✝² : V
a : w✝² ∈ C
w✝¹ : V
w✝ : w✝¹ ∈ C
h₁ : C.toSimpleGraph.Adj ⟨w✝², a⟩ ⟨w✝¹, w✝⟩
⊢ G.connectedComponentMk ((Embedding.subtype fun x ↦ x ∈ ↑C) ⟨w✝², a⟩) = C ∧
    G.Adj ((Embedding.subtype fun x ↦ x ∈ ↑C) ⟨w✝², a⟩) ((Embedding.subtype fun x ↦ x ∈ ↑C) ⟨w✝¹, w✝⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C✝ : G.Coloring α
inst✝² : Nonempty (G.Coloring α)
inst✝¹ : Nontrivial α
inst✝ : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ C v
h : (Iso.completeGraph (Equiv.swap (C v) c)).toHom.comp C = C
this : (Equiv.swap (C v) c) (C v) = C v
⊢ c = C v

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C✝ : G.Coloring α
inst✝² : Nonempty (G.Coloring α)
inst✝¹ : Infinite α
inst✝ : Nonempty V
C : G.Coloring α
v : V
f : α → G →g completeGraph α := fun c ↦ (Iso.completeGraph (Equiv.swap (C v) c)).toHom.comp C
a b : α
h : f a = f b
this : (Equiv.swap (C v) a) (C v) = (Equiv.swap (C v) b) (C v)
⊢ a = b

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
v : V
⊢ ((G.recolorOfEmbedding f.toEmbedding) ((G.recolorOfEmbedding f.symm.toEmbedding) C)) v = C v

Tactic:
apply Equiv.apply_symm_apply

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ s(w, v) ∈ (c.rotate v hvc).edges

Tactic:
rwa [(c.rotate_edges v hvc).mem_iff, Sym2.eq_swap]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
⊢ ∃ a, C a = i

Tactic:
by_contra! hi

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ ∀ e ∈ P.edges, e ∉ {s(x, y)}

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
heP₁ : s(x, y) ∉ P₁.edges
⊢ ∀ e ∈ P₁.edges, e ∉ {s(x, y)}

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this✝ : card V ≤ card V - 1
this : 1 < card V
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
w : V
hwp : w ∈ p.support
hws : w ∉ s
⊢ w ≠ u

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
w : V
hwp : w ∈ p.support
hws : w ∉ s
⊢ w ≠ v

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
p : G.Walk u v
e : Sym2 V
⊢ ∀ (a₁ a₂ : V),
    (fun v_1 w ↦ v_1 ∈ p.support ∧ w ∈ p.support) a₁ a₂ = (fun v_1 w ↦ v_1 ∈ p.support ∧ w ∈ p.support) a₂ a₁

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (∀ (x y : V), G.Adj x y → s(x, y) ∉ p.edges → x ∈ p.support → y ∉ p.support) ↔
    ∀ ⦃u' v' : V⦄, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges

Tactic:
grind

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

Goal state before:
pp: case inl.inl
V : Type u
G : SimpleGraph V
w b : V
hvw : G.Adj b w
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩

Tactic:
rfl

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

Goal state before:
pp: case inl.inr
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
rfl

Goal state after:
case inl.inr
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
rfl

Goal state after:
case inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inr.inr
V : Type u
G : SimpleGraph V
v b : V
hvw : G.Adj v b
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
⊢ (between s t G).Adj v w ↔ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)

Tactic:
rfl

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

Goal state before:
pp: case mk.mk
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
W₁ : Type u_2
W₂ : Type u_3
inst✝ : DecidableRel fun x1 x2 ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
val✝¹ : Sym2 V
a✝¹ : V × V
property✝¹ : Quot.mk (Sym2.Rel V) a✝¹ ∈ G.edgeSet
val✝ : Sym2 V
a✝ : V × V
property✝ : Quot.mk (Sym2.Rel V) a✝ ∈ G.edgeSet
⊢ ((if hp : a✝¹.1 ∈ s ∧ a✝¹.2 ∈ t then (fun h ↦ ⟨s(Sum.inl ⟨a✝¹.1, ⋯⟩, Sum.inr ⟨a✝¹.2, ⋯⟩), ⋯⟩) hp
      else (fun h ↦ ⟨s(Sum.inl ⟨a✝¹.2, ⋯⟩, Sum.inr ⟨a✝¹.1, ⋯⟩), ⋯⟩) ⋯) =
      if hp : a✝.1 ∈ s ∧ a✝.2 ∈ t then (fun h ↦ ⟨s(Sum.inl ⟨a✝.1, ⋯⟩, Sum.inr ⟨a✝.2, ⋯⟩), ⋯⟩) hp
      else (fun h ↦ ⟨s(Sum.inl ⟨a✝.2, ⋯⟩, Sum.inr ⟨a✝.1, ⋯⟩), ⋯⟩) ⋯) →
    ⟨Quot.mk (Sym2.Rel V) a✝¹, property✝¹⟩ = ⟨Quot.mk (Sym2.Rel V) a✝, property✝⟩

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a₁ : V × V)
    (ha₁ :
      a₁ ∈
        {x |
          match x with
          | (x, y) => G.Adj x y})
    (a₂ : V × V)
    (ha₂ :
      a₂ ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
    ((match a₁, ha₁ with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        match a₂, ha₂ with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) →
      a₁ = a₂

Tactic:
grind

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

Goal state before:
pp: case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑p.length + G.edist v w

Tactic:
← hq,

Goal state after:
case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑p.length + ↑q.length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range ((fun w ↦ ↑w.length) ∘ Walk.reverse)) = G.edist v u

Tactic:
Function.comp_def

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.reverse.length) = G.edist v u
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
this : ¬2 ≤ G.edist u v
⊢ False

Tactic:
simp_all [Order.le_one_iff]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ p.length + G.dist v w

Tactic:
← hq,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ p.length + q.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
h : v ∈ p.support
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
simp only [SimpleGraph.Walk.mem_support_iff_exists_getVert] at h ⊢
  obtain ⟨i, hi⟩ := h
  by_cases! he : i = 0 ∨ i = p.length
  · have huv : u = v := by aesop
    rw [← huv, hpc.neighborSet_toSubgraph_endpoint]
    exact Set.ncard_pair hpc.snd_ne_penultimate
  rw [← hi.1, hpc.neighborSet_toSubgraph_internal he.1 (by lia)]
  exact Set.ncard_pair (hpc.getVert_sub_one_ne_getVert_add_one (by lia))

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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
x✝ : ↑(G ⊕g H).edgeSet
e : Sym2 (V ⊕ W)
he : e ∈ (G ⊕g H).edgeSet
⊢ ∀ (a b : V ⊕ W) (h : (G ⊕g H).Adj a b),
    (match a, b, h with
      | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
      | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
      | Sum.inl u, Sum.inr v, h => False.elim ⋯
      | Sum.inr u, Sum.inl v, h => False.elim ⋯) =
      match b, a, ⋯ with
      | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
      | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
      | Sum.inl u, Sum.inr v, h => False.elim ⋯
      | Sum.inr u, Sum.inl v, h => False.elim ⋯

Tactic:
grind

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

Goal state before:
pp: case mk.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u v : V
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩

Tactic:
rfl

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

Goal state before:
pp: case mk.inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u v : W
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩

Tactic:
rfl

Goal state after: