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

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

Tactic:
← mul_smul_comm

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

Goal state before:
pp: case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ (↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head
      h =
    U

Tactic:
rw [head_cons]

Goal state after:
case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ s = U
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
⊢ ↑(p.take (p.firstReturn + 1) ⋯) ≠ []

Tactic:
take

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
⊢ ↑{ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ } ≠ []
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ ↑(((p + q).take (p.firstReturn + 1) ⋯).denest ⋯) = ↑((p.take (p.firstReturn + 1) ⋯).denest ⋯)

Tactic:
take

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ ↑({ toList := List.take (p.firstReturn + 1) ↑(p + q), count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯) =
    ↑({ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(#(restricted n p))) =
    PowerSeries.mk fun n ↦ ∑ p_1, (Multiset.toFinsupp p_1.parts).prod fun i c ↦ if p i then 1 else 0

Tactic:
restricted,

Goal state after:
case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(#{x | ∀ i ∈ x.parts, p i})) =
    PowerSeries.mk fun n ↦ ∑ p_1, (Multiset.toFinsupp p_1.parts).prod fun i c ↦ if p i then 1 else 0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k n : ℕ
x : R
⊢ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)) +
      x ^ (3 * k + 5) * (x ^ ((k + 1 + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + 1 + i + 1))) =
    x ^ ((k + 1) * (n + 1)) * (x ^ (2 * k + (n + 1) + 3) - 1) *
        ((∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))) * (1 - x ^ (k + n + 2))) -
      x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))

Tactic:
Finset.prod_range_succ',

Goal state after:
R : Type u_1
inst✝ : CommRing R
k n : ℕ
x : R
⊢ x ^ ((k + 1) * n) * ((∏ k_1 ∈ Finset.range n, (1 - x ^ (k + (k_1 + 1) + 1))) * (1 - x ^ (k + 0 + 1))) +
      x ^ (3 * k + 5) * (x ^ ((k + 1 + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + 1 + i + 1))) =
    x ^ ((k + 1) * (n + 1)) * (x ^ (2 * k + (n + 1) + 3) - 1) *
        ((∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))) * (1 - x ^ (k + n + 2))) -
      x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))
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 ↦ powMulProdOneSubPow 0 x_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x

Tactic:
powMulProdOneSubPow,

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 ^ ((0 + 1) * x_1) * ∏ i ∈ Finset.range (x_1 + 1), (1 - x ^ (0 + i + 1))
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingFirst n = (n + 1).choose 2

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingFirst 1 = n !

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingSecond 1 = 1

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingSecond n = (n + 1).choose 2

Tactic:
induction n with

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
⊢ ∏' (n : ℕ), (1 - X ^ (n + 1)) = pentagonalSeries R

Tactic:
nontriviality R
  rw [pentagonalSeries_eq_tsum_pow_pentagonal_sub]
  refine Pentagonal.tprod_one_sub_pow ?_ ?_ ?_ ?_ ?_
  · rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto]
    refine fun d ↦ tendsto_atTop_of_eventually_const fun i (hi : i ≥ d + 1) ↦ ?_
    grind
  · exact Pentagonal.summable_pow_mul_prod_one_sub_pow R
  · exact Pentagonal.multipliable_one_sub_X_pow R
  · exact (hasSum_pow_pentagonal_sub_pentagonalSeries R).summable
  · rw [tendsto_iff_coeff_tendsto]
    refine fun n ↦ tendsto_atTop_of_eventually_const fun k (hk : k ≥ n) ↦ ?_
    rw [map_zero]
    apply coeff_of_lt_order
    grw [← le_order_mul, ← le_order_mul]
    refine (lt_add_of_lt_of_nonneg (lt_add_of_nonneg_of_lt (by simp) ?_) (by simp))
    rw [order_X_pow, Nat.cast_lt, ← Nat.add_one_le_iff, Nat.le_div_iff_mul_le (by simp)]
    apply Nat.mul_le_mul <;> linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
⊢ e ∈ {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} ↔ ∃ x y, G.IsLink e x y ∧ H.IsLink e x y

Tactic:
simp only [edgeSet_eq_setOfPred_exists_isLink, mem_inter_iff, mem_ofPred_eq]
      exact ⟨fun ⟨⟨⟨x, y, hexy⟩, ⟨z, w, hezw⟩⟩, h⟩ ↦ ⟨x, y, hexy, by rwa [← h]⟩,
        fun ⟨x, y, hfG, hfH⟩ ↦ ⟨⟨⟨_, _, hfG⟩, ⟨_, _, hfH⟩⟩,
        fun z w ↦ by rw [hfG.isLink_iff_sym2_eq, hfH.isLink_iff_sym2_eq]⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ False

Tactic:
have := h ▸ he.edge_mem

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
this : e ∈ ∅
⊢ False
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
⊢ ∃ m ∈ s, m * m = m

Tactic:
have : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact

Goal state after:
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this✝ : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
this : CompactSpace M'
⊢ ∃ m ∈ s, m * m = m
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: ⊢ ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

Tactic:
intro κ

Goal state after:
κ : Type (max v u)
⊢ ∀ [Finite κ], ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D ≤r M

Tactic:
apply delete_isRestriction

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I D : Set α
⊢ M.Indep I ∧ I ⊆ M.E \ D ↔ M.Indep I ∧ Disjoint I D

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
I D : Set α
⊢ M.Indep I ∧ I ⊆ M.E ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I X ∧ X ⊆ M.E \ D ↔ M.IsBasis I X ∧ Disjoint X D

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I X ∧ X ⊆ M.E ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ l, IsMono C l
⊢ ∀ (C : (ι ⊕ ι' → Option α) → κ), (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
intro C

Goal state after:
case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ l, IsMono C l
C : (ι ⊕ ι' → Option α) → κ
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → (C ⊆ M.E \ D ↔ Disjoint C D)

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → (C ⊆ M.E ∧ Disjoint C D ↔ Disjoint C D)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
⊢ FP (Stream'.drop n a) ⊆ FP a

Tactic:
induction n with

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

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

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ M.E \ C ∧ Disjoint M.E D
⊢ M = M ／ C ＼ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ M✶.IsBasis ((M.E \ I) \ B) (M✶.E \ I) ∧ B ⊆ M.E \ I ↔ M.IsBase (B ∪ I) ∧ Disjoint B I

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ M✶.IsBasis ((M.E \ I) \ B) (M✶.E \ I) ∧ B ⊆ M.E ∧ Disjoint B I ↔ M.IsBase (B ∪ I) ∧ Disjoint B I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E \ I ↔ Disjoint J I ∧ ¬M.Indep (J ∪ I) ∧ J ∪ I ⊆ M.E

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint J I ↔ Disjoint J I ∧ ¬M.Indep (J ∪ I) ∧ J ∪ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
⊢ I ⊆ univ.sigma Bs

Tactic:
← univ_sigma_preimage_mk I

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' I) ⊆ univ.sigma Bs
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : Maximal (fun A ↦ (Disjoint A I ∧ M.Indep (A ∪ I)) ∧ A ⊆ X) J ∧ X ⊆ M.E \ I
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : Maximal (fun A ↦ (Disjoint A I ∧ M.Indep (A ∪ I)) ∧ A ⊆ X) J ∧ X ⊆ M.E ∧ Disjoint X I
⊢ M.IsBasis (J ∪ I) (X ∪ I)
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case h.refine_1
ι : 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
⊢ I ⊆ univ.sigma Js

Tactic:
← univ_sigma_preimage_mk I

Goal state after:
case h.refine_1
ι : 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
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' I) ⊆ univ.sigma Js
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J \ I ⊆ Y \ X

Tactic:
subset_sdiff,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J \ I ⊆ Y ∧ Disjoint (J \ I) X
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.E \ I

Tactic:
subset_sdiff,

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 ∧ Disjoint X I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
⊢ e ∈ M.closure C

Tactic:
← closure_inter_ground

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
⊢ e ∈ M.closure (C ∩ M.E)
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.E \ C ∧ X ⊆ M.E \ C ↔ (M.closure (X ∪ C) = M.E ∧ X ⊆ M.E ∧ C ⊆ M.E) ∧ Disjoint X C

Tactic:
subset_sdiff,

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 ∧ Disjoint X C ↔
    (M.closure (X ∪ C) = M.E ∧ X ⊆ M.E ∧ C ⊆ M.E) ∧ 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.E \ (C ∩ M.E)

Tactic:
subset_sdiff,

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 ∧ Disjoint K (C ∩ M.E)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∑ i_1 ∈ S, m.degree (X i - C i_1) = single i #S

pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∀ i_1 ∈ S, IsRegular (m.leadingCoeff (X i - C i_1))

Tactic:
· simp [Finset.sum_congr rfl (fun r _ ↦ m.degree_X_sub_C i r)]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∀ i_1 ∈ S, IsRegular (m.leadingCoeff (X i - C i_1))
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}
⊢ n ≤ #(sA.disjSum sB)

Tactic:
card_disjSum

Goal state after:
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}
⊢ n ≤ #sA + #sB
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ s \\ tᶜˢ = s ⊼ t

Tactic:
by
  rw [← infs_compls_eq_diffs, compls_compls]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r - k) ↑(∂^[k] 𝒜)

Tactic:
by
  simp_rw [Set.Sized, mem_coe, mem_shadow_iterate_iff_exists_sdiff]
  rintro t ⟨s, hs, hts, rfl⟩
  rw [card_sdiff_of_subset hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
⊢ Surjective ⇑supIrredLowerSet

Tactic:
aesop (add simp Surjective)

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
⊢ Surjective ⇑infIrredUpperSet

Tactic:
aesop (add simp Surjective)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #((a ⊔ u) \ v) = #a

Tactic:
rw [card_sdiff_of_subset (h.2.trans le_sup_left), sup_eq_union,
      card_union_of_disjoint h.1.symm, huv, add_tsub_cancel_right]

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

Goal state before:
pp: case ind.inr.succ.h𝒜₂
α : 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 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ image (fun x ↦ s ⊓ x) 𝒜

Tactic:
simpa using fun _ ↦ ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ IsUpperSet ↑s

Tactic:
by
  classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
    · exact mem_insert_self _ _
    rw [coe_insert]
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

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

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

Tactic:
tsub_eq_zero_of_le hs,

Goal state after:
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ 0
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
⊢ collapse 𝒜 a f t = f t + f (insert a t)

Tactic:
collapse_eq ha,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
⊢ ((if t ∈ 𝒜 then f t else 0) + if insert a t ∈ 𝒜 then f (insert a t) else 0) = f t + f (insert a t)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ collapse 𝒜 a f t

Tactic:
collapse_eq ha,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ (if t ∈ 𝒜 then f t else 0) + if insert a t ∈ 𝒜 then f (insert a t) else 0
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : 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 ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
collapse_eq ha,

Goal state after:
α : 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 ∈ 𝒜
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
have := hs.card_le
  rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le Nat.two_pos] at this
  revert hs
  refine s.strongDownwardInductionOn ?_ this
  rintro s ih _hcard hs
  by_cases! h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
  · exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩
  obtain ⟨t, ht, hst⟩ := h
  refine (ih ?_ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans
  rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_comm]
  exact ht.card_le

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

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

Tactic:
· simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
      exact Or.inl (mul_comm _ _)

Goal state after: