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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
hi : m ∣ i + 1
⊢ ∃ j, j ≠ 0 ∧ j * m - 1 = i

Tactic:
obtain ⟨j, hj⟩ := dvd_def.mp hi

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
⊢ ∃ j, j ≠ 0 ∧ j * m - 1 = i
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : 0 < expansion K S A
⊢ A.Nonempty

Tactic:
by_contra! rfl

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
hA : 0 < expansion K S ∅
⊢ False
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : IsFragment K S A
⊢ A.Nonempty

Tactic:
by_contra! rfl

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
hA : IsFragment K S ∅
⊢ False
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case ht.refine_2
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
scaling_eq_self : (fun x ↦ x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' * m = m

Tactic:
mul_assoc,

Goal state after:
case ht.refine_2
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
scaling_eq_self : (fun x ↦ x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * (m' * m) = m
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a

Tactic:
let S : Set (Ultrafilter M) := ⋂ n, { U | ∀ᶠ m in U, m ∈ FP (a.drop n) }

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
⊢ (∃ D ⊆ M.E, N = M ＼ D) → N ≤r M

Tactic:
by rintro ⟨D, -, rfl⟩; apply delete_isRestriction

Goal state after:
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:
rw [delete_closure_eq, hXD.sdiff_eq_left]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ (C₁ ∪ C₂)

Tactic:
simp [← dual_inj]

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

Goal state before:
pp: case hnc
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ ¬↑hb.unit⁻¹ * m.leadingCoeff f = 0

Tactic:
· simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]

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

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

Tactic:
← inter_sdiff_assoc,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
h : (M ／ J).IsBasis (I \ J) ((X ∩ M.E) \ J)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
have h := (hIX.isBasis'.contract_isBasis'_sdiff_of_subset hJI).isBasis_inter_ground
  rwa [contract_ground, ← inter_sdiff_assoc, inter_eq_self_of_subset_left hIX.subset_ground] at h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ (M ／ I).IsBasis J X

Tactic:
refine (isBasis'_iff_isBasis ?_).1 <| h.isBasis'.contract_isBasis_union_union hJI hXI
  rw [contract_ground, subset_sdiff, and_iff_left hXI]
  exact subset_union_left.trans h.subset_ground

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ (M ／ C).IsBasis (I \ C) (X \ C)

Tactic:
hJC.contract_eq_contract_delete,

Goal state after:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ (M ／ J ＼ (C \ J)).IsBasis (I \ C) (X \ C)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ (M ／ (C \ K)).IsCircuit K

Tactic:
by
  simpa [inter_eq_self_of_subset_right hKC] using hC.contract_isCircuit (C := C \ K) <|
    by rwa [sdiff_ssubset_left_iff, inter_eq_self_of_subset_right hKC]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sigma M).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩
  simp only [sigma_indep_iff] at hI ⊢
  intro i
  apply indep_of_forall_finite_subset_indep
  intro J hJI hJ
  convert! hI (Sigma.mk i '' J) (by simpa) (hJ.image _) i
  rw [sigma_mk_preimage_image_eq_self]

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

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

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

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ B = B ∩ M.E ∪ B ∩ N.E

Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hB.2.2]

Goal state after:
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
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
this : ∀ (p q : Path r b), p = q
⊢ ∀ (a : Path r b), a = default

Tactic:
by
        intro p
        apply this

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

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v) →
    ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))

Tactic:
intro h_singleton w hw_ne h_bidir

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
w : V
hw_ne : w ≠ v
h_bidir : Nonempty (Path v w) ∧ Nonempty (Path w v)
⊢ False
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
a✝ : b✝ ⟶ c✝
ih : ∀ (h : p'.vertices ≠ []), p'.vertices.head h = a
h : (p'.cons a✝).vertices ≠ []
⊢ (p'.cons a✝).vertices.head h = a

Tactic:
| cons p' _ ih =>

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

Goal state before:
pp: case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inl f⟩)

Tactic:
Equiv.sigmaSumDistrib_apply,

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inl f⟩)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inr g⟩)

Tactic:
Equiv.sigmaSumDistrib_apply,

Goal state after:
case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inr g⟩)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj (φ.obj u)) (Hom (Symmetrify.of.obj (φ.obj u))))
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inl f⟩)

Tactic:
Equiv.sigmaSumDistrib_apply,

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inl f⟩)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj (φ.obj u)) (Hom (Symmetrify.of.obj (φ.obj u))))
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inr g⟩)

Tactic:
Equiv.sigmaSumDistrib_apply,

Goal state after:
case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inr g⟩)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v : V
hv : v ∈ p.vertices
⊢ ∃ p₁ p₂, p = p₁.comp p₂

Tactic:
obtain ⟨n, hn, rfl⟩ : ∃ n, ∃ hn : n < p.vertices.length, v = p.vertices[n] :=
    exists_mem_iff_getElem.mp ⟨v, hv, rfl⟩
  obtain ⟨v, p₁, p₂, hp, hv, rfl⟩ := p.exists_eq_comp_and_length_eq_of_lt_length n hn
  exact ⟨p₁, p₂, hp⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ

Tactic:
by
  simp_rw [memberSubfamily, filter_union, image_union]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
wlog hε₁ : ε ≤ 1 generalizing ε

Goal state after:
case inr
A : Finset ℕ
ε : ℝ
hε : 0 < ε
this : ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
hε₁ : ¬ε ≤ 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t

Tactic:
rintro ⟨v, hv, w, hw, rfl⟩
    exact union_subset_union hv hw

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

Goal state before:
pp: α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
a b : α
⊢ (b ⊔ a) \ (b \ a) = a

Tactic:
sup_sdiff,

Goal state after:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
a b : α
⊢ b \ (b \ a) ⊔ a \ (b \ a) = a
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

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

Tactic:
exact (hb.2 hb.1).elim

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

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

Tactic:
covBy_iff_exists_insert

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shadow

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

Tactic:
rw [card_erase_of_mem hi, h𝒜 hA]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t

Tactic:
simp_rw [upShadow, mem_sup, mem_image, mem_compl]

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

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

Tactic:
covBy_iff_exists_insert

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
⊢ t \ (t \ s) ∈ 𝒜

Tactic:
sdiff_sdiff_eq_self hst

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
⊢ 𝒜.Nonempty

Tactic:
by_contra! rfl

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
hs : s ∉ ∅
h𝒜₁ : (insert s ∅).Nonempty
h𝒜₂ : univ ∉ insert s ∅
h𝒜₃ : (insert s ∅).Nontrivial
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < #∅ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #∅ + 1 = #(insert s ∅)
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons
ι : 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 * #(f' i) + 2 ^ Fintype.card α * 2 * #(s.biUnion f' ∩ (f' i)ᶜ) ≤
    2 ^ Fintype.card α * 2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
mul_assoc,

Goal state after:
case inr.cons
ι : 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 * #(f' i)) + 2 ^ Fintype.card α * 2 * #(s.biUnion f' ∩ (f' i)ᶜ) ≤
    2 ^ Fintype.card α * 2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))
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 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
mul_assoc,

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.KruskalKatona

Goal state before:
pp: case mpr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ s.erase (s.min' hs)

Tactic:
refine mem_erase_of_ne_of_mem (lt_of_le_of_lt ?_ lt).ne' ha

Goal state after:
case mpr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ s.min' hs ≤ k
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3
α : 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)
⊢ #((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) +
      #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) ≤
    #𝒜.shatterer

Tactic:
← hℬ,

Goal state after:
case refine_3
α : 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)
⊢ #((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) + #ℬ ≤ #𝒜.shatterer