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)
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))
h1 : ∀ (k : ℕ), pentagonal (↑k + 1) = (k + 1) * (3 * k + 2) / 2
h2 : ∀ (k : ℕ), pentagonal (-↑k) = k * (3 * k + 1) / 2
⊢ Tendsto
    (fun x_1 ↦
      ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (x_1 + 1) * x ^ ((x_1 + 1) * (3 * x_1 + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow x_1 n x)
    atTop (𝓝 (∏' (n : ℕ), (1 - x ^ (n + 1))))

Tactic:
rw [← tendsto_sub_nhds_zero_iff]

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))
h1 : ∀ (k : ℕ), pentagonal (↑k + 1) = (k + 1) * (3 * k + 2) / 2
h2 : ∀ (k : ℕ), pentagonal (-↑k) = k * (3 * k + 1) / 2
⊢ Tendsto
    (fun x_1 ↦
      ∏' (n : ℕ), (1 - x ^ (n + 1)) -
          (-1) ^ (x_1 + 1) * x ^ ((x_1 + 1) * (3 * x_1 + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow x_1 n x -
        ∏' (n : ℕ), (1 - x ^ (n + 1)))
    atTop (𝓝 0)
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.Inc e x ↔ G.Inc e x
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.IsLoopAt e x ↔ G.IsLoopAt e x
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.IsNonloopAt e x ↔ G.IsNonloopAt e x
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
by
  refine ⟨fun hin ↦ ?_, fun hin ↦ ?_⟩
  on_goal 2 => rw [isLink_comm] at he
  all_goals rw [← hHG.isLink_congr hin] at he; exact he.right_mem

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ K * ↑(#(↑H).toFinset) + ex (↑H).toFinset ≤ K * ↑(#(↑H).toFinset) + (1 - ε / 2) * ↑(#((↑H).toFinset * S))

Tactic:
grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]

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

Goal state before:
pp: case map_rel_iff'
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
⊢ ∀ {a b : ↑V(ofSimpleGraph G)},
    G.Adj ((Equiv.Set.univ α) a) ((Equiv.Set.univ α) b) ↔ (ofSimpleGraph G).toSimpleGraph.Adj a b

Tactic:
refine ⟨fun h ↦ ⟨fun h' ↦ h.ne (congrArg Subtype.val h'), ?_⟩, fun ⟨_, h⟩ ↦ ?_⟩

Goal state after:
case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
h : G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
⊢ (ofSimpleGraph G).Adj ↑a✝ ↑b✝

case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
h : (ofSimpleGraph G).Adj ↑a✝ ↑b✝
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)

Tactic:
by rw [h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X ∩ (M.E ∩ Dᶜ)) ∧ Disjoint (X ∩ (M.E ∩ Dᶜ)) D ↔ M.IsBasis' I (X \ D)

Tactic:
inter_comm M.E,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X ∩ (Dᶜ ∩ M.E)) ∧ Disjoint (X ∩ (Dᶜ ∩ M.E)) D ↔ M.IsBasis' I (X \ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
inter_comm M.E,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X ∩ (Dᶜ ∩ M.E)) ∩ (Dᶜ ∩ M.E) = M.closure (X \ D) \ D
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop (1 + s.min' hs) a) (∏ x ∈ s.erase (s.min' hs), a.get x)

Tactic:
refine Set.mem_of_subset_of_mem ?_ (ih _ (s.min'_mem hs) h)

Goal state after:
case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
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
f : ↥(prefixed s)
⊢ (fun x ↦
        match x with
        | (g, g') =>
          ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
              invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
              left_inv := ⋯, right_inv := ⋯ },
            ⋯⟩)
      ((fun f ↦
          ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ },
            { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ }))
        f) =
    f

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
⊢ ↑(↑((fun x ↦
              match x with
              | (g, g') =>
                ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
                    invFun := fun n ↦
                      if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
                    left_inv := ⋯, right_inv := ⋯ },
                  ⋯⟩)
            ((fun f ↦
                ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
                    right_inv := ⋯ },
                  { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩,
                    left_inv := ⋯, right_inv := ⋯ }))
              f))
        x) =
    ↑(↑f x)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
⊢ (M✶ ＼ C).IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C

Tactic:
delete_isCircuit_iff

Goal state after:
α : Type u_1
M : Matroid α
K C : Set α
⊢ M✶.IsCircuit K ∧ Disjoint K C ↔ M.IsCocircuit K ∧ Disjoint K C
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
inst✝ : DecidableEq X
s : Finset X
⊢ (prefixed s).dens = (↑((Fintype.card X).choose #s))⁻¹

Tactic:
by
  simp [dens, card_prefixed, Nat.cast_choose _ s.card_le_univ]

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α}, (M ／ K).IsCircuit C → M.Indep K → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I ＼ (K \ I)).IsCircuit C
hI : M.IsBasis' I K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
delete_isCircuit_iff

Goal state after:
case inr
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α}, (M ／ K).IsCircuit C → M.Indep K → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
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
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
⊢ ψ.IsCovering

Tactic:
refine ⟨fun v => ?_, fun v => ?_⟩ <;> obtain ⟨u, rfl⟩ := φsur v

Goal state after:
case refine_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (ψ.star (φ.obj u))

case refine_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (ψ.costar (φ.obj u))
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
h : n ≤ p'.length
d : V
p₁ : Path a d
p₂ : Path d b✝
hp : p' = p₁.comp p₂
hl : p₁.length = n
⊢ p'.cons e = p₁.comp (p₂.cons e)

Tactic:
simp [hp]

Goal state after:
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
a b : M
x : SchreierGraph V ι
⊢ (a * b) • x = a • b • x

Tactic:
by
    ext
    exact mul_smul a b x.toVertex

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

Goal state before:
pp: case cons.cons
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₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₁, p₁.cons e₁⟩ =
      (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₂, p₂.cons e₂⟩ →
    ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
rename_i x₂

Goal state after:
case cons.cons
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₂
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₁, p₁.cons e₁⟩ =
      (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₂, p₂.cons e₂⟩ →
    ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
n : ℕ
⊢ schnirelmannDensity A * ↑n ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A}))

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ schnirelmannDensity A * ↑0 ≤ ↑(#({a ∈ Ioc 0 0 | a ∈ A}))

case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
n : ℕ
hn : n ≠ 0
⊢ schnirelmannDensity A * ↑n ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A}))
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case e_a
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A} = {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B}

Tactic:
ext x

Goal state after:
case e_a
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
x : ℕ
⊢ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A} ↔ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case h.inl
x : ℕ
a✝ : 0 < x
hm : x ≠ 1
hm' : x > 0
hxm : x ≤ x
h : x % x = 1
⊢ x = 1

Tactic:
simp at h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
refine mem_shadow_iff.2
        ⟨(t ⊔ u) \ v,
          sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, ?_, ?_⟩
      · rw [sup_eq_union, mem_sdiff, mem_union]
        exact ⟨Or.inl hat, hav⟩
      · simp [← erase_sdiff_comm, erase_union_distrib, erase_eq_of_notMem hau]

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

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

Tactic:
rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this

Goal state after:
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

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

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

Tactic:
· refine Or.inr ⟨k, mem_of_mem_erase ‹_›, fun hk ↦ hkt <| mem_of_mem_insert_of_ne hk hjk.ne',
      fun x hx ↦ ?_⟩
    simpa only [mem_insert, z hx, (hjk.trans hx).ne', mem_erase, Ne, false_or,
      and_iff_right_iff_imp] using fun _ ↦ ((min'_le _ _ <| mem_of_mem_erase hks).trans_lt hx).ne'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ #s = 0

Tactic:
exact h₁.1 hs

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False

Tactic:
by
    simp_rw [mem_shadow_iff, mem_falling] at h₁
    obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
    refine h𝒜 (slice_subset h₂) ht ?_ ((erase_subset _ _).trans hst)
    rintro rfl
    exact notMem_erase _ _ (hst ha)

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✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
hk : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
    ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))

Tactic:
by
  induction k with
  | zero =>
    simp only [cast_one, cast_le, sum_singleton, div_one, choose_self, range_one,
      zero_add, range_one, sum_singleton,
      choose_self, cast_one, div_one, cast_le, tsub_zero]
    exact card_le_card (slice_subset_falling _ _)
  | succ k ih =>
    rw [sum_range_succ, ← slice_union_shadow_falling_succ,
      card_union_of_disjoint (IsAntichain.disjoint_slice_shadow_falling h𝒜),
      cast_add, _root_.add_div, add_comm]
    rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
    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.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r : Setoid α
a w✝ : α
ha : a ∈ {x | r x w✝}
⊢ {x | r x w✝} = {x | r x a}

Tactic:
ext x

Goal state after:
α : Type u_1
r : Setoid α
a w✝ : α
ha : a ∈ {x | r x w✝}
x : α
⊢ x ∈ {x | r x w✝} ↔ x ∈ {x | r x a}
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
⊢ s = {x | (mkClasses c H) x y}

Tactic:
ext x

Goal state after:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s ↔ x ∈ {x | (mkClasses c H) x y}
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case succ
n n✝ : ℕ
ih : ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))}, Set.Sized r ↑𝒜 → #𝒞 ≤ #𝒜 → IsInitSeg 𝒞 r → #(∂^[n✝] 𝒞) ≤ #(∂^[n✝] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[n✝ + 1] 𝒞) ≤ #(∂^[n✝ + 1] 𝒜)

Tactic:
refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_

Goal state after:
case succ
n n✝ : ℕ
ih : ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))}, Set.Sized r ↑𝒜 → #𝒞 ≤ #𝒜 → IsInitSeg 𝒞 r → #(∂^[n✝] 𝒞) ≤ #(∂^[n✝] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ IsInitSeg (∂ 𝒞) (r - 1)
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
⊢ ⋃ i, s i = univ

Tactic:
ext x

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ x ∈ ⋃ i, s i ↔ x ∈ univ
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 β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
i : ι
x : α
hx : x ∈ s i
⊢ f i x = hs.piecewise f x

Tactic:
piecewise_apply,

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
i : ι
x : α
hx : x ∈ s i
⊢ f i x = f (hs.index x) x
Module: Mathlib.Data.Setoid.Partition

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

Tactic:
piecewise_apply,

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 : f (hs.index x) x ∈ t
⊢ x ∈ ⋃ i, s i ∩ f i ⁻¹' t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ Maximal (fun x ↦ (induce x G).Connected) C.supp

Tactic:
refine C.ind fun v ↦ ?_
  refine ⟨connected_toSimpleGraph _, fun s hconn hle u hu ↦ ConnectedComponent.sound ?_⟩
  exact hconn.preconnected ⟨u, hu⟩ ⟨v, hle rfl⟩ |>.map <| Embedding.induce s |>.toHom

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber = ↑n + 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

Tactic:
rw [eq_iff_le_not_lt, not_lt, ENat.add_one_le_iff (ENat.natCast_ne_top n), ← not_le,
    chromaticNumber_le_iff_colorable, ← Nat.cast_add_one, chromaticNumber_le_iff_colorable]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u_4
inst✝ : Infinite V
⊢ ⊤.chromaticNumber = ⊤

Tactic:
by_contra hc
  rw [← Ne, chromaticNumber_ne_top_iff_exists] at hc
  obtain ⟨n, ⟨hn⟩⟩ := hc
  exact not_injective_infinite_finite _ hn.injective_of_top_hom

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
⊢ G.CliqueFree n

Tactic:
have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
⊢ G.CliqueFree n
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf ((fun w ↦ ↑w.length) '' Walk.reverse '' Set.univ) = G.edist v u

Tactic:
← Set.image_comp,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf ((fun w ↦ ↑w.length) ∘ Walk.reverse '' Set.univ) = G.edist v u