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

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
⊢ P = 0

Tactic:
suffices MvPolynomial.rename e.symm P = 0 by
      have that := MvPolynomial.rename_injective (R := R) e.symm (e.symm.injective)
      rw [RingHom.injective_iff_ker_eq_bot] at that
      rwa [← RingHom.mem_ker, that] at this
    apply h _ (fun i ↦ S (e i))
    · intro i
      convert! Hdeg (e i)
      conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]
    · intro x hx
      simp only [MvPolynomial.eval_rename]
      apply Heval
      intro s
      simp only [Function.comp_apply]
      convert! hx (e.symm s)
      simp only [Equiv.apply_symm_apply]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = (M.closure (X ∪ C) \ C) \ X ∪ M.closure (X ∪ C) \ C ∩ X

Tactic:
sdiff_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = M.closure (X ∪ C) \ (C ∪ X) ∪ M.closure (X ∪ C) \ C ∩ X
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
this : Q = 0
⊢ P = 0

Tactic:
by
      rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_zero]

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

Goal state before:
pp: case h.right.left.right
σ : 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
j : ι
⊢ m.toSyn
      (m.degree
        (b j * (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) j)) ≤
    m.toSyn (m.degree f)

Tactic:
Finsupp.single_apply

Goal state after:
case h.right.left.right
σ : 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
j : ι
⊢ m.toSyn
      (m.degree (b j * if i = j then (monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f) else 0)) ≤
    m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝¹ :
  (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X
h' : ∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
x✝ : (i : ι) × α i
i : ι
x : α i
hx : ⟨i, x⟩ ∈ I
⊢ ⟨i, x⟩ ∈ X

Tactic:
simpa using hIX i hx

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

Goal state before:
pp: case h.right.right
σ : 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
· intro c hc i
        by_cases hc' : c ∈ r'.support
        · exact H'.2.2 c hc' i
        · convert! hf i
          classical
          have := MvPolynomial.support_add hc
          rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this
          simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b c : V
p : Path a b
b✝ c✝ : V
q' : Path b b✝
e : b✝ ⟶ c✝
ih : (p.comp q').vertices = p.vertices.dropLast ++ q'.vertices
⊢ (p.comp (q'.cons e)).vertices = p.vertices.dropLast ++ (q'.cons e).vertices

Tactic:
| cons q' e ih =>

Goal state after:
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), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.obj u'' = c✝ ∧ φ.map eu ≍ ev
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Tactic:
obtain ⟨rfl, k⟩ := k

Goal state after:
case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : φ.map eu ≍ ev
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u'', (φ.mapPath q').cons ev⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
n : ℕ
⊢ schnirelmannDensity A * ↑n ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A}))

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  exact (le_div_iff₀ (by positivity)).1 (schnirelmannDensity_le_div hn)

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

Goal state before:
pp: case insert.refine_2
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ (s : Finset α), insert a s ∈ 𝒜 → a ∉ s → s ⊆ u

Tactic:
exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
le_iff_forall_pos_lt_add

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x + ε
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜}) + #({s ∈ image (fun s ↦ s.erase a) 𝒜 | s ∉ 𝒜}) = #𝒜

Tactic:
filter_image,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜}) + #(image (fun s ↦ s.erase a) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})) = #𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ n ≤ (n - 1) / m * m + m

Tactic:
have := @Nat.lt_div_mul_add n.pred m hm'
    rwa [← Nat.succ_le_iff, Nat.succ_pred hn.ne'] at this

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}
⊢ ↑n ≤ ↑(#sA) + ↑(#sB)

Tactic:
nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
        @schnirelmannDensity_mul_le_card_filter B _ n]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s₁ s₂ t : Finset α
⊢ (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t

Tactic:
by
  simpa only [disjSups, inter_product, filter_inter_distrib] using image_inter_subset _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
hva : Disjoint v a
hua : u ≤ a
⊢ compress u v ((a ⊔ v) \ u) = a

Tactic:
by
  rw [compress_of_disjoint_of_le disjoint_sdiff_self_right
      (le_sdiff.2 ⟨(le_sup_right : v ≤ a ⊔ v), hva.mono_right hua⟩),
    sdiff_sup_cancel (le_sup_of_le_left hua), hva.symm.sup_sdiff_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
⊢ compress u v (compress u v a) = compress u v a

Tactic:
by
  unfold compress
  split_ifs with h h'
  · rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
  · rfl
  · rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅
⊢ {a ∈ 𝓒 u v s | compress u v a ∈ 𝓒 u v s} ∪ {a ∈ image (compress u v) (𝓒 u v s) | a ∉ 𝓒 u v s} = 𝓒 u v s

Tactic:
filter_image,

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅
⊢ {a ∈ 𝓒 u v s | compress u v a ∈ 𝓒 u v s} ∪ image (compress u v) ({a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s}) = 𝓒 u v s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ #({a ∈ s | compress u v a ∈ s}) + #({a ∈ image (compress u v) s | a ∉ s}) = #s

Tactic:
filter_image,

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ #({a ∈ s | compress u v a ∈ s}) + #(image (compress u v) ({a ∈ s | compress u v a ∉ s})) = #s
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ (∃ a, Iic a = s) → SupIrred s

Tactic:
rintro ⟨a, rfl⟩
    exact supIrred_Iic _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
        ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
simp_rw [← add_div, ← Nat.cast_add, card_truncatedInf_union_add_card_truncatedInf_sups]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b c : α
⊢ (b ⊔ c) \ a ≤ b \ a ⊔ c \ a

Tactic:
by rw [sup_sdiff]

Goal state after:
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 𝒜
s : Finset α
⊢ s ∈ ∂ 𝒜' → s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'

Tactic:
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
⊢ s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s

Tactic:
exact mem_insert _ _

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

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ #(s.erase (s.min' hs)) = #t

Tactic:
rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]

Goal state after:
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))
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 ∉ 𝒜} = 𝒜

Tactic:
filter_image,

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 ∈ 𝒜} ∪ image (compress U V) ({a ∈ 𝒜 | compress U V a ∉ 𝒜}) = 𝒜
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case ha
α : 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 ∈ ℬ
⊢ 0 ≤ f₄ (s ∪ t) + f₄ (s ∪ insert a t)

pp: case hbc
α : 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 ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)

Tactic:
· exact add_nonneg (h₄ _) (h₄ _)

Goal state after:
case hbc
α : 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 ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)
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 ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
⊢ ∑ x ∈ image (compress U V) 𝒜 with x ∉ 𝒜, ∑ a ∈ x, 2 ^ ↑a < ∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ x, 2 ^ ↑a

Tactic:
filter_image,

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))
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 ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
⊢ ∑ x ∈ image (compress U V) ({a ∈ 𝒜 | compress U V a ∉ 𝒜}), ∑ a ∈ x, 2 ^ ↑a <
    ∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ x, 2 ^ ↑a
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
⊢ s = {x | (mkClasses c H) x y}

Tactic:
by
  ext x
  constructor
  · intro hx _s' hs' hx'
    rwa [eq_of_mem_eqv_class H hs' hx' hs hx]
  · intro hx
    obtain ⟨b', ⟨hc, hb'⟩, _⟩ := H x
    rwa [eq_of_mem_eqv_class H hs hy hc (hx b' hc hb')]

Goal state after:
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 ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ ∑ x ∈ image Fin.val (compress U V A), 2 ^ x < ∑ x ∈ image Fin.val A, 2 ^ x

Tactic:
geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl,

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))
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 ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ toColex (image Fin.val (compress U V A)) < toColex (image Fin.val A)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
inst✝² : Nontrivial V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
⊢ 0 < G.degree v

Tactic:
exact h.degree_pos_of_nontrivial v

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
⊢ a ∈ i✝.supp → a ∉ j✝.supp

Tactic:
hsx

Goal state after:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : a ∈ i✝.supp
⊢ a ∉ j✝.supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : G.connectedComponentMk a = j✝
⊢ False

Tactic:
hsx

Goal state after:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : i✝ = j✝
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
hG : G.Colorable n
f : ι → V
hf : Pairwise fun i j ↦ G.Adj (f i) (f j)
⊢ Nat.card ι ≤ n

Tactic:
obtain ⟨C⟩ := hG

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
f : ι → V
hf : Pairwise fun i j ↦ G.Adj (f i) (f j)
C : G.Coloring (Fin n)
⊢ Nat.card ι ≤ n
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:
ENat.natCast_sInf,

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ G.chromaticNumber = ⨅ a ∈ {n' | G.Colorable n'}, ↑a

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 : ℕ
hc : G.Colorable n
⊢ n ∈ {n | G.Colorable n}

Tactic:
exact hc

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this : ↑(card V) ≤ ↑(card V) - ↑1
⊢ False

Tactic:
← ENat.natCast_sub,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this : ↑(card V) ≤ ↑(card V - 1)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → (completeGraph (Fin 2)).Adj (c a) (c b)
v w : V
hvw : G.Adj v w
⊢ v ∈ {v | c v = 0} ∧ w ∈ {v | c v = 1} ∨ v ∈ {v | c v = 1} ∧ w ∈ {v | c v = 0}

Tactic:
apply hc at hvw

Goal state after:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → (completeGraph (Fin 2)).Adj (c a) (c b)
v w : V
hvw : (completeGraph (Fin 2)).Adj (c v) (c w)
⊢ v ∈ {v | c v = 0} ∧ w ∈ {v | c v = 1} ∨ v ∈ {v | c v = 1} ∧ w ∈ {v | c v = 0}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts.Nonempty

Tactic:
rw [H.connected_iff] at h; exact h.2

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
⊢ w.toSubgraph ≤ G'

Tactic:
refine ⟨fun v' hv' ↦ ?_, fun u' v' hadj ↦ hw <| w.mem_edges_toSubgraph.mp (hadj : s(_, _) ∈ _)⟩

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : v' ∈ w.toSubgraph.verts
⊢ v' ∈ G'.verts