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

Goal state before:
pp: case neg
κ : Type (max v u)
inst✝ : Finite κ
h : ¬Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

Tactic:
exact ⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ B ⊆ M.E \ D

Tactic:
by simp [subset_sdiff, h.1.subset_ground, h.2]

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
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ Disjoint {e} I ∧ M.Dep (insert e I)

Tactic:
and_iff_right (by simpa using he.2),

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ M.Dep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)

Tactic:
suffices ∀ ⦃K⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I by
    simpa +contextual [IsBasis', (hIX.indep.subset hJI).contract_indep_iff,
      subset_sdiff, maximal_subset_iff, disjoint_sdiff_left,
      union_eq_self_of_subset_right hJI, hIX.indep, sdiff_subset.trans hIX.subset,
      sdiff_subset_iff, subset_antisymm_iff, union_comm J]

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
⊢ False

Tactic:
exact h.1 (subset_sdiff.1 h.2).2

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

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

Tactic:
simp only [Finsupp.coe_add, Pi.add_apply]

Goal state after:
case h.right.left
σ : 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 *
          (g' j + (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) j))) ≤
    m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = M ／ C ↾ R \ C

Tactic:
rw [contract_restrict_eq_restrict_contract _ disjoint_sdiff_right]
  simp [union_eq_self_of_subset_right hCR]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ : f ![a, b] = f ![(fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0, (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1]
asymm : (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1
⊢ (List.ofFn ![a, b]).Perm (List.ofFn ![b, a])

Tactic:
simp [List.Perm.swap]

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
q : Path r r
⊢ Path.nil = q

Tactic:
rcases q with _ | ⟨q, f⟩
        · rfl
        · exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a : V
p : Path a a
⊢ p.length = 0 ↔ p = nil

Tactic:
cases p

Goal state after:
case nil
V : Type u_1
inst✝ : Quiver V
a : V
⊢ nil.length = 0 ↔ nil = nil

case cons
V : Type u_1
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
⊢ (a✝¹.cons a✝).length = 0 ↔ a✝¹.cons a✝ = nil
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
a✝ : i ∈ h.support
⊢ (eval x) (h i) * (eval x) (Alon.P (S i) i) = 0

Tactic:
convert! mul_zero _

Goal state after:
case e'_2.e'_6
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
a✝ : i ∈ h.support
⊢ (eval x) (Alon.P (S i) i) = 0
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
rw [← not_le, le_schnirelmannDensity_iff]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ (¬∀ (n : ℕ), 0 < n → x ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n) ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ s.powerset ⊼ s.powerset = s.powerset

Tactic:
simp [← powerset_inter]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∈ A
h : A.erase i ∈ ↑(∂ 𝒜)
⊢ #(A.erase i) = r - 1

Tactic:
card_erase_of_mem hi,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∈ A
h : A.erase i ∈ ↑(∂ 𝒜)
⊢ #A - 1 = r - 1
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
a : α
ha : a ∈ ↑s
has : ∀ ⦃y : α⦄, (fun x ↦ x ∈ ↑s) y → a ≤ y → y ≤ a
⊢ ∃ a, Iic a = s

Tactic:
exact ⟨a, (hs.2 <| erase_sup_Iic ha fun b hb ↦
      le_imp_eq_iff_le_imp_ge'.2 <| has hb).resolve_left (erase_lt.2 ha).ne⟩

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 α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ v.erase y ⊆ (insert x s ∪ v) \ u

Tactic:
union_sdiff_distrib,

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 ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ v.erase y ⊆ insert x s \ u ∪ v \ u
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
this : 2 ^ Fintype.card α * #ℬ - 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
← mul_tsub,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
this : 2 ^ Fintype.card α * (#ℬ - #(𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ - 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ)
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

pp: case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

pp: case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ

Tactic:
← mul_tsub,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * (#ℬ - #(𝒜ᶜ ∩ ℬ))
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * 2 ^ Fintype.card α + #(s.biUnion f') * 2 ^ Fintype.card α ≤
    (2 ^ Fintype.card α + 2 ^ Fintype.card α) * 2 ^ Fintype.card α -
      (2 ^ Fintype.card α + 2 ^ Fintype.card α) * 2 ^ (Fintype.card α - #(cons i s hi))

Tactic:
← mul_tsub,

Goal state after:
case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * 2 ^ Fintype.card α + #(s.biUnion f') * 2 ^ Fintype.card α ≤
    (2 ^ Fintype.card α + 2 ^ Fintype.card α) * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr.inr
α : 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
a : α
ha : a ∈ s
⊢ a ∈ insert j t

Tactic:
rcases lt_trichotomy k a with (lt | rfl | gt)

Goal state after:
case mpr.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
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ insert j t

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 j t

case mpr.inr.inr.inr.inr
α : 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
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ insert j t
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 α
⊢ ∑ r ∈ range (k + 1 + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
    ↑(#(falling (Fintype.card α - (k + 1)) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))

Tactic:
rw [sum_range_succ, ← slice_union_shadow_falling_succ,
      card_union_of_disjoint (IsAntichain.disjoint_slice_shadow_falling h𝒜),
      cast_add, _root_.add_div, add_comm]

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 α
⊢ ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) +
      ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) ≤
    ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) +
      ↑(#(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
inst✝¹ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ 0 < G.degree v

Tactic:
by
  simp [degree_pos_iff_mem_support, h.support_eq_univ]

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
x✝ : x ∈ ⋃ i, f i '' s i
t : Set β
i : ι
hi : (fun i ↦ f i '' s i) i = t
ht : x ∈ t
⊢ x ∈ range (hs.piecewise f)

Tactic:
simp only [← hi, mem_image] at ht
    obtain ⟨a, ha1, ha2⟩ := ht
    refine ⟨a, ?_⟩
    simp only [hs.mem_iff_index_eq] at ha1
    simpa [hs.mem_iff_index_eq, ← ha1] using! ha2

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
hsx : G.connectedComponentMk a = i✝
hsy : i✝ = j✝
⊢ False

Tactic:
exact h hsy

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

Goal state before:
pp: V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
⊢ Surjective ⇑C

Tactic:
rw [← Finite.injective_iff_surjective]

Goal state after:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
⊢ Injective ⇑C
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case succ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this✝ : Fintype ι
this : n + 1 - 1 < card ι
⊢ (completeMultipartiteGraph V).CliqueFree (card ι)

Tactic:
exact hc.mono this

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
ih :
  (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤
    (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
this✝ : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset
this : 𝒜 ⊻ ℬ ⊆ (insert a u).powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
simpa only [powerset_sups_powerset_self, powerset_infs_powerset_self, sum_collapse,
      not_false_eq_true, *] using ih

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

Goal state before:
pp: case inl
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₁) (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂)

Tactic:
rw [← Sum.inl_getLeft s₁ hs₁, ← Sum.inr_getRight s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr]

Goal state after:
case inl
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁)) ((Subtype.val ∘ ⇑fβ) (s₂.getRight hs₂))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
w u v x : V
p : G.Walk u v
hadj : p.toSubgraph.Adj w x
⊢ ¬p.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
w u x : V
hadj : nil.toSubgraph.Adj w x
⊢ ¬nil.Nil

case cons
V : Type u
G : SimpleGraph V
w u v x v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hadj : (cons h✝ p✝).toSubgraph.Adj w x
⊢ ¬(cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v

Tactic:
rw [(Order.one_le_iff_pos.mpr h).ge_iff_eq']

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v = 1 ↔ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ G.edist u v ≤ 2

pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
· obtain ⟨w, hw⟩ := h.2.2
    rw [mem_commonNeighbors] at hw
    have := (Walk.cons hw.1 <| .cons hw.2.symm .nil).edist_le
    simp_all

Goal state after:
case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c
⊢ False

Tactic:
have : ¬c' u ↔ c' u := (c'.odd_length_iff_not_congr p).mp hOdd

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c
this : ¬c' u = true ↔ c' u = true
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

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

Tactic:
by
  have := hG.nonempty
  refine ⟨fun h ↦ ⟨⟨fun u v ↦ ?_⟩, h.1.2⟩, fun hT' ↦ ?_⟩
  · exact G.reachable_eq_of_maximal_isAcyclic T h ▸ hG.preconnected u v
  · rw [maximal_isAcyclic_iff_reachable_eq hT hT'.isAcyclic,
      T.preconnected_iff_reachable_eq_top.mp hT'.preconnected,
      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]

Goal state after: