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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : ↑(#(B * A)) < K * ↑(#A)
hx : x ∈ B⁻¹ * B
⊢ (2 - K) * ↑(#A) < ↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x}))

Tactic:
simp only [mem_mul, mem_inv, exists_exists_and_eq_and] at hx

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : ↑(#(B * A)) < K * ↑(#A)
hx : ∃ a ∈ B, ∃ z ∈ B, a⁻¹ * z = x
⊢ (2 - K) * ↑(#A) < ↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x}))
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : ¬((crossProduct a) b = 0 ∨ (crossProduct c) d = 0)
⊢ False

Tactic:
simp_rw [not_or, ← ne_eq, crossProduct_ne_zero_iff_linearIndependent] at h

Goal state after:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
⊢ False
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z : G
⊢ z ∈ a •> ((A⁻¹ * A) <• a) → z ∈ A * A

Tactic:
hz

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z : G
hz : z ∈ a •> ((A⁻¹ * A) <• a)
⊢ z ∈ A * A
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = ↑p

Tactic:
← p.toList.dropLast_append_getLast h',

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = (↑p).dropLast ++ [(↑p).getLast h']
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ [U].length ≤ i

Tactic:
length_singleton

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ 1 ≤ i
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < [U].length + (↑p).length + [D].length
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))

Tactic:
length_singleton

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ [U].length ≤ i

Tactic:
length_singleton

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ 1 ≤ i
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
hc : 0 < a ! * c
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) = (m.sum + a).choose a * m.bell

Tactic:
apply Nat.eq_of_mul_eq_mul_right hc

Goal state after:
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ⋯
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := ⋯
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
hc : 0 < a ! * c
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a).choose a * m.bell * (a ! * c)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ count D ↑p + count U ↑p = (↑p).length

Tactic:
convert! (p.toList.length_eq_countP_add_countP (· == D)).symm

Goal state after:
case e'_6
p : DyckWord
⊢ count U = countP fun a ↦ decide ¬(a == D) = true
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q))

Tactic:
rw [take_append, show p.firstReturn + 1 - p.toList.length = 0 by lia,
        take_zero, append_nil, count_take_firstReturn_add_one h]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : BoundedOrder α
⊢ eulerChar 𝕜 αᵒᵈ = eulerChar 𝕜 α

Tactic:
by
  simp [eulerChar, ← mu_toDual 𝕜 (α := α)]

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

Goal state before:
pp: p : DyckWord
⊢ [U].length + (↑p).length + [D].length ≤ (↑p).length + 1 + 1

Tactic:
length_singleton

Goal state after:
p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
⊢ False

Tactic:
let κ := connectivity K S

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
⊢ False
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
⊢ ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S) ∧ ↑(#Z) ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z

Tactic:
let κ := connectivity K S

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
⊢ ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S) ∧ ↑(#Z) ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))

Tactic:
have h := fun n ↦ tprod_one_sub_pow_eq_powMulProdOneSubPow n hx hsum hlhs

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#(↑H).toFinset) * ↑(#Z) / ↑(#(↑H).toFinset) = ↑(#((↑H).toFinset * Z)) / ↑(#(↑H).toFinset)

Tactic:
simp [← card_mul_eq_mul_card_of_injOn_opSMul hZinj, Nat.cast_mul]

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

Goal state before:
pp: case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))

Tactic:
norm_cast
      exact rothNumberNat_le_ruzsaSzemerediNumberNat _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y

Tactic:
by
    simp_rw [← hIsLink, ← hedgeSet]
    exact G.edge_mem_iff_exists_isLink

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : G.Inc e x
⊢ (bouquet v E(G)).Inc e x

pp: case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : (bouquet v E(G)).Inc e x
⊢ G.Inc e x

Tactic:
· simp [← mem_singleton_iff, ← hrw, h.edge_mem, h.vertex_mem]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : (bouquet v E(G)).Inc e x
⊢ G.Inc e x
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case ht
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}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∀ m_1 ∈ (fun x ↦ x * m) '' N, ∀ m' ∈ (fun x ↦ x * m) '' N, m_1 * m' ∈ (fun x ↦ x * m) '' N

Tactic:
rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩

Goal state after:
case ht
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}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
m'' : M
hm'' : m'' ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x ↦ x * m) m'' * (fun x ↦ x * m) m' ∈ (fun x ↦ x * m) '' N
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ (M ＼ D).IsBasis I X

Tactic:
by
  rw [delete_isBasis_iff]; exact ⟨h, hX⟩

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

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

Tactic:
inter_eq_left

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) \ D ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
hXD : Disjoint X D
⊢ (M ＼ D).closure X = M.closure X \ D

Tactic:
delete_closure_eq,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
hXD : Disjoint X D
⊢ M.closure (X \ D) \ D = M.closure X \ D
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
⊢ ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l

Tactic:
obtain ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension α κ η

Goal state after:
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
⊢ ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
aux : ∀ {K : Set α}, (M ／ K).IsCircuit C → M.Indep K → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hI : M.IsBasis' I K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
rw [hI.contract_eq_contract_delete, delete_isCircuit_iff] at hC

Goal state after:
case inr
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α}, (M ／ K).IsCircuit C → M.Indep K → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case succ.inl
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)
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
hn : height r < n + 1
⊢ Nonempty (Path r r)

Tactic:
exact ⟨Path.nil⟩

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

Goal state before:
pp: case nil
V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
a b : Symmetrify V
⊢ Nonempty (Path a a)

Tactic:
exact ⟨Path.nil⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
insert_erase ha

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
insert_erase ha

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ a

Tactic:
rw [← hba, le_sdiff]

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
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ b ⊔ u ∧ Disjoint u v
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
⊢ α ↪o Set { a // SupIrred a }

Tactic:
by_cases! h : IsEmpty α
  · exact OrderEmbedding.ofIsEmpty
  have := Fintype.toOrderBot α
  exact OrderIso.lowerSetSupIrred.toOrderEmbedding.trans ⟨⟨_, SetLike.coe_injective⟩, Iff.rfl⟩

Goal state after:
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 ∈ 𝒜
⊢ r ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
    refine card_le_card ?_
    simp_rw [image_subset_iff, mem_bipartiteBelow]
    exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩

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

Goal state before:
pp: case pos.refine_3
α : 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₁ (insert a s) * f₂ (insert a t) ≤ f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t)

Tactic:
simpa [*] using h ‹insert a s ⊆ _› ‹insert a t ⊆ _›

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
⊢ t ⊆ s → s ∈ ↑𝒜.shatterer → t ∈ ↑𝒜.shatterer

Tactic:
by simpa using Shatters.mono_right

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
⊢ insert a (t.erase a) = t

Tactic:
insert_erase ha

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
⊢ t = t
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x | r x z}
hx : x ∈ c
hy : y ∈ c
⊢ r x y

Tactic:
by
    subst c
    exact r.trans' hx (r.symm' hy)

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

Goal state before:
pp: n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r ↑𝒜
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)

Tactic:
by
  -- WLOG `|𝒜| = |𝒞|`
  obtain ⟨𝒜', h𝒜, h𝒜𝒞⟩ := exists_subset_card_eq h𝒞𝒜
  -- By `kruskal_katona_helper`, we find a fully compressed family `ℬ` of the same size as `𝒜`
  -- whose shadow is no bigger.
  obtain ⟨ℬ, hℬ𝒜, h𝒜ℬ, hℬr, hℬ⟩ := UV.kruskal_katona_helper 𝒜' (h𝒜r.mono (by gcongr))
  -- This means that `ℬ` is an initial segment of the same size as `𝒞`. Hence they are equal and
  -- we are done.
  suffices ℬ = 𝒞 by subst 𝒞; exact hℬ𝒜.trans (by gcongr)
  have hcard : #ℬ = #𝒞 := h𝒜ℬ.symm.trans h𝒜𝒞
  obtain h𝒞ℬ | hℬ𝒞 := h𝒞.total (UV.isInitSeg_of_compressed hℬr hℬ)
  · exact (eq_of_subset_of_card_le h𝒞ℬ hcard.le).symm
  · exact eq_of_subset_of_card_le hℬ𝒞 hcard.ge

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C✝ : G.Coloring α
inst✝² : Nonempty (G.Coloring α)
inst✝¹ : Nontrivial α
inst✝ : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ C v
⊢ Nontrivial (G.Coloring α)

Tactic:
refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C✝ : G.Coloring α
inst✝² : Nonempty (G.Coloring α)
inst✝¹ : Nontrivial α
inst✝ : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ C v
h : (Iso.completeGraph (Equiv.swap (C v) c)).toHom.comp C = C
⊢ c = C v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

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

pp: V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ {n' | G.Colorable n'}.Nonempty

Tactic:
chromaticNumber

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n = ⨅ 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
⊢ G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n

Tactic:
chromaticNumber

Goal state after:
V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≠ ⊤ ↔ ∃ n, G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≤ G'.chromaticNumber

Tactic:
chromaticNumber

Goal state after:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≤ ⨅ n ∈ Set.ofPred G'.Colorable, ↑n
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c 0 = ∅

Tactic:
simp [ball]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c 1 = {c}

Tactic:
simp [ball]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c v : V
⊢ v ∈ G.ball c ⊤ ↔ G.Reachable v c

Tactic:
simp [lt_top_iff_ne_top, edist_ne_top_iff_reachable]

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

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
⊢ ¬(G ⊕g H).Reachable (Sum.inl v) (Sum.inr w)

Tactic:
by
  rintro ⟨p⟩
  have hs : ∀ x : V ⊕ W, x ∉ Set.range .inl ↔ x ∈ Set.range .inr := by simp
  obtain ⟨⟨d, hadj⟩, _, hd1, hd2⟩ := p.exists_boundary_dart (Set.range .inl) (by simp) (by simp)
  simp only [hs] at hadj hd1 hd2
  obtain ⟨v', hv'⟩ := hd1
  obtain ⟨w', hw'⟩ := hd2
  rw [← hv', ← hw'] at hadj
  exact not_adj_sum_inl_inr _ _ hadj

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

Goal state before:
pp: n : ℕ
v : Fin (n + 2)
⊢ (cycleGraph (n + 2)).degree v = {v - 1, v + 1}.card

Tactic:
SimpleGraph.degree,

Goal state after:
n : ℕ
v : Fin (n + 2)
⊢ ((cycleGraph (n + 2)).neighborFinset v).card = {v - 1, v + 1}.card
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
u : V
p : (sSup Hs).Walk u u
hp : p.IsCycle
⊢ False

Tactic:
obtain ⟨H, hH, hpH⟩ := p.exists_mem_contains_edges_of_directed Hs hnemp h_dir

Goal state after:
case inr
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
u : V
p : (sSup Hs).Walk u u
hp : p.IsCycle
H : SimpleGraph V
hH : H ∈ Hs
hpH : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ False