mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  have h := fun n ↦ tprod_one_sub_pow_eq_powMulProdOneSubPow n hx hsum hlhs
  simp_rw [← sub_eq_iff_eq_add] at h
  refine (HasSum.tsum_eq ?_).symm
  rw [hrhs.hasSum_iff_tendsto_nat, (map_add_atTop_eq_nat 1).symm]
  apply tendsto_map'
  have h1 (k : ℕ) : pentagonal (k + 1) = ((k + 1) * (3 * k + 2) / 2) := by grind [pentagonal_def]
  have h2 (k : ℕ) : pentagonal (-k) = (k * (3 * k + 1) / 2) := by grind [pentagonal_neg]
  simp_rw [h1, h2, Function.comp_def, ← h]
  rw [← tendsto_sub_nhds_zero_iff]
  simpa [powMulProdOneSubPow] using htail.neg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
⊢ (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X

Tactic:
by
  simp only [deleteVerts, induce_isLink, mem_sdiff, and_congr_right_iff]
  exact fun h ↦ by simp [h.left_mem, h.right_mem]

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
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
⊢ (fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s))
      ((fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩)) n) =
    n

Tactic:
obtain hns | hsn := lt_or_ge n.1 #s
        · simp [hns]
        · simp [hsn.not_gt, hsn, mem_compl.1 <| Subtype.prop _]

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hts' : #t ≤ #s
⊢ False

Tactic:
exact hts <| ht.subset_of_card_le_card hs hts'

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

Goal state before:
pp: case right
σ : 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
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.toSyn (m.degree (m.reduce hb f)) = m.toSyn (m.degree f)
⊢ False

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq] at K

Goal state after:
case right
σ : 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
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ False
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:
by
  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.Nullstellensatz

Goal state before:
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 x hx
      simp only [MvPolynomial.eval_rename]
      apply Heval
      intro s
      simp only [Function.comp_apply]
      convert! hx (e.symm s)
      simp only [Equiv.apply_symm_apply]

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

Goal state before:
pp: case hE
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
x✝ : α
⊢ x✝ ∈ (M.disjointSum N h).E ↔ x✝ ∈ (N.disjointSum M ⋯).E

pp: case h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I✝ : Set α
a✝ : I✝ ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I✝ ↔ (N.disjointSum M ⋯).Indep I✝

Tactic:
· simp [union_comm]

Goal state after:
case h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I✝ : Set α
a✝ : I✝ ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I✝ ↔ (N.disjointSum M ⋯).Indep I✝
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x ↦ f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x ↦ f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False

Tactic:
rw [rhs_swap, distrib] at impos

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • ω.size • f ![a, b] < 2 • ω.size • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x ↦ f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False
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:
erw [Equiv.sigmaSumDistrib_apply, 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)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)
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:
erw [Equiv.sigmaSumDistrib_apply, 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)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
Module: Mathlib.Combinatorics.Quiver.Path.Weight

Goal state before:
pp: case cons
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
b✝ c✝ : V
a✝¹ : Path b b✝
a✝ : b✝ ⟶ c✝
ih : weight (fun {i j} ↦ w) (p.comp a✝¹) = weight (fun {i j} ↦ w) p * weight (fun {i j} ↦ w) a✝¹
⊢ weight (fun {i j} ↦ w) (p.comp (a✝¹.cons a✝)) = weight (fun {i j} ↦ w) p * weight (fun {i j} ↦ w) (a✝¹.cons a✝)

Tactic:
| cons _ _ 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 : 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:
erw [Equiv.sigmaSumDistrib_apply, 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)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)
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:
erw [Equiv.sigmaSumDistrib_apply, 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)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
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 hxe_ne

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
hxe_ne : v ≠ (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
⊢ 1 • x = x

Tactic:
ext
    exact one_smul M x.toVertex

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₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂

Tactic:
exact ⟨hφx, hφp⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm✝ : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1

Tactic:
simp only [Nat.mul_add_mod', Nat.mod_eq_of_lt hm, add_pos_iff, or_true, and_true, true_and,
      ← Nat.le_sub_iff_add_le hn, zero_lt_one]

Goal state after:
m : ℕ
hm✝ : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ y * m ≤ n - Nat.succ 0
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: 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 : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
⊢ #(Ioo 0 n) < n

Tactic:
by simp [Nat.card_Ioo, n]

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≤ a
⊢ a ≤ id b

Tactic:
exact (hs.eq hb ha hba).ge

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 ∈ lowerClosure ↑𝒜
hℬ : s ∈ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
rw [truncatedSup_union h𝒜 hℬ, truncatedSup_infs h𝒜 hℬ]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
hℬ : s ∈ lowerClosure ↑ℬ
⊢ #(𝒜.truncatedSup s ⊔ ℬ.truncatedSup s) + #(𝒜.truncatedSup s ⊓ ℬ.truncatedSup s) =
    #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ s ⊔ t
⊢ s = Iic a ∨ t = Iic a

Tactic:
exact this.imp (fun ha ↦ (le_sup_left.trans_eq hst).antisymm <| Iic_le.2 ha) fun ha ↦
    (le_sup_right.trans_eq hst).antisymm <| Iic_le.2 ha

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 α
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
⊢ Disjoint v ((b ⊔ u) \ v)

Tactic:
exact disjoint_sdiff_self_right

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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
hu : u = ⊥
⊢ Disjoint v ((compress u v b ⊔ u) \ v)

Tactic:
exact disjoint_sdiff_self_right

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized r ↑(𝓒 u v 𝒜)

Tactic:
by
  simp_rw [Set.Sized, mem_coe, mem_compression]
  rintro s (hs | ⟨huvt, t, ht, rfl⟩)
  · exact h𝒜 hs.1
  · rw [card_compress huv, h𝒜 ht]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
by
  rw [← isLowerSet_compl, ← coe_compl] at h𝒜
  have := h𝒜.le_card_inter_finset hℬ
  rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this

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

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ False

Tactic:
refine s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ (↑(insert a s)).Intersecting
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t

Tactic:
· rw [zero_add]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ image (fun t ↦ t) 𝒜 = univ ↔ 𝒜 = univ

Tactic:
image_id'

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

Goal state before:
pp: case pos
α : 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₁ s + f₁ (insert a s)) * (0 + f₂ (insert a t)) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [zero_add, add_mul]

Goal state after:
case pos
α : 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₁ s * f₂ (insert a t) + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r ↑𝒜
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r ↑ℬ
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
this : ℬ = 𝒞
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)

Tactic:
subst 𝒞

Goal state after:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r ↑𝒜
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r ↑ℬ
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
h𝒞𝒜 : #ℬ ≤ #𝒜
h𝒞 : IsInitSeg ℬ r
h𝒜𝒞 : #𝒜' = #ℬ
⊢ #(∂ ℬ) ≤ #(∂ 𝒜)
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✝¹ : Infinite α
inst✝ : Nonempty V
⊢ Infinite (G.Coloring α)

Tactic:
classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩

Goal state after:
case mp.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ (Walk.cons ⋯ ↑p.toPath).IsCycle

case mp.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)

Tactic:
{ replace ht : _ ∉ s := h.1.subset_compl_left ht; simp [hs, ht] }

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)

Tactic:
{ replace ht : _ ∉ s := h.1.subset_compl_left ht; simp [hs, ht] }

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph ≤ ⊤.induce {v_1 | v_1 ∈ p.support}

Tactic:
by
  convert! Subgraph.le_induce_top_verts
  exact p.verts_toSubgraph.symm

Goal state after: