mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : n + ↑⟨y, hy⟩ - ↑⟨x, hx⟩ = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
]

Goal state after:
case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : n + ↑⟨y, hy⟩ - ↑⟨x, hx⟩ = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inr.inl.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : j ∈ ↑right.toLeft
⊢ G.Adj i j

Tactic:
]

Goal state after:
case refine_1.inr.inl.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : j ∈ ↑right.toLeft
⊢ G.Adj i j
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inr.inl.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : Sum.inl j ∈ right
⊢ G.Adj i j

Tactic:
]

Goal state after:
case refine_1.inr.inl.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : Sum.inl j ∈ right
⊢ G.Adj i j
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), (mulCayley s).Adj v w → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a

Tactic:
]

Goal state after:
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), (mulCayley s).Adj v w → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})

Tactic:
]

Goal state after:
M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})

Tactic:
]

Goal state after:
M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this✝ : 3 ≤ p.length
this : p.length + 1 - 1 ≤ 2
⊢ False

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this✝ : 3 ≤ p.length
this : p.length + 1 - 1 ≤ 2
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w = p.reverse.snd

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w = p.reverse.snd
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ (q.concat ⋯).support

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ (q.concat ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ p₀.support

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ p₀.support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
⊢ s(u', v') ∈ (cons ⋯ tail.tail).edges.head?

Tactic:
]

Goal state after:
case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
⊢ s(u', v') ∈ (cons ⋯ tail.tail).edges.head?
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ Fintype.card V = Fintype.card V

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
⊢ G.edgeFinset.card = {default}ᶜ.card

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
⊢ G.edgeFinset.card = {default}ᶜ.card
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ (({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset) ∧
    ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
]

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ (({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset) ∧
    ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
]

Goal state after:
case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G

Tactic:
]

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
]

Goal state after:
case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
]

Goal state after:
case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ A i j = 1 ↔ A i j = 1

Tactic:
]

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

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G

Tactic:
]

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
]

Goal state after:
case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
f : W → V
hf : Function.Surjective f
h : (A.submatrix f f).IsAdjMatrix
⊢ (A.submatrix (f ∘ Function.surjInv hf) (f ∘ Function.surjInv hf)).IsAdjMatrix

Tactic:
]

Goal state after:
α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
f : W → V
hf : Function.Surjective f
h : (A.submatrix f f).IsAdjMatrix
⊢ (A.submatrix (f ∘ Function.surjInv hf) (f ∘ Function.surjInv hf)).IsAdjMatrix
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
hij : A i j = 1
⊢ A i j = 1

Tactic:
]

Goal state after:
α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
hij : A i j = 1
⊢ A i j = 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
⊢ ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
    H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H

Tactic:
]

Goal state after:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
⊢ ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
    H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : (f a).firstDart ⋯ = (f b).firstDart ⋯ ∨ (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h' : (f a).length ≤ (f b).length
⊢ a = b

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : (f a).firstDart ⋯ = (f b).firstDart ⋯ ∨ (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h' : (f a).length ≤ (f b).length
⊢ a = b
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
]

Goal state after:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂

Tactic:
]

Goal state after:
case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁

Tactic:
]

Goal state after:
case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ H.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ H.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ #(induce {v}ᶜ G).edgeFinset ≤ extremalNumber (Fintype.card ↑{v}ᶜ) H

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ #(induce {v}ᶜ G).edgeFinset ≤ extremalNumber (Fintype.card ↑{v}ᶜ) H
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr.refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : (f a).length = (f b).length + 1
⊢ a = b

Tactic:
]

Goal state after:
case inr.refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : (f a).length = (f b).length + 1
⊢ a = b
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ ∑ u ∈ G.neighborFinset v, vec u = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G x v

Tactic:
]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))

Tactic:
]

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ G.neighborFinset u, ↑(#(G.finsetWalkLength n x v)) =
    ↑(∑ u_1, #(Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑u_1) v)))

pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ (↑univ).PairwiseDisjoint fun w ↦
    Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)

Tactic:
]

Goal state after:
case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ G.neighborFinset u, ↑(#(G.finsetWalkLength n x v)) =
    ↑(∑ u_1, #(Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑u_1) v)))

case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ (↑univ).PairwiseDisjoint fun w ↦
    Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)