mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ X ⊆ (M ／ I).E

Tactic:
contract_ground,

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ (X \ I ∩ (M ／ I).E) = M ／ I ＼ ((X ∩ M.E) \ I)

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ (X \ I ∩ (M.E \ I)) = M ／ I ＼ ((X ∩ M.E) \ I)
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)
⊢ (M ／ C).IsBasis (I \ C) (X \ C ∩ (M ／ C).E)

Tactic:
contract_ground,

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)
⊢ (M ／ C).IsBasis (I \ C) (X \ C ∩ (M.E \ C))
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case of_equiv.Hdeg
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
⊢ ∀ (i : σ), degreeOf i ((rename ⇑e.symm) P) < #(S (e i))

pp: case of_equiv.Heval
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
⊢ ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (e i)) → (eval x) ((rename ⇑e.symm) P) = 0

Tactic:
· intro i
      convert! Hdeg (e i)
      conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]

Goal state after:
case of_equiv.Heval
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
⊢ ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (e i)) → (eval x) ((rename ⇑e.symm) P) = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M ／ C).E \ (M ／ C).loops ↔ e ∈ M.E \ M.closure C

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M.E \ C) \ (M ／ C).loops ↔ e ∈ M.E \ M.closure C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ M.closure (X ∪ C) \ C = (M ／ C).E ∧ X ⊆ (M ／ C).E ↔ M.Spanning (X ∪ C) ∧ Disjoint X C

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ M.closure (X ∪ C) \ C = M.E \ C ∧ X ⊆ M.E \ C ↔ M.Spanning (X ∪ C) ∧ Disjoint X C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I) ∧ K ⊆ (M ／ (C ∩ M.E)).E

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I) ∧ K ⊆ M.E \ (C ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
⊢ D ∩ (M.E \ C) = D \ C ∩ (M.E \ C)
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 ／ C).E \ D = (M ↾ M.E \ D) ／ C

Tactic:
contract_ground,

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 \ C) \ D = (M ↾ M.E \ D) ／ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' : Set α
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C' \ D) ＼ D

Tactic:
by
  rw [delete_contract_eq_sdiff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]

Goal state after:
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₂)
⊢ ∃ p, 0 < p.length

Tactic:
have hp_pos : 0 < p.length := by
    simpa [p, Path.length_comp, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
      Nat.succ_pos (p₁.length + p₂.length)

Goal state after:
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
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
h2 : ∀ c ∈ r.support, ∀ b_1 ∈ {b}, ¬m.degree b_1 ≤ c
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (↑⟨b, ⋯⟩ * q)) ≤ m.toSyn (m.degree f)
⊢ ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c

Tactic:
simp only [Set.mem_singleton_iff, forall_eq] at h2

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (↑⟨b, ⋯⟩ * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c
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 b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
intro hxPrev

Goal state after:
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hxPrev : v ∈ pPrev.vertices
⊢ v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
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
⊢ ∀ x ∈ Ioc 0 ↑⟨n, hn⟩, x ∈ A

Tactic:
rintro x hx

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 : ℕ
hx : x ∈ Ioc 0 ↑⟨n, hn⟩
⊢ x ∈ A
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⋯
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

Tactic:
rw [div_lt_iff₀ (Nat.cast_pos.2 hn), ← div_lt_iff₀' hε, Nat.cast_add_one]

Goal state after:
case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ε < ↑⌊↑(#A) / ε⌋₊ + 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : A.Finite
⊢ schnirelmannDensity A = 0

Tactic:
simpa using schnirelmannDensity_finset hA.toFinset

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ a ⊔ (u ⊔ u) = a ⊔ u

Tactic:
sup_idem

Goal state after:
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ a ⊔ u = a ⊔ u
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

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

Tactic:
rw [coe_sups, upperClosure_sups, UpperSet.mem_sup_iff]

Goal state after:
Module: Mathlib.Order.Birkhoff

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

Tactic:
obtain ⟨s, rfl, hs⟩ := exists_supIrred_decomposition a

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ s.sup id ≤ (fun s ↦ (↑s).toFinset.sup Subtype.val) ((fun a ↦ { carrier := {b | ↑b ≤ a}, lower' := ⋯ }) (s.sup id))
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ⊆ s
⊢ s ∈ Finset.memberSubfamily a 𝒜 → t ∈ Finset.memberSubfamily a 𝒜

Tactic:
mem_memberSubfamily

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ⊆ s
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #𝒜 * #ℬ ≤ 2 ^ #(insert a s) * #(𝒜 ∩ ℬ)

Tactic:
card_insert_of_notMem hs,

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #𝒜 * #ℬ ≤ 2 ^ (#s + 1) * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ Finset.memberSubfamily a 𝒞
⊢ t ⊆ s

Tactic:
mem_memberSubfamily

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : insert a t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s
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)
⊢ #((insert i s).biUnion f') ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi))

Tactic:
rw [biUnion_insert]

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)
⊢ #(f' i ∪ s.biUnion f') ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_1
α : 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 : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : u ∈ memberSubfamily a 𝒜
ht : s ∩ u ⊆ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
mem_memberSubfamily

Goal state after:
case refine_3.refine_1
α : 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 : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_1
α : 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 : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : v ∈ memberSubfamily a 𝒜
hsv : s ∩ v = {a}
⊢ False

Tactic:
mem_memberSubfamily

Goal state after:
case refine_3.refine_1
α : 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 : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ a ∉ v
hsv : s ∩ v = {a}
⊢ False
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) ≤
    ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ↑(#(∂ (falling (Fintype.card α - k) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1))

Tactic:
grw [ih <| le_of_succ_le hk, local_lubell_yamamoto_meshalkin_inequality_div
      (tsub_pos_iff_lt.2 <| Nat.succ_le_iff.1 hk).ne' <| sized_falling _ _]

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) ↑𝒜
⊢ ∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r))⁻¹ =
    ∑ r ∈ range (Fintype.card α + 1), ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose r)

Tactic:
by
      simp [slice, div_eq_mul_inv]

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 : u ∈ memberSubfamily a 𝒜
hsu : s ∩ u = t.erase a
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
mem_memberSubfamily

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
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ s ∩ insert a u = s ∩ u

Tactic:
inter_insert_of_notMem ha

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ s ∩ u = s ∩ u
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

Tactic:
cases p with

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

Goal state before:
pp: α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
⊢ ∀ (y₁ y₂ : Set α), y₁ ∈ s ∧ a ∈ y₁ → y₂ ∈ s ∧ a ∈ y₂ → y₁ = y₂

Tactic:
intro b₁ b₂ hb₁ hb₂

Goal state after:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ b₁ = b₂
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
h : ¬∃ v, ∀ (w : V), G.Reachable v w
u : V
⊢ ∀ (v : V), Gᶜ.Reachable u v

Tactic:
v

Goal state after:
V : Type u
G : SimpleGraph V
h : ¬∃ v, ∀ (w : V), G.Reachable v w
u v : V
⊢ Gᶜ.Reachable u v
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 ↑𝒞
⊢ k.choose (r - i) = #(powersetCard (r - i) range'k)

Tactic:
rw [card_powersetCard, card_attachFin, card_range]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : univ.PairwiseDisjoint fun i ↦ f i '' s i
x y : α
h : hs.piecewise f x = hs.piecewise f y
this : hs.index x = hs.index y
⊢ x = y

Tactic:
apply h_injOn (hs.index x) (hs.mem_index x) (this ▸ hs.mem_index y)
    simpa only [piecewise_apply, this] using h

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

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

Tactic:
cases p with

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

Goal state before:
pp: n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝¹ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
⊢ (n - 1).choose (n - r) < #𝒜

Tactic:
choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm

Goal state after:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝¹ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
⊢ (n - 1).choose (r - 1) < #𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ G.neighborSet v ⊆ t

Tactic:
isBipartiteWith_neighborSet h hv

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ {w | w ∈ t ∧ G.Adj v w} ⊆ t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (⊤.induce {u, v}).Connected

Tactic:
by
  rw [← subgraphOfAdj_eq_induce huv]
  exact subgraphOfAdj_connected huv

Goal state after: