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

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
⊢ 0 < (map (fun x ↦ x !) m).prod * (count a m)!

Tactic:
by simp [Nat.factorial_pos]

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst✝² : Zero 𝕜
inst✝¹ : LE α
inst✝ : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
a b : α
hab : ¬a ≤ b
⊢ (c • ⇑f) a b = 0

Tactic:
by simp_rw [Pi.smul_apply, apply_eq_zero_of_not_le hab, smul_zero]

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

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < (↑(p.take (p.firstReturn + 1) ⋯)).length
⊢ count D (List.take i ↑(p.take (p.firstReturn + 1) ⋯)) < count U (List.take i ↑(p.take (p.firstReturn + 1) ⋯))

Tactic:
simp only [take, length_take, lt_min_iff] at ub ⊢

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < p.firstReturn + 1 ∧ i < (↑p).length
⊢ count D (List.take i (List.take (p.firstReturn + 1) ↑p)) < count U (List.take i (List.take (p.firstReturn + 1) ↑p))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
this :
  f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0
⊢ f i (Multiset.count i p.parts) =
    (coeff (p.toFinsuppAntidiag i)) 1 +
      ∑' (i_1 : ℕ), (coeff (p.toFinsuppAntidiag i)) (f i (i_1 + 1) • X ^ (i * (i_1 + 1)))

Tactic:
simpa [toFinsuppAntidiag, hi, hi0, coeff_X_pow]

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ (fun n ↦ (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) =O[atTop] fun n ↦
    ↑(ruzsaSzemerediNumberNat n)

Tactic:
refine .of_norm_eventuallyLE ?_
    filter_upwards [eventually_ge_atTop 6] with n hn
    have : (0 : ℝ) ≤ n / 3 - 2 := by rify at hn; linarith
    simpa [neg_mul, abs_mul, abs_of_nonneg this] using ruzsaSzemerediNumberNat_lower_bound n

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ⋂₀ c = ⋂ i, ↑i

Tactic:
exact Set.sInter_eq_iInter

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e : Set α
H : Hypergraph α
h : H.IsTrivial
⊢ e ∉ E(H)

Tactic:
by grind [IsTrivial]

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
⊢ (M ／ I).Dep {e}

Tactic:
hI.indep.contract_dep_iff,

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
⊢ Disjoint {e} I ∧ M.Dep ({e} ∪ I)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.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
i : ι
hb0 : m.degree (b i) = 0
⊢ m.leadingCoeff (b i) • f = f * b i

Tactic:
nth_rewrite 2 [eq_C_of_degree_eq_zero hb0]

Goal state after:
case h.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
i : ι
hb0 : m.degree (b i) = 0
⊢ m.leadingCoeff (b i) • f = f * C (m.leadingCoeff (b i))
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (M ／ I).Dep D ∧ Disjoint D (X \ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
hI.indep.contract_dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (Disjoint D I ∧ M.Dep (D ∪ I)) ∧ Disjoint D (X \ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
⊢ M.Dep (C ∪ X)

Tactic:
by
  rw [Dep, and_iff_left (union_subset hC (h.subset_ground.trans sdiff_subset))]
  intro hi
  rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
    and_iff_left hi] at h
  exact h.1 (subset_sdiff.1 h.2).2

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (M ／ I).Dep {e} ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
hI.indep.contract_dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ M.Dep ({e} ∪ I)) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M ／ C).Indep I ∧ I ⊆ R ↔ (M ↾ (R ∪ C)).Indep (I ∪ J) ∧ Disjoint C I

Tactic:
hJ'.contract_indep_iff,

Goal state after:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M ↾ (R ∪ C)).Indep (I ∪ J) ∧ Disjoint C I
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
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] < f r

Tactic:
show r = ![r 0, r 1] by simp [← List.ofFn_inj]

Goal state after:
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
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] < f ![r 0, r 1]
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
half_sharp :
  (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ 2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
two_nsmul,

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
half_sharp :
  (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum +
      (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b ↦ ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

Tactic:
obtain ⟨g, r, H⟩ := m.div (b := fun (p : B) ↦ p) (fun b ↦ hB b b.prop) f

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑B →₀ MvPolynomial σ R
r : MvPolynomial σ R
H :
  f = (Finsupp.linearCombination (MvPolynomial σ R) fun p ↦ ↑p) g + r ∧
    (∀ (i : ↑B), m.toSyn (m.degree (↑i * g i)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ (i : ↑B), ¬m.degree ↑i ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b ↦ ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inl
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hk : 0 ∉ A
⊢ schnirelmannDensity A ≤ 1 - (↑0)⁻¹

Tactic:
simpa using schnirelmannDensity_le_one

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

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
this : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ -
      ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
have : (m - i : ℚ) ≠ 0 := sub_ne_zero_of_ne (cast_lt.mpr h₂).ne'

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this✝¹ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
this✝ : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)
this : ↑m - ↑i ≠ 0
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ -
      ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹

Tactic:
apply le_antisymm (schnirelmannDensity_le_of_le m hm'.ne' _) _

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ (↑m)⁻¹

m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ (↑m)⁻¹ ≤ schnirelmannDensity {n | n % m = 1}
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
  simp [disjSups, filter_union, image_union]

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 t₁ t₂ : Finset α
⊢ s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂

Tactic:
by
  simp [disjSups, filter_union, image_union]

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

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

Tactic:
coe_sups,

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

Goal state before:
pp: case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Tactic:
sup_insert

Goal state after:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : f i ⊔ s.sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t
⊢ a ∉ upperClosure ↑(s ⊻ t)

Tactic:
coe_sups,

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t
⊢ a ∉ upperClosure (↑s ⊻ ↑t)
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1

Tactic:
by
  simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
hℬ : s ∈ upperClosure ↑ℬ
⊢ #(𝒜.truncatedInf s ⊓ ℬ.truncatedInf s) + #(𝒜.truncatedInf s ⊔ ℬ.truncatedInf s) =
    #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
exact card_inter_add_card_union _ _

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha : a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }
⊢ a ∈ ↑s

Tactic:
obtain ⟨i, hi, ha⟩ := a.2.supPrime.le_finset_sup.1 ha
          exact s.lower ha (Set.mem_toFinset.1 hi)

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

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint c c

pp: case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
ha : b ≠ ⊥
h : ∀ b_1 ∈ s, ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

pp: case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

pp: case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
· rwa [disjoint_self]

Goal state after:
case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
ha : b ≠ ⊥
h : ∀ b_1 ∈ s, ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
ha : b ≠ ⊥
h : ∀ b_1 ∈ s, ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

pp: case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

pp: case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
· exact h _ hc

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
h : Subsingleton V
⊢ ⊥.Preconnected

Tactic:
by simp [Preconnected]

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

Goal state before:
pp: V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
⊢ v ∈ G.support

Tactic:
obtain ⟨w, hw⟩ := exists_ne v

Goal state after:
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w : V
hw : w ≠ v
⊢ v ∈ G.support
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case cons
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
hw : w ∈ C
⊢ C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
have h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩ := h

Goal state after:
case cons
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
hw : w ∈ C
h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩
⊢ C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
⊢ range (hs.piecewise f) = ⋃ i, f i '' s i

Tactic:
refine ext fun x => ⟨?_, fun ⟨t, ⟨i, hi⟩, ht⟩ ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
⊢ x ∈ range (hs.piecewise f) → x ∈ ⋃ i, f i '' s i

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk✝ : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < ↑k
⊢ ((G.deleteEdges {e}).deleteEdges s).Reachable u v

Tactic:
rw [deleteEdges_deleteEdges, Set.union_comm]
    apply h
    grw [Set.encard_union_le, Set.encard_singleton]
    exact ENat.add_lt_add_iff_right ENat.one_ne_top |>.mpr hk

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

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

Tactic:
simp only [huv, or_false]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ p.snd = v'

Tactic:
· have : i + 1 = 0 := by
      apply hp.getVert_injOn (by rw [Set.mem_ofPred]; lia) (by rw [Set.mem_ofPred]; lia)
      rw [p.getVert_zero, hr2]
    contradiction

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b

Tactic:
exact
    reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
      fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax

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

Goal state before:
pp: case refine_2.patches.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x | x ∈ (Nonempty.some ⋯).support} ⊆ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)

Tactic:
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]

Goal state after:
case refine_2.patches.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x | x ∈ (Nonempty.some ⋯).support} ⊆ ⋃ x ∈ t, {a | a ∈ (Nonempty.some ⋯).support}
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inl.inr.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ ↑left.toLeft
j : V
hj : j ∈ ↑right.toRight
⊢ G.Adj i j

Tactic:
· rw [mem_coe, mem_toLeft] at hi
        rw [mem_coe, mem_toRight] at hj
        simpa using h hi hj

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
⊢ ∀ (x : G.Walk u v), x ∈ {w ∈ G.finsetWalkLengthLT n u v | w.IsPath} ↔ x ∈ {p | p.IsPath ∧ p.length < n}

Tactic:
simp [mem_finsetWalkLengthLT_iff, and_comm]

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

Goal state before:
pp: case cons
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u✝ v✝ u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
ih : ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet

Tactic:
obtain ⟨H₁, hH₁, ih⟩ := ih
    obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
    obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
    simpa using ⟨H, hH, (le_iff_adj.mp h₂) _ _ h_adj, fun a ha => edgeSet_mono h₁ (ih a ha)⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w = p.penultimate

Tactic:
rw [← snd_reverse]

Goal state after:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w = p.reverse.snd
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
hr : 0 < r
f : (completeGraph (Fin (r + 1))).Copy (turanGraph n r)
x y : Fin (r + 1)
d : x ≠ y
c : ↑(f x) % r = ↑(f y) % r
⊢ False

Tactic:
exact absurd c <| f.toHom.map_adj d

Goal state after: