mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ b✝ c✝ : U
p₁ : Path u b✝
e₁ : b✝ ⟶ c✝
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨b✝, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨b✝, p₁⟩ = a₂
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨c✝, p₁.cons e₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ →
      ⟨c✝, p₁.cons e₁⟩ = a₂

Tactic:
| cons p₁ e₁ ih =>

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ 1 ≤ ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A})) / ↑↑⟨n, hn⟩

Tactic:
one_le_div (Nat.cast_pos.2 hn),

Goal state after:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ ↑n ≤ ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A}))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then e ({b ∈ s | a ≤ b}.sup' ⋯ id) else e ⊤) =
    if h : e a ∈ lowerClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤

Tactic:
map_finset_sup',

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ (⇑e ∘ id) else e ⊤) =
    if h : e a ∈ lowerClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
⊢ {b}.truncatedInf a = if b ≤ a then b else ⊥

Tactic:
by
  simp only [truncatedInf, coe_singleton, upperClosure_singleton, UpperSet.mem_Ici_iff,
    id_eq]
  split_ifs <;> simp [Finset.filter_true_of_mem, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
⊢ e (s.truncatedInf a) = (map e.toEmbedding s).truncatedInf (e a)

Tactic:
have : e a ∈ upperClosure (s.map e.toEquiv.toEmbedding) ↔ a ∈ upperClosure s := by simp
  simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this]
  congr with h
  simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv,
    OrderIso.le_iff_le, id, inf'_map]

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

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (s ∪ t).truncatedInf a = t.truncatedInf a

Tactic:
by
  rw [union_comm, truncatedInf_union_left ht hs]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
by_cases h𝒜 : s ∈ lowerClosure (𝒜 : Set <| Finset α) <;>
    by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
hℬ : s ∈ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
hℬ : s ∉ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure ↑𝒜
hℬ : s ∈ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure ↑𝒜
hℬ : s ∉ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert k t

Tactic:
apply mem_insert_self

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

Goal state before:
pp: case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) +
      ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) ≤
    ↑(#(𝒜 # (Fintype.card α - (k + 1))) + #(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) /
      ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))

Tactic:
cast_add,

Goal state after:
case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) +
      ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) ≤
    (↑(#(𝒜 # (Fintype.card α - (k + 1)))) + ↑(#(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜)))) /
      ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case grind
ι : 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
x : α
_i _j : κ
a : Set α
ha✝ : x ∈ a
c : ι
hc : (fun i ↦ ⋃ (_ : i ∈ g ⁻¹' {_i}), s i) c = a
b : Set α
hb✝ : x ∈ b
d : ι
hd : (fun i ↦ ⋃ (_ : i ∈ g ⁻¹' {_j}), s i) d = b
h✝ : ¬_i = _j
hb : x ∈ s d
ha : x ∈ s c
this✝ : c = d
⊢ False

Tactic:
finish

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

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

Tactic:
rw [ENat.natCast_sInf, chromaticNumber]

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ {n' | G.Colorable n'}.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ ↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C

Tactic:
by
  simp [← card_le_chromaticNumber_iff_forall_surjective]

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

Goal state before:
pp: case calc_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s =
    ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s

Tactic:
congr with s

Goal state after:
case calc_2.e_a.e_s.e_a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ s ∈ image (insert a) u.powerset ↔ s ∈ (insert a u).powerset \ u.powerset
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

Tactic:
obtain rfl | rfl := hb

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

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
V : Type u
G : SimpleGraph V
v a b : V
hvw : G.Adj v a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = v ∨ b = a
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb✝⟩

Tactic:
obtain rfl | rfl := hb

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⟩

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⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄, v_1 ∈ w.support → ∀ ⦃w_1 : V⦄, w_1 ∈ w.support → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)

Tactic:
adj_toSubgraph_iff_mem_edges

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄, v_1 ∈ w.support → ∀ ⦃w_1 : V⦄, w_1 ∈ w.support → G.Adj v_1 w_1 → s(v_1, w_1) ∈ w.edges) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Tactic:
· simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
    rw [sup_comm, inf_comm]
    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ μ a * μ b * (f a * g b) ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))

Tactic:
← mul_assoc (μ (a ⊓ b))

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ μ a * μ b * (f a * g b) ≤ μ (a ⊓ b) * μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b))
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
⊢ ¬p.Nil

Tactic:
grind [Nil.length_eq_zero]

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h✝ : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅
hxy : ¬x = y
⊢ x ∉ (p.takeUntil y ⋯).support

Tactic:
exact notMem_support_takeUntil_support_takeUntil_subset (Ne.symm hxy) hx hyp

Goal state after:
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 = 0 ↔ A i j = 1

Tactic:
rw [← apply_ne_one_iff h, Classical.not_not]

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

Tactic:
rw [h, le_antisymm_iff]
  and_intros
  on_goal 2 =>
    replace e := e.symm
  all_goals
    rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
    intro G _ h
    apply card_edgeFinset_le_extremalNumber
    contrapose h
    exact h.trans' ⟨e.toCopy⟩

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

Goal state before:
pp: n r : ℕ
⊢ (∀ (x x_1 : Fin n), (↑x % r ≠ ↑x_1 % r) = ⊤.Adj x x_1) ↔ r = 0 ∨ n ≤ r

Tactic:
top_adj,

Goal state after:
n r : ℕ
⊢ (∀ (x x_1 : Fin n), (↑x % r ≠ ↑x_1 % r) = (x ≠ x_1)) ↔ r = 0 ∨ n ≤ r
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ⊤.Adj ⟦a⟧ ⟦b⟧ ↔ G.Adj a b

Tactic:
top_adj,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ⟦a⟧ ≠ ⟦b⟧ ↔ G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False

Tactic:
rw [hn] at ineq

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #large + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ q.length

Tactic:
hG.path_concat hp hq hadj hv,

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ (p.concat hadj).length
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, #x = r → ¬∀ ⦃x_1 : V⦄, x_1 ∈ ↑x → ∀ ⦃y : V⦄, y ∈ ↑x → x_1 ≠ y → G.Adj x_1 y

Tactic:
intro z zc

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
z : Finset V
zc : #z = r
⊢ ¬∀ ⦃x : V⦄, x ∈ ↑z → ∀ ⦃y : V⦄, y ∈ ↑z → x ≠ y → G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : G.radius = 0
⊢ Subsingleton α

Tactic:
contrapose! h
    simp [radius_ne_zero_of_nontrivial]

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.edist w✝¹ w + G.edist w w✝ ≤ 2 * G.radius

Tactic:
rw [two_mul]

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.edist w✝¹ w + G.edist w w✝ ≤ G.radius + G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n✝ r : ℕ
hr : r > 0
n : ℕ
⊢ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2

Tactic:
nth_rw 1 [← Nat.mod_add_div n r, Nat.sq_sub_sq, add_tsub_cancel_left,
        show (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) =
          (2 * ((n % r) * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r by grind]

Goal state after:
n✝ r : ℕ
hr : r > 0
n : ℕ
⊢ (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : n < r
this : #⊤.edgeFinset = n.choose 2
⊢ turanGraph n r = ⊤

Tactic:
rw [turanGraph_eq_top]

Goal state after:
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : n < r
this : #⊤.edgeFinset = n.choose 2
⊢ r = 0 ∨ n ≤ r
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
β : G.ComponentCompl K → Prop
f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)
⊢ ∀ (C : G.ComponentCompl K), β C

Tactic:
by
  apply ConnectedComponent.ind
  exact fun ⟨v, vnK⟩ => f vnK

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

Goal state before:
pp: case inr.inr.e_a.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r * (r - 1) / 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1)

Tactic:
Nat.div_mul_cancel rd,

Goal state after:
case inr.inr.e_a.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r * (r - 1) * (n' / r) + n' % r * (n' / r + 1) * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ hom ⋯ C = hom h' (hom h C)

Tactic:
change C.map _ = (C.map _).map _
  rw [ConnectedComponent.map_comp, induceHom_comp]
  rfl

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (fun x ↦ ↑(extremalNumber x H) / (H.turanDensity * ↑(x.choose 2))) atTop (𝓝 1)
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)

Tactic:
have hz : ∀ᶠ (x : ℕ) in atTop, turanDensity H * x.choose 2 ≠ 0 := by
    rw [eventually_atTop]
    refine ⟨2, fun n hn ↦ ?_⟩
    simpa [h, Nat.choose_eq_zero_iff]

Goal state after:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (fun x ↦ ↑(extremalNumber x H) / (H.turanDensity * ↑(x.choose 2))) atTop (𝓝 1)
hz : ∀ᶠ (x : ℕ) in atTop, H.turanDensity * ↑(x.choose 2) ≠ 0
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: case intro.refine_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
⊢ ∀ {a b : V},
    G.Adj a b →
      F.Adj ((u (Opposite.op (singletonFinsubgraph a))).toFun ⟨a, ⋯⟩)
        ((u (Opposite.op (singletonFinsubgraph b))).toFun ⟨b, ⋯⟩)

Tactic:
intro v v' e

Goal state after:
case intro.refine_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v v' : V
e : G.Adj v v'
⊢ F.Adj ((u (Opposite.op (singletonFinsubgraph v))).toFun ⟨v, ⋯⟩)
    ((u (Opposite.op (singletonFinsubgraph v'))).toFun ⟨v', ⋯⟩)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : (t ∪ u).Finite
⊢ Even (t ∪ u).ncard

Tactic:
rw [finite_union] at hfin
    have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu
    rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]
    exact Even.add_self u.ncard

Goal state after: