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

Goal state before:
pp: case a
n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
⊢ a * (count a p.parts * p.parts.bell) = (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)

Tactic:
have ha0 : a ≠ 0 := by grind

Goal state after:
case a
n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
ha0 : a ≠ 0
⊢ a * (count a p.parts * p.parts.bell) = (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)
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
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : ¬muFun 𝕜 a b = 0
⊢ a ≤ b

Tactic:
by
    rw [muFun_apply] at h
    split_ifs at h with hab
    · exact hab.le
    · rw [neg_eq_zero] at h
      obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h
      exact (nonempty_Ico.1 ⟨x, hx⟩).le

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

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ r' = List.take ((↑q).length - (↑p).length) ↑q

Tactic:
← h,

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ r' = List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)
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
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ k * (x ^ 1 * x ^ 1) * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1))

Tactic:
mul_comm (x ^ k),

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ 1 * x ^ 1 * x ^ k * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1))
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
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ k * (x ^ 1 * x ^ 1) * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))

Tactic:
mul_comm (x ^ k),

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ 1 * x ^ 1 * x ^ k * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0

Goal state after:
case inl
n : ℕ
hn : ↑n / 3 - 2 ≤ 0
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

case inr
n : ℕ
hn : 0 ≤ ↑n / 3 - 2
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
⊢ V(G) ⊂ V(H) ∨ E(G) ⊂ E(H)

Tactic:
simp only [ssubset_iff_subset_ne, hGH.1.vertexSet_mono, ne_eq, true_and, hGH.1.edgeSet_mono]

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
⊢ ¬V(G) = V(H) ∨ ¬E(G) = E(H)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ (X ∪ D \ X)

Tactic:
union_sdiff_self,

Goal state after:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ (X ∪ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
⊢ (M ＼ D).Spanning S ↔ M.Spanning S ∧ Disjoint S D

Tactic:
by
  simp only [spanning_iff_exists_isBase_subset', hD.delete_isBase_iff, and_assoc, delete_ground,
    subset_sdiff, and_congr_left_iff, and_imp]
  refine fun hSE hSD ↦ ⟨fun ⟨B, hB, hBD, hBS⟩ ↦ ⟨B, hB, hBS⟩, fun ⟨B, hB, hBS⟩ ↦ ⟨B, hB, ?_, hBS⟩⟩
  exact hSD.mono_left hBS

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx✝ : x ∈ sᶜ
hx : ¬↑(↑f x) < #s
⊢ (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩) ⟨x, hx✝⟩) = ⟨x, hx✝⟩

Tactic:
not_lt

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx✝ : x ∈ sᶜ
hx : #s ≤ ↑(↑f x)
⊢ (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩) ⟨x, hx✝⟩) = ⟨x, hx✝⟩
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx : ¬↑(↑f x) < #s
⊢ ↑(↑((fun x ↦
              match x with
              | (g, g') =>
                ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
                    invFun := fun n ↦
                      if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
                    left_inv := ⋯, right_inv := ⋯ },
                  ⋯⟩)
            ((fun f ↦
                ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
                    right_inv := ⋯ },
                  { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩,
                    left_inv := ⋯, right_inv := ⋯ }))
              f))
        x) =
    ↑(↑f x)

Tactic:
not_lt

Goal state after:
case neg
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx : #s ≤ ↑(↑f x)
⊢ ↑(↑((fun x ↦
              match x with
              | (g, g') =>
                ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
                    invFun := fun n ↦
                      if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
                    left_inv := ⋯, right_inv := ⋯ },
                  ⋯⟩)
            ((fun f ↦
                ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
                    right_inv := ⋯ },
                  { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩,
                    left_inv := ⋯, right_inv := ⋯ }))
              f))
        x) =
    ↑(↑f x)
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js

Tactic:
rw [← univ_sigma_preimage_mk S]

Goal state after:
case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' S) ⊆ univ.sigma Js
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ I ∪ M.closure I \ I

Tactic:
union_sdiff_self,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ I ∪ M.closure I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
obtain ⟨C', hC'ss, hC'⟩ := (hKi.contract_dep_iff.1 hC.dep).2.exists_isCircuit_subset

Goal state after:
α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: 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
n : ℕ
hn : height b < n
⊢ Nonempty (Path r b)

Tactic:
induction n generalizing b with
      | zero => exact False.elim (Nat.not_lt_zero _ hn)
      | succ n ih =>
      rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
      · exact ⟨Path.nil⟩
      · rcases ih a (lt_of_lt_of_le (height_lt e) (Nat.lt_succ_iff.mp hn)) with ⟨p⟩
        exact ⟨p.cons e⟩

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
R : Type u_2
inst✝ : Monoid R
w : {i j : V} → (i ⟶ j) → R
a : V
⊢ weight (fun {i j} ↦ w) nil = 1

Tactic:
simp [weight]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
R : Type u_2
inst✝ : Monoid R
w : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path a b
e : b ⟶ c
⊢ weight (fun {i j} ↦ w) (p.cons e) = weight (fun {i j} ↦ w) p * w e

Tactic:
simp [weight]

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

Goal state before:
pp: 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₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂

Tactic:
exact ⟨hφy, hφe⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s

Tactic:
refine ⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, notMem_erase _ _⟩, insert_erase ha⟩⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s

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) ∈ 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ 1 ≤ ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A})) / ↑↑⟨n, hn⟩

Tactic:
rw [one_le_div (Nat.cast_pos.2 hn), Nat.cast_le, filter_true_of_mem, Nat.card_Ioc, Nat.sub_zero]

Goal state after:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ ∀ x ∈ Ioc 0 ↑⟨n, hn⟩, x ∈ A
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
refine Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : s ∉ 𝒜 ∧ insert a s ∈ 𝒜
⊢ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case a
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := ⋯
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ := ⋯
sA : Finset ℕ := ⋯
sB : Finset ℕ := ⋯
⊢ image f (sA.disjSum sB) ⊆ Ioo 0 n

Tactic:
grind [mem_disjSum]

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 : Finset α
⊢ s ○ t = t ○ s

Tactic:
by
  aesop (add simp disjoint_comm, simp sup_comm)

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ {a}.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ {a} → SupIrred b

Tactic:
by simp [ha]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ t ∪ s \ t ∈ 𝒜

Tactic:
union_sdiff_self_eq_union,

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ t ∪ s ∈ 𝒜
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
apply WellFoundedLT.induction a _
  clear a
  rintro a ih
  by_cases ha : SupIrred a
  · exact ⟨{a}, by simp [ha]⟩
  rw [not_supIrred] at ha
  obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
  · exact ⟨∅, by simp [ha.eq_bot]⟩
  obtain ⟨s, rfl, hs⟩ := ih _ hb
  obtain ⟨t, rfl, ht⟩ := ih _ hc
  exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩

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 ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)

Goal state after:
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)

case neg
α : 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)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)

Goal state after:
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)

case neg
α : 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)
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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s

Tactic:
← h,

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v ≤ (b ⊔ u) \ v
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ 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 α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s

Tactic:
← h,

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ (b ⊔ u) \ v ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case refine_3
α : 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
this : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
⊢ False

Tactic:
have : v ⊆ insert w ((s ∪ v) \ u) :=
    (subset_sdiff.2 ⟨subset_union_right, hvu⟩).trans (subset_insert _ _)

Goal state after:
case refine_3
α : 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
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
⊢ False
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inr.hb
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose r

Tactic:
exact Nat.choose_pos hr'

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun t ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ∈ s.powerset
⊢ ∃ u ∈ 𝒜, s ∩ u = t

Tactic:
← h,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun t ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ∈ image (fun t ↦ s ∩ t) 𝒜
⊢ ∃ u ∈ 𝒜, s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.inr
α : 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 : Finset α
hs : (nonMemberSubfamily a 𝒜).Shatters (insert a s)
⊢ False

Tactic:
· exact aux (fun t ht ↦ (mem_nonMemberSubfamily.1 ht).2) hs <| mem_insert_self _ _

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) ≤ 1

Tactic:
rw [div_le_iff₀] <;> norm_cast

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)

𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ False

Tactic:
refine hB ?_

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ B ∈ ℬ