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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t - #t✝ = 1 ↔ #t = #t✝ + 1

Tactic:
tsub_eq_iff_eq_add_of_le,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t = 1 + #t✝ ↔ #t = #t✝ + 1

α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t - #t✝ = k ↔ #t = #t✝ + k

Tactic:
tsub_eq_iff_eq_add_of_le,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t = k + #t✝ ↔ #t = #t✝ + k

α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t✝ - #t = 1 ↔ #t✝ = #t + 1

Tactic:
tsub_eq_iff_eq_add_of_le,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t✝ = 1 + #t ↔ #t✝ = #t + 1

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ a

pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ u ≤ a

Tactic:
· rw [← hba, le_sdiff]
    exact ⟨le_sup_right, h.1.mono_right h.2⟩

Goal state after:
case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ u ≤ a
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t✝ - #t = k ↔ #t✝ = #t + k

Tactic:
tsub_eq_iff_eq_add_of_le,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t✝ = k + #t ↔ #t✝ = #t + k

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊔ b) = ofIsEmpty a ∪ ofIsEmpty b

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊓ b) = ofIsEmpty a ∩ ofIsEmpty b

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
simp [eq_iff_true_of_subsingleton]

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

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

Tactic:
card_sdiff_of_subset (h.2.trans le_sup_left),

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #(a ⊔ u) - #v = #a
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
⊢ {t ∈ 𝒜 | t.erase a = s} =
    if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅

Tactic:
by
  ext t; split_ifs <;> simp [erase_eq_iff ha] <;> aesop

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

Goal state before:
pp: case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(#𝒜) * ↑((Fintype.card α).choose (r - 1)) ≤ ↑(#(∂ 𝒜)) * ↑((Fintype.card α).choose r)

Tactic:
norm_cast

Goal state after:
case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inr.hb
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose r)

Tactic:
norm_cast

Goal state after:
case inr.hb
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose r
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inr.hd
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose (r - 1))

Tactic:
norm_cast

Goal state after:
case inr.hd
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose (r - 1)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case e'_4
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r

Tactic:
simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]

Goal state after:
case e'_4
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ (Fintype.card α).choose r * (Fintype.card α - r) = (Fintype.card α - r) * (Fintype.card α).choose r ∨ #(∂ 𝒜) = 0
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) ≤ 1 * ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))

Tactic:
norm_cast

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))

Tactic:
norm_cast

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s))⁻¹ ≤ 1

Tactic:
by
  calc
    _ = ∑ r ∈ range (Fintype.card α + 1),
        ∑ s ∈ 𝒜 with #s = r, ((Fintype.card α).choose r : 𝕜)⁻¹ := by
      rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]
    _ = ∑ r ∈ range (Fintype.card α + 1), (#(𝒜 # r) / (Fintype.card α).choose r : 𝕜) := by
      simp [slice, div_eq_mul_inv]
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜

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

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ s ∩ v.erase a = s ∩ u

Tactic:
inter_erase,

Goal state after:
case pos.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ (s ∩ v).erase a = s ∩ u
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : p.Nil
⊢ v ∈ H.verts

Tactic:
exact hnp.eq ▸ hv'

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : ¬p.Nil
⊢ v ∈ H.verts

Tactic:
exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail

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

Goal state before:
pp: α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
⊢ IsPartition s

Tactic:
refine ⟨h₃, fun a ↦ existsUnique_of_exists_of_unique (h₂ a) ?_⟩
  intro b₁ b₂ hb₁ hb₂
  apply h₁.elim hb₁.1 hb₂.1
  simp only [Set.not_disjoint_iff]
  exact ⟨a, hb₁.2, hb₂.2⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some ⋯.some ∈ ⋃ i ∈ g ⁻¹' {k}, s i

Tactic:
by
    refine mem_iUnion_of_mem ((singleton_nonempty k).preimage hg).some ?_
    simp only [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop]
    constructor
    · simpa using ((singleton_nonempty k).preimage hg).some_mem
    · exact hs.some_mem ((singleton_nonempty k).preimage hg).some

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

Goal state before:
pp: case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #(A \ B) + #B = #A

Tactic:
card_sdiff_add_card_eq_card hBA

Goal state after:
case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #A = #A
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber = ⨅ n, ↑↑n

Tactic:
rw [chromaticNumber, iInf_subtype]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ↑(sInf {n' | G.Colorable n'}) ≤ ↑n

Tactic:
norm_cast

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ sInf {n' | G.Colorable n'} ≤ n
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 α
⊢ Surjective ⇑C

Tactic:
intro i

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 : α
⊢ ∃ a, C a = i
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
s : Finset V
h : G.IsClique ↑s
hc : card α ≤ s.card
C : G.Coloring α
a✝¹ : α
a✝ : a✝¹ ∈ Set.univ
⊢ ↑(card α) ≤ (induce (↑s) G).chromaticNumber

Tactic:
simp_all [← induce_eq_top]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph n).Copy G
this : n = n - 3 + 3
⊢ ∃ v p, p.IsCycle ∧ p.length = n

Tactic:
rw [this] at h

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph (n - 3 + 3)).Copy G
this : n = n - 3 + 3
⊢ ∃ v p, p.IsCycle ∧ p.length = n
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_2.refine_2
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⟩
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
have hne : x ≠ y := fun _ ↦ by simp_all

Goal state after:
case refine_2.refine_2
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
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s

Tactic:
cases h1 with
      | inl h1 => exact Or.inl h1.left
      | inr h1 => exact Or.inr h1.left

Goal state after:
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)))

Tactic:
norm_cast

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)))
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
hT' : T.IsTree
⊢ Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) T

Tactic:
· rw [maximal_isAcyclic_iff_reachable_eq hT hT'.isAcyclic,
      T.preconnected_iff_reachable_eq_top.mp hT'.preconnected,
      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]

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

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u✝ : α
w : G.Walk u✝ u✝
ho : Odd w.length
this : 3 ≤ ↑2
⊢ False

Tactic:
norm_cast

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α},
    (completeMultipartiteGraph fun c ↦ { x // h.setoid c.out x }).Adj
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩,
            invFun := fun x ↦
              match x with
              | ⟨fst, x⟩ => ↑x,
            left_inv := ⋯, right_inv := ⋯ }
          a)
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩,
            invFun := fun x ↦
              match x with
              | ⟨fst, x⟩ => ↑x,
            left_inv := ⋯, right_inv := ⋯ }
          b) ↔
      G.Adj a b

Tactic:
simp_rw [Equiv.coe_fn_mk, comap_adj, top_adj, ne_eq, Quotient.eq]

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ¬h.setoid a b ↔ G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_1
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
e : Sym2 (Fin r × Fin t)
he : e ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
induction e with | _ v₁ v₂
    rw [mem_edgeSet, completeEquipartiteGraph_adj] at he
    exact ⟨⟨v₁.1, v₂.1, he⟩, ⟨v₁.2⟩⟩

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

Goal state before:
pp: r t : ℕ
⊢ #(completeEquipartiteGraph r t).edgeFinset = r.choose 2 * t ^ 2

Tactic:
← mul_right_inj' two_ne_zero,

Goal state after:
r t : ℕ
⊢ 2 * #(completeEquipartiteGraph r t).edgeFinset = 2 * (r.choose 2 * t ^ 2)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≠ 0 ↔ ¬Subsingleton α

Tactic:
← eccent_eq_zero_iff

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≠ 0 ↔ ¬eccent ?m.16 ?m.17 = 0

α : Type u_1
G : SimpleGraph α
u : α
⊢ α

α : Type u_1
G : SimpleGraph α
u : α
⊢ SimpleGraph α
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
x✝ Y Z : (Finset V)ᵒᵖ
h : x✝ ⟶ Y
h' : Y ⟶ Z
⊢ ↾ComponentCompl.hom ⋯ = ↾ComponentCompl.hom ⋯ ≫ ↾ComponentCompl.hom ⋯

Tactic:
ext C
    simp

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

Goal state before:
pp: case h₁.inr
n r : ℕ
hr : r > 0
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)

Tactic:
rw [Nat.sub_one_mul, Nat.sub_one_mul, mul_comm]

Goal state after:
case h₁.inr
n r : ℕ
hr : r > 0
⊢ r * (n % r) - r ≤ r * (n % r) - n % r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
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
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ({G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset) ≤
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

pp: case refine_2
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
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ ({G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset) ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset

Tactic:
all_goals
    simp_rw [Finset.sup_le_iff, mem_filter, mem_univ, true_and]
    intro G ⟨h_le, h_free⟩
    simp_rw [Iso.card_edgeFinset_eq (.map e₁.toEquiv G)]
    have h' : G.map e₁.toEquiv.toEmbedding ∈ univ.filter fun G ↦
        G ≤ completeBipartiteGraph _ _ ∧ K.Free G := by
      rw [mem_filter_univ, map_le_iff_le_comap]
      refine ⟨fun _ _ hadj ↦ ?_, ?_⟩
      · replace h_le := h_le hadj
        rw [← Embedding.map_adj_iff e₁.toEmbedding, ← comap_adj] at h_le
        exact h_le
      · rw [Function.Embedding.coeFn_mk, ← free_congr e₂ (.map e₁.toEquiv G)]
        exact h_free
    have h_le_sup := @le_sup _ _ _ _ _ (#·.edgeFinset) (G.map e₁.toEquiv.toEmbedding) h'
    simp_rw [← card_coe, mem_edgeFinset] at h_le_sup ⊢
    exact h_le_sup

Goal state after: