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

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
h : G ≤ H
a : α
w : G.Walk a a
hw : w.IsCycle
⊢ ↑(Walk.mapLe h w).length ≤ ↑w.length

Tactic:
by

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
⊢ zarankiewicz m n s t ≤ x ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) ↔ ¬G.IsAcyclic

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ 3 ≤ G.egirth

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.egirth = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
⊢ w.edges.Nodup

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ v ∈ K.vertsᶜ \ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) +
      ∑ v ∈ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤
    ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
⊢ w ≠ Walk.nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
⊢ w.support.tail.Nodup

Tactic:
by

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
x✝ : ∃ b, (b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b) ∧ x < #b.edgeFinset
w✝ : SimpleGraph (V ⊕ W)
h_le : w✝ ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free w✝
h_lt : x < #w✝.edgeFinset
⊢ x < #w✝.edgeFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
⊢ ⊤.egirth = 3

Tactic:
by

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
x✝ : ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < #G.edgeFinset
w✝¹ : SimpleGraph (V ⊕ W)
w✝ : DecidableRel w✝¹.Adj
h_le : w✝¹ ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free w✝¹
h_lt : x < #w✝¹.edgeFinset
⊢ #w✝¹.edgeFinset = #w✝¹.edgeFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
⊢ G'.egirth ≤ G.egirth

Tactic:
by

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
⊢ x < zarankiewicz m n s t ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < #G.edgeFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.girth = 0
⊢ ¬3 ≤ G.girth

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.IsAcyclic
⊢ G.girth = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.girth = w.length) → ¬G.IsAcyclic

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.girth = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
⊢ ⊤.girth = 3

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
f : G ≃g G'
⊢ G.girth = G'.girth

Tactic:
by

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Fintype V
inst✝⁵ : Fintype W
inst✝⁴ : Fintype α
inst✝³ : Fintype β
R : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : R
h : 0 ≤ x
⊢ ↑(zarankiewicz m n s t) ≤ x ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → ↑(#G.edgeFinset) ≤ x

Tactic:
by

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Fintype V
inst✝⁵ : Fintype W
inst✝⁴ : Fintype α
inst✝³ : Fintype β
R : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : R
h : 0 ≤ x
⊢ x < ↑(zarankiewicz m n s t) ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < ↑(#G.edgeFinset)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
he : Even #s
n : ℕ
hn : #s = n + n
t : Finset α
ht : t ⊆ s
ht' : #t = n
⊢ t ∪ s \ t = s ∧ Disjoint t (s \ t) ∧ #t = #(s \ t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #t = #u) → Even #s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
h : ¬1 = 0
⊢ (s ∩ Function.support fun i ↦ 1).Infinite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Finset ι
s : ι → Set α
⊢ ∅.ncard = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Finset ι
s : ι → Set α
⊢ ∅.encard = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ Nonempty (↑s ≃ ↑s ⊕ ↑s)

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
⊢ ↑N * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
by

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

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ zarankiewicz m n s t ≤ extremalNumber (m + n) (completeBipartiteGraph α β)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
by

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

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ 0 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
by

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

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ 0 ≤ ↑(zarankiewicz n n s t) / 2

Tactic:
by

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

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ 0 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Even s.ncard ↔ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
⊢ (⋃ i ∈ t, s i).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ ∀ i ∈ univ, (s i).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = ∑ᶠ (i : ι), (s i).ncard

Tactic:
by

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

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ 2 * extremalNumber n (completeBipartiteGraph α β) ≤ zarankiewicz n n s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).encard = ∑ᶠ (i : ι), (s i).encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
⊢ (⋃ i ∈ t, s i).ncard ≤ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
⊢ (⋃ i ∈ t, s i).encard ≤ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : ι → Set α
⊢ (⋃ i, s i).ncard ≤ ∑ i, (s i).ncard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : ι → Set α
⊢ (⋃ i, s i).encard ≤ ∑ i, (s i).encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
⊢ (⋃ i, s i).ncard ≤ ∑ᶠ (i : ι), (s i).ncard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
⊢ (⋃ i, s i).encard ≤ ∑ᶠ (i : ι), (s i).encard

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
⊢ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t) =
    ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n - ↑(#K.verts)) - (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t))

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
⊢ Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝ : v ∈ p
h : f ⟨v, h✝⟩ = w
⊢ v ∈ p

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ w ∈ p

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h : if h : v ∈ p then f ⟨v, h⟩ = w else if h : w ∈ p then f ⟨w, h⟩ = v else False
⊢ G.Adj v w

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ #(K.parts.pi fun x ↦ powersetCard t x) * t = (∏ x ∈ K.parts, (#x).choose t) * t

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
⊢ ∀ {v w : V}, (if h : v ∈ p then f ⟨v, h⟩ = w else if h : w ∈ p then f ⟨w, h⟩ = v else False) → v ∈ p ∪ Set.range f

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ h.toEdge ⟨v, ⋯⟩ = ⟨s(v, w), hvw⟩

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
⊢ ∀ (a b : V),
    (if h : a ∈ p then f ⟨a, h⟩ = b else if h : b ∈ p then f ⟨b, h⟩ = a else False) →
      if h : b ∈ p then f ⟨b, h⟩ = a else if h : a ∈ p then f ⟨a, h⟩ = b else False

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ Surjective h.toEdge

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b s)
h3 : b ∉ s
ha : G.Adj a b
⊢ G.IsNClique (r + 1) (insert b (insert a s))

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
s : Finset ↑p₁
⊢ ↑(Finset.image Subtype.val s) ⊆ p₁

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
⊢ h.toEdge ⟨v, ⋯⟩ = h.toEdge ⟨w, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert a (insert b (s.erase c)))

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ (∏ p ∈ K.parts, t'.choose t) * t ≤ t'.choose t ^ r * t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
⊢ ∃ v w₁ w₂ s t, G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ h.toEdge ⁻¹' {⟨s(u, v), huv⟩} = {⟨u, ⋯⟩, ⟨v, ⋯⟩}

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
s : Finset ↑p₁
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset ↑x).card

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ h.toEdge ⁻¹' {⟨s(u, v), huv⟩} = {⟨u, ⋯⟩, ⟨v, ⋯⟩}

Tactic:
by
  refine Set.ext fun w ↦ ⟨fun hw ↦ ?_, fun hw ↦ ?_⟩
  · grind [h.mem_coe_toEdge w.property]
  · rcases hw with rfl | rfl
    · simp [h.toEdge_eq_of_adj huv]
    · simp [h.toEdge_eq_of_adj huv.symm]

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

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
p2 : G.IsPathGraph3Compl v w₁ w₂
d1 : v ∉ s
d2 : v ∉ t
d3 : w₁ ∉ s
d4 : w₂ ∉ t
c1 : G.IsNClique (r + 1) (insert v s)
c2 : G.IsNClique (r + 1) (insert w₁ s)
c3 : G.IsNClique (r + 1) (insert v t)
c4 : G.IsNClique (r + 1) (insert w₂ t)
hk : #(s ∩ t) = k
⊢ #(t ∩ s) = k

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
⊢ p₁ ⊆ (hall_subgraph f this ⋯).verts

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
⊢ ‖Fin (r + 1)‖ ≤ #(insert w₁ s)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
⊢ (Subgraph.map (Hom.ofLE hGG') M).IsMatching

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (↑(insert w₁ s)) Set.univ
⊢ ‖Fin (r + 1)‖ ≤ #(insert w₂ t)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v : V
h' : v ∈ p₁
⊢ (fun w ↦ if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False) (f ⟨v, h'⟩) ∧
    ∀ (y : V),
      (fun w ↦ if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False) y → y = f ⟨v, h'⟩

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ ↑(t'.choose t ^ r * t) * (↑t' - ↑t) ≤ ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
exact mul_le_card_filter_mul K hr_pos ht'_pos hδ (mod_cast hN)

Goal state after: