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

Goal state before:
pp: ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst✝ : Nonempty V
⊢ Nontrivial (Digraph V)

Tactic:
use ⊥, ⊤
  have v := Classical.arbitrary V
  exact ne_of_apply_ne (·.Adj v v) (by simp)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
⊢ False

Tactic:
have hAB : A * B.transpose = 0 := by
    ext i j
    fin_cases i <;> fin_cases j <;> assumption

Goal state after:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : A * Bᵀ = 0
⊢ False
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ ↑H
⊢ x ∈ c ↔ ↑H <• x = c

Tactic:
refine ⟨fun hx => ?_, fun hx =>
    by simp only [← hx, mem_rightCoset_iff, mul_inv_cancel, SetLike.mem_coe, one_mem]⟩
  obtain ⟨⟨a⟩, rfl⟩ := hc
  change _ = _ <• _
  rw [eq_comm, smul_eq_iff_eq_inv_smul, ← op_inv, op_smul_op_smul, rightCoset_mem_rightCoset]
  rwa [← op_smul_eq_mul, op_inv, ← SetLike.mem_coe, ← Set.mem_smul_set_iff_inv_smul_mem]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
ub : min (1 + i) ((↑p).length - 1) < (↑p).length
lb : 0 < min (1 + i) ((↑p).length - 1)
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p)) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p))

Tactic:
have eq := hn.2 lb ub

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
ub : min (1 + i) ((↑p).length - 1) < (↑p).length
lb : 0 < min (1 + i) ((↑p).length - 1)
eq : count D (List.take (min (1 + i) ((↑p).length - 1)) ↑p) < count U (List.take (min (1 + i) ((↑p).length - 1)) ↑p)
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p)) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
⊢ Tendsto (fun i ↦ (X ^ (i + k + 1)).order) atTop (𝓝 ⊤)

Tactic:
order_X_pow,

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
⊢ Tendsto (fun i ↦ ↑(i + k + 1)) atTop (𝓝 ⊤)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (coeff n)
      ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))) =
    (coeff n) 0

Tactic:
rw [map_zero]

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (coeff n)
      ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))) =
    0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n < (X ^ ((k + 1) * (3 * k + 4) / 2)).order

Tactic:
order_X_pow,

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n < ↑((k + 1) * (3 * k + 4) / 2)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n < ↑((k + 1) * (3 * k + 4) / 2)

Tactic:
Nat.cast_lt,

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ n < (k + 1) * (3 * k + 4) / 2
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: case inr
α : Type u_1
H : Hypergraph α
nonempty : V(H).Nonempty ∨ E(H).Nonempty
⊢ H = ⊥ ∨ H.IsNonempty

Tactic:
| inr nonempty =>

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Semigroup M
i : ℕ
ih : ∀ (a : Stream' M), a.get i ∈ FP a
a : Stream' M
⊢ a.get (i + 1) ∈ FP a

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M ／ X = M ／ I ＼ (X \ I)

Tactic:
nth_rw 1 [← sdiff_union_of_subset hI.subset, ← dual_inj, dual_contract_delete, dual_contract,
    union_comm, ← delete_delete, ext_iff_indep]

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ (M✶ ＼ I ＼ (X \ I)).E = (M✶ ＼ I ／ (X \ I)).E ∧
    ∀ ⦃I_1 : Set α⦄, I_1 ⊆ (M✶ ＼ I ＼ (X \ I)).E → ((M✶ ＼ I ＼ (X \ I)).Indep I_1 ↔ (M✶ ＼ I ／ (X \ I)).Indep I_1)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case refine_3
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (I \ C) J

pp: case refine_4
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) J

pp: case refine_5
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) (C \ J)

pp: case refine_1
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ I \ C ∪ J ⊆ X \ C ∪ J

Tactic:
all_goals tauto_set

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ m.toSyn (m.degree (b i) + (m.degree f - m.degree (b i))) ≤ m.toSyn (m.degree f)

Tactic:
add_tsub_cancel_of_le hf

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
⊢ (M i).Indep (Sigma.mk i ⁻¹' I)

Tactic:
apply indep_of_forall_finite_subset_indep

Goal state after:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
⊢ ∀ J ⊆ Sigma.mk i ⁻¹' I, J.Finite → (M i).Indep J
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b : WideSubquiver.toType V (geodesicSubtree r)⦄ (a_1 : a ⟶ b),
    (shortestPath r a).length < (shortestPath r b).length

Tactic:
by
      rintro a b ⟨e, p, h⟩
      simp_rw [h, Path.length_cons, Nat.lt_succ_iff]
      apply shortest_path_spec

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path v w)
hba : Nonempty (Path w v)
h_same_scc : StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v
⊢ False

Tactic:
obtain ⟨rfl⟩ := h_singleton w h_same_scc

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
hw_ne : v ≠ v
hab hba : Nonempty (Path v v)
h_same_scc : StronglyConnectedComponent.mk v = StronglyConnectedComponent.mk v
⊢ False
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : (fun f ↦ φ.map f) f = (fun f ↦ φ.map f) g
⊢ f = g

Tactic:
have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : (fun f ↦ φ.map f) f = (fun f ↦ φ.map f) g
this : φ.star u (Star.mk f) = φ.star u (Star.mk g)
⊢ f = g
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v : V
hv : v ∈ p.vertices
⊢ ∃ p₁ p₂, p = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
by
  induction p with
  | nil =>
    have hxa : v = a := by
      simpa [vertices_nil, List.mem_singleton] using hv
    subst hxa
    exact ⟨Path.nil, Path.nil, by simp only [comp_nil],
      by simp only [vertices_nil, tail_cons, not_mem_nil, not_false_eq_true]⟩
  | cons pPrev e ih =>
    have hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end := by
      simpa using (mem_vertices_cons pPrev e).1 hv
    have h_case₁ : v = (pPrev.cons e).end → ∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end),
        pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail := by
      rintro rfl
      exact ⟨pPrev.cons e, Path.nil, by simp [comp_nil], by simp [vertices_nil]⟩
    have h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end →
        ∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end),
          pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail := by
      intro hxPrev hxe_ne
      obtain ⟨q₁, q₂, h_prev, h_not_tail⟩ := ih hxPrev
      let q₂' : Path v (pPrev.cons e).end := q₂.cons e
      have h_no_tail : v ∉ q₂'.vertices.tail := by grind [vertices_cons, end_cons]
      exact ⟨q₁, q₂', by simp [q₂', h_prev], h_no_tail⟩
    cases hv' with
    | inl h_in_prefix =>
      by_cases h_eq_end : v = (pPrev.cons e).end
      · exact h_case₁ h_eq_end
      · exact h_case₂ h_in_prefix h_eq_end
    | inr h_eq_end => exact h_case₁ h_eq_end

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) = fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n

Tactic:
ext ⟨n, hn⟩

Goal state after:
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A})) / ↑↑⟨n, hn⟩ = ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B})) / ↑↑⟨n, hn⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < ε

Tactic:
by_contra! h

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ∀ (n : ℕ), 0 < n → ε ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n
⊢ False
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ lowerClosure (↑s ⊼ ↑t) ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t

Tactic:
lowerClosure_infs,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ lowerClosure ↑s ⊓ lowerClosure ↑t ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
h : ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
b c : α
ha : b ⊔ c = a
⊢ b = a ∨ c = a

Tactic:
by simpa [← ha] using h ha.ge

Goal state after:
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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s

Tactic:
rw [← h, le_sdiff_right] at hva

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
⊢ ∂ 𝒜' ⊆ 𝓒 u v (∂ 𝒜)

Tactic:
rintro s hs'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
⊢ s ∈ 𝓒 u v (∂ 𝒜)
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ ((t ⊔ u) \ v).erase a = (t.erase a ⊔ u) \ v

Tactic:
· simp [← erase_sdiff_comm, erase_union_distrib, erase_eq_of_notMem hau]

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 ∈ 𝒜
⊢ a ∉ s ∩ u

Tactic:
rintro ha

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 ∈ 𝒜
ha : a ∈ s ∩ u
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : 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
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
· refine ⟨insert a u, hu.2, ?_⟩
    rw [inter_insert_of_notMem ha]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)

Tactic:
exact le_collapse_of_mem (notMem_mono inter_subset_left ‹_›) h₃
        (inter_insert_of_notMem ‹_›) <| inter_mem_infs ‹_› ‹_›

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

Goal state before:
pp: 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
⊢ v ∈ H.verts

Tactic:
by_cases hnp : p.Nil

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

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑c ∧ ↑⟨w, hw⟩ = w

Tactic:
rw [← (mem_supp_iff _ _).mp h.1]

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑(H.coe.connectedComponentMk w✝) ∧ ↑⟨w, hw⟩ = w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
hc : G.Colorable n
⊢ (SimpleGraph.map (⇑f) G).Colorable n

Tactic:
by
  obtain ⟨C⟩ := hc
  use extend f C (const β default)
  intro a b ⟨_, _, _, hadj, ha, hb⟩
  rw [← ha, f.injective.extend_apply, ← hb, f.injective.extend_apply]
  exact C.valid hadj

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n + 1 ∧ ¬G.chromaticNumber ≤ ↑n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

Tactic:
chromaticNumber_le_iff_colorable,

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n + 1 ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
inst✝ : Fintype V
⊢ ⊤.chromaticNumber = ↑(card V)

Tactic:
by
  rw [chromaticNumber_eq_card_iff_forall_surjective (selfColoring _).colorable]
  intro C
  rw [← Finite.injective_iff_surjective]
  exact Hom.injective_of_top_hom C

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber ≤ ↑1 ∧ ¬G.chromaticNumber ≤ ↑0 ↔ G = ⊥ ∧ ¬IsEmpty V

Tactic:
chromaticNumber_le_iff_colorable,

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G.Colorable 1 ∧ ¬G.chromaticNumber ≤ ↑0 ↔ G = ⊥ ∧ ¬IsEmpty V
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Colorable 1 ∧ ¬G.chromaticNumber ≤ ↑0 ↔ G = ⊥ ∧ ¬IsEmpty V

Tactic:
chromaticNumber_le_iff_colorable,

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G.Colorable 1 ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: ι : Type u_4
V : ι → Type u_5
inst✝ : Fintype ι
f : (i : ι) → V i
⊢ ↑(card ι) ≤ (completeMultipartiteGraph V).chromaticNumber

Tactic:
by_contra! h

Goal state after:
ι : Type u_4
V : ι → Type u_5
inst✝ : Fintype ι
f : (i : ι) → V i
h : (completeMultipartiteGraph V).chromaticNumber < ↑(card ι)
⊢ False
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case calc_2.e_a.e_s.e_a.refine_1
α : 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 α
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) → s.erase a ⊆ u ∧ ¬s ⊆ u

Tactic:
rintro ⟨s, hs, rfl⟩
      exact ⟨subset_insert_iff.1 <| insert_subset_insert _ hs, fun h ↦
        hu <| h <| mem_insert_self _ _⟩

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

Goal state before:
pp: case pos
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
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : v = p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2

pp: case neg
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
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2

Tactic:
· have : G.dist v w ≤ p.tail.tail.length := by
      simpa [hv, p.getVert_tail] using dist_le p.tail.tail
    lia

Goal state after:
case neg
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
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : ∃ t ∈ S, w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Tactic:
obtain ⟨t, tS, wt⟩ := hw

Goal state after:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
t : Set V
tS : t ∈ S
wt : w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : AddGroup α
inst✝¹ : One α
inst✝ : DecidableEq V
i✝ j✝ : V
⊢ adjMatrix α (completeGraph V) i✝ j✝ = (of 1 - 1) i✝ j✝

Tactic:
simp [one_apply, sub_ite]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 * r + ↑v.1 < r * t

Tactic:
conv_rhs =>
      rw [← Nat.sub_one_add_one_eq_of_pos v.2.pos, Nat.mul_add_one, mul_comm r (t - 1)]

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 * r + ↑v.1 < (t - 1) * r + r