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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
i : ℕ
⊢ 1 - X ^ ((i + 1) * m) = (∑ j ∈ range m, X ^ ((i + 1) * j)) * (1 - X ^ (i + 1))

Tactic:
pow_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
i : ℕ
⊢ 1 - (X ^ (i + 1)) ^ m = (∑ x ∈ range m, (X ^ (i + 1)) ^ x) * (1 - X ^ (i + 1))
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ stirlingFirst 0 (n✝ + 1) = 0

Tactic:
rw [stirlingFirst]

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

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ ruzsaSzemerediNumber (α ⊕ α ⊕ α) = ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
      ring_nf

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.restrict F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∈ F

Tactic:
by
  simp [← isLink_self_iff, and_comm]

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

Goal state before:
pp: M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this✝² : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x ↦ x * p
m : M
hm : m ∈ s
idem : ⟨m, hm⟩ * ⟨m, hm⟩ = ⟨m, hm⟩
⊢ ∃ m ∈ s, m * m = m

Tactic:
exact ⟨m, hm, Subtype.ext_iff.mp idem⟩

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

Goal state before:
pp: α : Type u_1
H : Hypergraph α
h : H.IsComplete
⊢ ¬H.IsTrivial

Tactic:
intro hH

Goal state after:
α : Type u_1
H : Hypergraph α
h : H.IsComplete
hH : H.IsTrivial
⊢ False
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.cons'.refine_2
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
this : n ∈ {m | elem p * m ∈ ↑p}
⊢ (Stream'.corec elem succ p).head * n ∈ ↑p

Tactic:
simpa only using! this

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
⊢ FP (Stream'.drop i a).tail (a.get j)

Tactic:
have := FP.singleton (a.drop i).tail d

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
this : (Stream'.drop i a).tail.get d ∈ FP (Stream'.drop i a).tail
⊢ FP (Stream'.drop i a).tail (a.get j)
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
i : ι
hb0 : m.degree (b i) = 0
j : ι
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

Tactic:
by_cases hj : j = i

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
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

case neg
σ : 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
j : ι
hj : ¬j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ↾ (M.E \ C) \ D = (M ↾ M.E \ D) ／ C

Tactic:
sdiff_sdiff_comm,

Goal state after:
α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ↾ (M.E \ D) \ C = (M ↾ M.E \ D) ／ C
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
⊢ r = ![r 0, r 1]

Tactic:
simp [← List.ofFn_inj]

Goal state after:
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
contr : AdmitsFractional f ω
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ False

Tactic:
specialize contr ![![a, b], ![b, a]]

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 • ∑ i, f (![![a, b], ![b, a]] i)
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ False
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path i i₀
p₂ : Path j₀ j
p : Path i j := p₁.comp (e₀.toPath.comp p₂)
hp_pos : 0 < p.length
⊢ ∃ p, 0 < p.length

Tactic:
exact ⟨p, hp_pos⟩

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
⊢ (mapDomain (fun x ↦ i) e) j = (single i (e ())) j

Tactic:
by_cases hj : j = i

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : j = i
⊢ (mapDomain (fun x ↦ i) e) j = (single i (e ())) j

case neg
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ (mapDomain (fun x ↦ i) e) j = (single i (e ())) j
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
h : nil.vertices ≠ []
⊢ nil.vertices.head h = a

Tactic:
simp only [vertices_nil, head_cons]

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:
by
  cases p <;> tauto

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

Goal state before:
pp: case cons.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (φ.map e₁) ≍ (φ.mapPath p₂).cons (φ.map e₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
rw [← Path.cast_eq_iff_heq rfl hφy, Path.cast_cons, Path.cast_rfl_rfl] at h'

Goal state after:
case cons.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

Tactic:
let n : ℕ := ⌊#A / ε⌋₊ + 1

Goal state after:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
⊢ a = b

Tactic:
have h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v := by
    dsimp at hab
    rw [hab]

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ a = b
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ a = b

Tactic:
sdiff_sdiff_comm,

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : ((a ⊔ u) \ u) \ v ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ a = b
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : a \ v ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ a = b

Tactic:
sdiff_sdiff_comm,

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : a \ v ⊔ v = ((b ⊔ u) \ u) \ v ⊔ v
⊢ a = b
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
by_cases h : compress u v a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s
h : compress u v a ∉ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ infSum 𝒜 = 1

Tactic:
rw [← compls_compls 𝒜, eq_sub_of_add_eq (infSum_compls_add_supSum _),
    supSum_of_univ_notMem h𝒜₁.compls, add_sub_cancel_left]

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ univ ∉ 𝒜ᶜˢ
Module: Mathlib.Combinatorics.SetFamily.LYM

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

Tactic:
simp_rw [image_subset_iff, mem_bipartiteBelow]

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s
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 α - #(cons i s hi)))

Tactic:
← mul_two,

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 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ 𝒜.Shatters univ ↔ 𝒜 = univ

Tactic:
by
  rw [shatters_iff, powerset_univ]; simp_rw [univ_inter, image_id']

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

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

Tactic:
| _ b
     => 

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ Reachable ?m.15 (?m.16 (φ.symm v)) (?m.16 u) ↔ G'.Reachable v (φ u)

pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ Type ?u.26

pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ SimpleGraph ?m.13

pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ G ≃g ?m.15

Tactic:
RelIso.apply_symm_apply

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ G'.Reachable v (φ u) ↔ G'.Reachable v (φ u)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
s : Set V
x✝ : Maximal (fun x ↦ (induce x G).Connected) s
hconn : (fun x ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun x ↦ (induce x G).Connected) y → s ⊆ y → y ⊆ s
⊢ ∃ C, C.supp = s

Tactic:
have ⟨v, hv⟩ := hconn.nonempty

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
s : Set V
x✝ : Maximal (fun x ↦ (induce x G).Connected) s
hconn : (fun x ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun x ↦ (induce x G).Connected) y → s ⊆ y → y ⊆ s
v : V
hv : v ∈ s
⊢ ∃ C, C.supp = s
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)

Tactic:
by
      refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
      · rwa [card_powersetCard, card_attachFin, card_range]
      simp_rw [𝒞, mem_powersetCard]
      rintro A B hA ⟨HB₁, HB₂⟩
      refine ⟨fun t ht ↦ ?_, ‹_›⟩
      rw [mem_attachFin, mem_range]
      have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
        rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
      apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
      simp_rw [mem_image]
      rintro _ ⟨a, ha, hab⟩
      simpa [range'k, hab] using hA.1 ha

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 u : V
huv : u ≠ v
⊢ ∃ u, G.Adj v u

Tactic:
have ⟨w⟩ := h v u

Goal state after:
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v u : V
huv : u ≠ v
w : G.Walk v u
⊢ ∃ u, G.Adj v u
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
u v : V
⊢ (G.deleteEdges {s(u, v)}).IsBridge s(u, v) ↔ G.IsBridge s(u, v)

Tactic:
simp [isBridge_iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
hb : G.IsBridge e
he : e ∈ G.edgeSet
⊢ (G ⊔ edge u v).IsBridge e

Tactic:
refine (isBridge_iff_forall_cycle_notMem (edgeSet_mono le_sup_left he)).mpr ?_
  refine fun w p hp hpe ↦ (isBridge_iff_forall_cycle_notMem he).mp hb
    (p.transfer G fun e' he' ↦ ?_) (hp.transfer _) (Walk.edges_transfer p _ ▸ hpe)
  refine edgeSet_sup .. ▸ Walk.edges_subset_edgeSet _ he' |>.elim id fun h' ↦ h ?_ |>.elim
  exact .mono (sdiff_le_iff'.mpr le_rfl) <|
    adj_and_reachable_delete_edges_iff_exists_cycle.mpr ⟨_, p, by simp_all⟩ |>.right

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
⊢ G.CliqueFree m

Tactic:
by_contra h
  simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h
  obtain ⟨s, h, rfl⟩ := h
  exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)

Goal state after:
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)
⊢ Disjoint {v | c v = 0} {v | c v = 1}

Tactic:
by aesop (add simp [Set.disjoint_left])

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : ¬G.IsEdgeReachable 2 u x
e : Sym2 V
he : ¬(G.deleteEdges {e}).Reachable u x
he' : ¬(G.deleteEdges {e}).Reachable v x
hy : x ∈ w.support
⊢ e ∈ (w.dropUntil x hy).edges

Tactic:
by simpa using (w.dropUntil x _).reverse.mem_edges_of_not_reachable_deleteEdges he'

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
⊢ ∃ C, C.toSubgraph = G'

Tactic:
have ⟨v, hv⟩ := hconn.nonempty

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
v : V
hv : v ∈ G'.verts
⊢ ∃ C, C.toSubgraph = G'
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : G.Reachable u w
⊢ ↑(G.dist u w) ≤ ↑(G.dist u v + G.dist v w)

Tactic:
ENat.natCast_add

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : G.Reachable u w
⊢ ↑(G.dist u w) ≤ ↑(G.dist u v) + ↑(G.dist v w)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
⊢ (∑ a, μ a * f a) * ∑ a, μ a * g a ≤ (∑ a, μ a) * ∑ a, μ a * (f a * g a)

Tactic:
refine four_functions_theorem_univ (μ * f) (μ * g) μ _ (mul_nonneg hμ₀ hf₀) (mul_nonneg hμ₀ hg₀)
    hμ₀ (mul_nonneg hμ₀ <| mul_nonneg hf₀ hg₀) (fun a b ↦ ?_)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ (μ * f) a * (μ * g) b ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : G.Reachable u w
⊢ ↑(G.dist u w) ≤ ↑(G.dist u v + G.dist v w)

Tactic:
ENat.natCast_add

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : G.Reachable u w
⊢ ↑(G.dist u w) ≤ ↑(G.dist u v) + ↑(G.dist v w)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: 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.getVert (i + 1) = p.getVert 0

Tactic:
rw [p.getVert_zero, hr2]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Walk.boxProdRight G a (cons' x y z h w)).ofBoxProdRight = cons' x y z h w

Tactic:
by
    rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
      Walk.boxProdRight]
    · simp [ofBoxProdRight_boxProdRight]
    · exact ⟨h, rfl⟩

Goal state after: