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

Goal state before:
pp: ⊢ (ofTree BinaryTree.nil).toTree = BinaryTree.nil

Tactic:
simp [ofTree, toTree]

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

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ p.toTree.numNodes = p.semilength

Tactic:
rw [toTree]
    simp_rw [h, ite_false, numNodes]
    rw [← semilength_insidePart_add_semilength_outsidePart_add_one h,
      numNodes_toTree p.insidePart, numNodes_toTree p.outsidePart]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x

Tactic:
have hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1)) := by
    apply Summable.comp_nat_add (k := 1)
    conv in fun k ↦ _ =>
      ext k
      rw [pow_add, pow_add, mul_assoc (x ^ k), mul_comm (x ^ k), mul_assoc (x ^ 1 * x ^ 1)]
    exact hsum.mul_left _

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

Goal state before:
pp: case zero
n : ℕ
x✝ : n + 2 ≠ 0
hk : 0 ∈ Iic (n + 1)
⊢ Even (largeSchroder 0 * (n + 1 - 0).largeSchroder)

pp: case succ
n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)

Tactic:
· simpa using even_largeSchroder n.succ_ne_zero

Goal state after:
case succ
n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)
Module: Mathlib.Combinatorics.Enumerative.Stirling

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

Tactic:
by
  induction n <;> simp only [*, stirlingSecond, stirlingSecond_eq_zero_of_lt (lt_succ_self _),
    mul_zero]

Goal state after:
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)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
⊢ HasSum (fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))) (∏' (n : ℕ), (1 - x ^ (n + 1)))

Tactic:
rw [hrhs.hasSum_iff_tendsto_nat, (map_add_atTop_eq_nat 1).symm]

Goal state after:
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)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * (x ^ pentagonal (-↑i) - x ^ pentagonal (↑i + 1)))
    (map (fun a ↦ a + 1) atTop) (𝓝 (∏' (n : ℕ), (1 - x ^ (n + 1))))
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.Inc e x ↔ G.Inc e x

Tactic:
by
  simp_rw [Graph.Inc, hHG.isLink_iff he]

Goal state after:
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' * m = m}

Tactic:
Set.mem_ofPred_eq,

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: case refine_4
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 : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ U * V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
case refine_4
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 : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ ∀ᶠ (m : M) in ↑(U * V), m ∈ FP (Stream'.drop n a)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ＼ D).Dep X ↔ M.Dep X ∧ Disjoint X D

Tactic:
rw [dep_iff, dep_iff, delete_indep_iff, delete_ground, subset_sdiff]; tauto

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

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

Tactic:
rw [← dual_delete_dual, dual_isBase_iff', delete_ground, dual_ground, delete_isBase_iff,
    subset_sdiff, ← and_assoc, and_congr_left_iff, ← dual_dual M, dual_isBase_iff', dual_dual,
    dual_dual, union_comm, dual_ground, union_subset_iff, and_iff_right hI.subset_ground,
    and_congr_left_iff, ← isBase_restrict_iff, sdiff_sdiff, Spanning.isBase_restrict_iff,
    and_iff_left (sdiff_subset_sdiff_right subset_union_left)]

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

α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ M✶.Spanning (M.E \ I)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
and_iff_right disjoint_sdiff_left,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ M.Indep (I ∪ J) ↔ M.Indep (J \ I ∪ I)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
⊢ ∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c

Tactic:
classical
  obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ
  specialize hι fun v => C <| ∑ i, v i
  obtain ⟨l, c, hl⟩ := hι
  set s : Finset ι := {i | l.idxFun i = none} with hs
  refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩
  · rw [hs, Finset.mem_filter]
    exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩
  · exact fun m => m
  intro x xs
  rw [← hl ⟨x, xs⟩]
  clear hl; congr
  rw [← Finset.sum_add_sum_compl s]
  congr 1
  · rw [← Finset.sum_const]
    apply Finset.sum_congr rfl
    intro i hi
    rw [hs, Finset.mem_filter] at hi
    rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
  · apply Finset.sum_congr rfl
    intro i hi
    rw [hs, Finset.compl_filter, Finset.mem_filter] at hi
    obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
    simp [← hy, Option.map_some, Option.getD]

Goal state after:
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:
rw [delete_contract_eq_sdiff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
⊢ ∃ h,
    (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
      f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h

Tactic:
use h

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := ⋯
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
⊢ (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
    f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case nil
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₁ : U
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ →
      ⟨u, Path.nil⟩ = a₂

Tactic:
rintro ⟨y₂, p₂⟩
    rcases p₂ with - | ⟨p₂, e₂⟩
    · intro; rfl -- Porting note: goal not present in lean3.
    · intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      exfalso
      obtain ⟨h, h'⟩ := h
      rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'
      exact (Path.nil_ne_cons _ _) h'

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

Goal state before:
pp: case cons.inl
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
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_in_prefix : v ∈ pPrev.vertices
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
by_cases h_eq_end : v = (pPrev.cons e).end
      · exact h_case₁ h_eq_end
      · exact h_case₂ h_in_prefix h_eq_end

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜

Tactic:
conv_rhs => rw [← card_filter_add_card_filter_not (fun s => (a ∈ s))]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
hs : a ∉ s
t : Finset α
ht : t ∈ 𝒜
hts : insert a t = insert a s
⊢ s ∈ 𝒜

Tactic:
rwa [← insert_erase_invOn.2.injOn (h𝒜 _ ht) hs hts]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ¬{0}ᶜ ⊆ A → ¬1 ≤ schnirelmannDensity A

Tactic:
not_le

Goal state after:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1
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
⊢ ↑n ≤ ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A}))

Tactic:
Nat.cast_le,

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

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n ≤ ↑(((n - 1) / m + 1) * m)

pp: case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1

Tactic:
Nat.cast_le,

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ n ≤ ((n - 1) / m + 1) * m

case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (s ⊼ t).truncatedSup a = s.truncatedSup a ⊓ t.truncatedSup a

Tactic:
simp only [truncatedSup_of_mem, hs, ht, infs_aux.2 ⟨hs, ht⟩, sup'_inf_sup', filter_infs_le]
  simp_rw [← image_inf_product]
  rw [sup'_image]
  simp [Function.uncurry_def]

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

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

Tactic:
simp_rw [mem_upShadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]
  aesop

Goal state after:
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
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.memberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) +
      (#(Finset.nonMemberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (#s + 1) * #(𝒜 ∩ ℬ)

Tactic:
add_comm (_ * _),

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
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) +
        #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      (#(Finset.nonMemberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (#s + 1) * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ #(s.erase a) = k

Tactic:
rw [card_erase_of_mem ha, hs]

Goal state after:
case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

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

Tactic:
rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]

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

Goal state before:
pp: case mpr.tail
V : Type u
G : SimpleGraph V
u v b✝ c✝ : V
a✝ : Relation.ReflTransGen G.Adj u b✝
ha : G.Adj b✝ c✝
hr : G.Reachable u b✝
⊢ G.Reachable u c✝

Tactic:
| tail _ ha hr =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
u v : V
⊢ G.Reachable u v

Tactic:
by
  rw [Subsingleton.allEq u v]

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

Goal state before:
pp: 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𝒜𝒞 : #𝒜' = #ℬ
⊢ #(∂ ℬ) ≤ #(∂ 𝒜)

Tactic:
exact hℬ𝒜.trans (by gcongr)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
⊢ Gᶜ.Reachable u w

Tactic:
by_cases huw : G.Reachable u w

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
⊢ Gᶜ.Reachable u w

case neg
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : ¬G.Reachable u w
⊢ Gᶜ.Reachable u w
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 ↑𝒞
⊢ #(powersetCard (r - i) range'k) = #(∂^[i] 𝒞)

Tactic:
congr!

Goal state after:
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 ↑𝒞
⊢ powersetCard (r - i) range'k = ∂^[i] 𝒞
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
⊢ hs.piecewise f ⁻¹' t = ⋃ i, s i ∩ f i ⁻¹' t

Tactic:
refine ext fun x => ⟨fun hx => ?_, fun ⟨a, ⟨i, hi⟩, ha⟩ => ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ hs.piecewise f ⁻¹' t
⊢ x ∈ ⋃ i, s i ∩ f i ⁻¹' t

case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
x✝ : x ∈ ⋃ i, s i ∩ f i ⁻¹' t
a : Set α
i : ι
hi : (fun i ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ a
⊢ x ∈ hs.piecewise f ⁻¹' t
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✝¹ : Nontrivial α
inst✝ : Nonempty V
⊢ Nontrivial (G.Coloring α)

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

Goal state after:
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
w : V
⊢ G.Adj v w ↔ w ∈ {w | w ∈ t ∧ G.Adj v w}

Tactic:
Set.mem_ofPred_eq,

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 : V
⊢ G.Adj v w ↔ w ∈ t ∧ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ G.Adj v w ↔ v ∈ {v | v ∈ s ∧ G.Adj v w}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ G.Adj v w ↔ v ∈ s ∧ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
p : G.Walk u v
⊢ (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph

Tactic:
induction p <;> simp [*, Subgraph.map_sup]

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V ⊕ V
he : s(v, w) ∈ G.bipartiteDoubleCover.edgeFinset
⊢ ∃ a,
    ∃ (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
      (match a, ha with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        s(v, w)

Tactic:
mem_edgeFinset,

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V ⊕ V
he : s(v, w) ∈ G.bipartiteDoubleCover.edgeSet
⊢ ∃ a,
    ∃ (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
      (match a, ha with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        s(v, w)