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

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ a ∈ A

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ b ∈ B

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inr.inl
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

Tactic:
exact ⟨a, by simp [*], b, by simp [*], by grind⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (({b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}).inf' ⋯ fun x ↦ id x) =
    ({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2

Tactic:
← image_sup_product

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 ↦ x1 ⊔ x2) ({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a})).inf' ⋯ fun x ↦ id x) =
    ({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2
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

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

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

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
simp only [Function.comp_apply, Function.iterate_succ]

Goal state after:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[k] (∂⁺ 𝒜) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
have : ∀ t : Finset α,
    (card α - #(truncatedSup {s} t) : ℚ) / ((card α - #t) * (card α).choose #t) =
    if t ⊆ s then (card α - #s : ℚ) / ((card α - #t) * (card α).choose #t) else 0 := by
    rintro t
    simp_rw [truncatedSup_singleton]
    split_ifs <;> simp
  simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq,
    ← eq_sub_iff_add_eq', supSum, ← sum_sub_distrib, ← sub_div]
  rw [sum_congr rfl fun t _ ↦ this t, sum_ite, sum_const_zero, add_zero, filter_subset_univ,
    sum_powerset, ← binomial_sum_eq ((card_lt_iff_ne_univ _).2 hs), eq_comm]
  refine sum_congr rfl fun n _ ↦ ?_
  rw [mul_div_assoc, ← nsmul_eq_mul]
  exact sum_powersetCard n s fun m ↦ (card α - #s : ℚ) / ((card α - m) * (card α).choose m)

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s

Tactic:
exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
⊢ #s + 1 = #t

Tactic:
by
    rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
⊢ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose (Fintype.card α / 2)))⁻¹ ≤ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s))⁻¹

Tactic:
gcongr with s hs

Goal state after:
case hb
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
s : Finset α
hs : s ∈ 𝒜
⊢ 0 < ↑((Fintype.card α).choose #s)

case a
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
s : Finset α
hs : s ∈ 𝒜
⊢ (Fintype.card α).choose #s ≤ (Fintype.card α).choose (Fintype.card α / 2)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

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

Tactic:
contrapose! a

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} = 𝒜
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ a ∈ {x | r x b}

Tactic:
← h_eq

Goal state after:
case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ a ∈ {x | r x a}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp

Tactic:
by
  ext v
  simp_rw [Set.mem_iUnion]
  refine ⟨fun ⟨_, ⟨hi, hi'⟩⟩ ↦ hi hi', ?_⟩
  intro hv
  use G.connectedComponentMk v
  use c'.connectedComponentMk_supp_subset_supp h hv
  simp only [mem_supp_iff]

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

Goal state before:
pp: case left
ι : 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 : κ
⊢ g ⋯.some = k

Tactic:
simpa using ((singleton_nonempty k).preimage hg).some_mem

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

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

Tactic:
Nat.sInf_def

Goal state after:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable (↑(Nat.find ?m.12)).toNat

V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
⊢ ¬w.Nil

Tactic:
rintro ⟨⟩

Goal state after:
V : Type u
G : SimpleGraph V
u x : V
hxu : x ≠ u
hx : (G.neighborSet x).Subsingleton
w : V
hxv : x ≠ u
hw : Walk.nil.IsTrail
hxw : x ∈ Walk.nil.support
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
| ∑ x ∈ t.attach, #(G.neighborFinset ↑x)

Tactic:
rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
w : ↥t
| #(bipartiteBelow G.Adj s ↑w)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ g b)

Tactic:
← sup_eq_union,

Goal state after:
case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ⊔ g b)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ G.edgeSet.encard ≤ s.encard * t.encard

Tactic:
grw [hG.edgeSetEmbeddingCompleteBipartiteGraph.encard_le]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ (completeBipartiteGraph ↑s ↑t).edgeSet.encard ≤ s.encard * t.encard
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ ↑w✝.length

Tactic:
← Walk.length_map (.ofLE h)

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ ↑(Walk.map (Hom.ofLE h) w✝).length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ ↑(Walk.map (Hom.ofLE h) w✝).length

Tactic:
apply edist_le

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ w✝.length

Tactic:
← Walk.length_map (.ofLE h)

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ (Walk.map (Hom.ofLE h) w✝).length
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case neg.refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y

Tactic:
have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h

Goal state after:
case neg.refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : ↑w.length = (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ nil ∈ {p | p.length = n + 1} ↔ nil ∈ ⋃ w, ⋃ (h : G.Adj u w), cons h '' {p' | p'.length = n}

Tactic:
simp [eq_comm]

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
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
w : V
hw : w ∈ {default}ᶜ
⊢ ¬(f w).Nil

Tactic:
case =>

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
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}ᶜ
⊢ ((f a).firstDart ⋯).edge ∈ G.edgeFinset

Tactic:
case =>

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
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 ⋯).edge = ((f b).firstDart ⋯).edge
h' : (f a).length ≤ (f b).length
⊢ a = b

Tactic:
dart_edge_eq_iff

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 : ℕ
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:
h'

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' : 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}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

Tactic:
case =>

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
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
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
⊢ False

Tactic:
case =>

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
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
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = b

Tactic:
case =>

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

Goal state before:
pp: case inj'.inl
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : i₁ = i₂ → j₁ ≠ j₂
heq : i₁ = i₂
⊢ ↑((fₜ (fᵣ i₁)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)

Tactic:
heq,

Goal state after:
case inj'.inl
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : i₁ = i₂ → j₁ ≠ j₂
heq : i₁ = i₂
⊢ ↑((fₜ (fᵣ i₂)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
this : Set.univ = ↑C
⊢ False

Tactic:
exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
⊢ ↑(#K.verts) * (↑G.minDegree - ↑(#K.verts)) ≤ ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset)

Tactic:
rw [← isBipartiteWith_sum_degrees_eq_card_edges (between_verts_isBipartiteWith K),
    ← nsmul_eq_mul, ← sum_const, Nat.cast_sum]
  exact sum_le_sum (fun v hv ↦ sub_le_iff_le_add.mpr <|
    mod_cast (G.minDegree_le_degree v).trans (degree_le_between_add hv))

Goal state after:
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
v v' : V
e : G.Adj v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ F.Adj
    (((ConcreteCategory.hom ((G.finsubgraphHomFunctor F).map hv)) (u (Opposite.op (finsubgraphOfAdj e)))).toFun ⟨v, ⋯⟩)
    ((u (Opposite.op (singletonFinsubgraph v'))).toFun ⟨v', ⋯⟩)

Tactic:
← hu hv'

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'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ F.Adj
    (((ConcreteCategory.hom ((G.finsubgraphHomFunctor F).map hv)) (u (Opposite.op (finsubgraphOfAdj e)))).toFun ⟨v, ⋯⟩)
    (((ConcreteCategory.hom ((G.finsubgraphHomFunctor F).map hv')) (u (Opposite.op (finsubgraphOfAdj e)))).toFun
      ⟨v', ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.egirth = ⊤ ↔ G.IsAcyclic

Tactic:
simp [egirth, IsAcyclic]

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
  rw [← finsum_one, finsum_mem_biUnion h ht hs, finsum_mem_congr rfl fun i hi ↦ finsum_one]

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
x✝ : ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ ↑e
⊢ v ∈ M.verts

Tactic:
exact mem_verts_of_mem_edge he hv

Goal state after: