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

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0

Tactic:
by
  have : NeZero p := inferInstance
  classical
  -- Let `N` be the number of common roots of our polynomials `f₁` and `f₂` (`f s ff` and `f s tt`).
  set N := Fintype.card {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0}
  -- Zero is a common root to `f₁` and `f₂`, so `N` is nonzero
  let zero_sol : {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0} :=
    ⟨0, by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]⟩
  have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
  have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
  -- Chevalley-Warning gives us that `p ∣ n` because the total degrees of `f₁` and `f₂` are at most
  -- `p - 1`, and we have `2 * p - 1 > 2 * (p - 1)` variables.
  have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
  -- Hence, `2 ≤ p ≤ N` and we can make a common root `x ≠ 0`.
  obtain ⟨x, hx⟩ := Fintype.exists_ne_of_one_lt_card ((Fact.out : p.Prime).one_lt.trans_le <|
    Nat.le_of_dvd hN₀ hpN) zero_sol
  -- This common root gives us the required subsequence, namely the `i ∈ s` such that `x i ≠ 0`.
  refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
  · simp +contextual [subset_iff]
  -- From `f₁ x = 0`, we get that `p` divides the number of `a` such that `x a ≠ 0`.
  · rw [card_map]
    refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_
    -- This number is nonzero because `x ≠ 0`.
    · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
      exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
    · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
    -- And it is at most `2 * p - 1`, so it must be `p`.
    · rw [univ_eq_attach, card_attach, hs]
      exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
  -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`.
  · simpa [f₂, ZMod.pow_card_sub_one, Finset.sum_filter] using x.2.2

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
by
    by_cases hat : a ∈ ofColex t
    · have ⟨b, hbu, hbt, hab⟩ := htu hat hau
      by_cases hbs : b ∈ ofColex s
      · have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu hbs hbt
        exact ⟨c, hcu, hcs, hab.trans hbc⟩
      · exact ⟨b, hbu, hbs, hab⟩
    · exact trans_aux hst htu has hat

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

Goal state before:
pp: case composite.succ.refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
this✝ : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
this : t₀ ∉ 𝒜
⊢ ∀ ⦃t : Finset ι⦄, t ∈ cons t₀ 𝒜 this → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
simp only [cons_eq_insert, mem_insert, forall_eq_or_imp, and_assoc]
      exact ⟨ht₀.trans sdiff_subset, ht₀card, ht₀sum, h𝒜⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (w✝¹ • ↑x✝³ ⬝ᵥ ↑x✝⁴ = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)

Tactic:
← h2,

Goal state after:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (w✝¹ • ↑x✝³ ⬝ᵥ w✝ • ↑x✝² = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ #(𝒜.sup' h𝒜₀ ⇑toColex) = r ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)

Tactic:
h𝒜.1 hs

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ r = r ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card P ≤ Fintype.card L

Tactic:
by_contra hc₂
  obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
  have :=
    calc
      ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
      _ ≤ ∑ l, lineCount L (f l) :=
        (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
      _ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
      _ < ∑ p, lineCount L p := by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
  exact lt_irrefl _ this

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : p ∉ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
l : L
x✝ : l ∈ univ
⊢ pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)

Tactic:
hf2

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : p ∉ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
l : L
x✝ : l ∈ univ
⊢ lineCount L (f l) • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
⊢ (A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)).Nonempty

Tactic:
by
      rw [← card_pos, ← Nat.cast_pos (α := ℚ)]
      have := card_inter_add_card_union (A ∩ (c * d) • A) (A ∩ (a * b)⁻¹ • A)
      rw [← Nat.cast_inj (R := ℚ), Nat.cast_add, Nat.cast_add] at this
      have : (#((A ∩ (c * d) • A) ∪ (A ∩ (a * b)⁻¹ • A)) : ℚ) ≤ #A := by
        rw [Nat.cast_le, ← inter_union_distrib_left]
        exact card_le_card inter_subset_left
      linarith

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ Projectivization.mk K a ha = Projectivization.mk K b hb ∨ Projectivization.mk K c hc = Projectivization.mk K d hd

Tactic:
rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]

Goal state after:
case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m : Multiset ℕ
this :
  (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]
        nth_rewrite 3 [← Finset.erase_eq_of_notMem hm]
        exact this

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

Goal state before:
pp: case e_a.a
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ! ^ count x m * (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) = (x * count x m)!

Tactic:
bell_mul_eq_lemma

Goal state after:
case e_a.a
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ (x * count x m)! = (x * count x m)!

case e_a.a.hx
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ≠ 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
k : ℕ
⊢ count D (List.take k (List.take i ↑p)) ≤ count U (List.take k (List.take i ↑p))

Tactic:
take_take

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
k : ℕ
⊢ count D (List.take (min k i) ↑p) ≤ count U (List.take (min k i) ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (1 + i) (List.take ((↑p).length - 1) ↑p))) ≤
    count U (List.drop 1 (List.take (1 + i) (List.take ((↑p).length - 1) ↑p)))

Tactic:
take_take

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p)) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i : ℕ
⊢ Filter.Tendsto (fun j ↦ (f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))).order) Filter.atTop (nhds ⊤)

Tactic:
by
  refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)
  intro m hm
  grw [PowerSeries.smul_eq_C_mul, ← le_order_mul]
  refine lt_add_of_nonneg_of_lt (by simp) ?_
  nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧)
  rw [order_X_pow]
  norm_cast
  grind

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

Goal state before:
pp: ⊢ insidePart 0 = 0

Tactic:
simp [insidePart]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≤ x, f y
x : α
⊢ f x = ∑ y ≤ x, (mu 𝕜) y x * g y

Tactic:
convert! moebius_inversion_top (α := αᵒᵈ) f g h x using 3
  rw [← mu_toDual]; rfl

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
⊢ Fintype.card α * addRothNumber univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Tactic:
by
  obtain ⟨s, -, hscard, hs⟩ := addRothNumber_spec (univ : Finset α)
  have := noAccidental hs
  rw [← hscard, ← card_triangleIndices, ← card_triangles]
  exact (locallyLinear hs).le_ruzsaSzemerediNumber

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
let α := Fin (2 * n + 1)
  have : Nat.Coprime 2 (2 * n + 1) := by simp
  have : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa
    using! (ZMod.unitOfCoprime 2 this).isUnit⟩
  open scoped Fin.CommRing in
  calc
    (2 * n + 1) * rothNumberNat n
    _ = Fintype.card α * addRothNumber (Iio (⟨n, by lia⟩ : α)) := by
      rw [Fin.addRothNumber_eq_rothNumberNat (by simp), Fintype.card_fin]
    _ ≤ Fintype.card α * addRothNumber (univ : Finset α) := by
      gcongr; exact subset_univ _
    _ ≤ ruzsaSzemerediNumber (Sum α (Sum α α)) := addRothNumber_le_ruzsaSzemerediNumber _
    _ = ruzsaSzemerediNumberNat (6 * n + 3) := by
      simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
      ring_nf

Goal state after:
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.IsNonloopAt e x ↔ G.IsNonloopAt e x

Tactic:
simp_rw [Graph.IsNonloopAt, hHG.isLink_iff he]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ ¬H ≤i G ↔ ∃ e x y, G.IsLink e x y ∧ x ∈ V(H) ∧ y ∈ V(H) ∧ e ∉ E(H)

Tactic:
contrapose!

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ H ≤i G ↔ ∀ (e : β) (x y : α), G.IsLink e x y → x ∈ V(H) → y ∈ V(H) → e ∈ E(H)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ ¬H ≤c G ↔ ∃ x y, G.Adj x y ∧ x ∈ V(H) ∧ y ∉ V(H)

Tactic:
contrapose!

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ H ≤c G ↔ ∀ (x y : α), G.Adj x y → x ∈ V(H) → y ∈ V(H)
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
z w : α
hzw : G.IsLink e z w
⊢ f x = f z ∨ f x = f w

Tactic:
obtain rfl | rfl := hxy.left_eq_or_eq hzw <;> simp

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

Goal state before:
pp: α : Type u_1
e : Set α
H : Hypergraph α
h : H.IsComplete
⊢ e ∈ E(H) ↔ e ⊆ V(H)

Tactic:
grind [IsComplete, subset_vertexSet_of_mem_edgeSet]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.tail'
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
b : Stream' M
n : M
h : FP b.tail n
ih : ∀ (p : { s // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → n ∈ ↑p

Tactic:
| tail' b n h ih =>

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

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

Tactic:
by
  rw [← dual_delete_dual, ← dual_ground, delete_inter_ground_eq, dual_delete_dual]

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✶.Coindep I

Tactic:
dual_coindep_iff

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ M.Indep I
Module: Mathlib.Combinatorics.Nullstellensatz

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

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

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

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

Tactic:
rw [isNonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]
  refine ⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
    fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩
  rw [← closure_inter_ground]
  exact (M.subset_closure (C ∩ M.E)) ⟨heC, h.1⟩

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

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

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis C

Goal state after:
α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_option.Hdeg
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
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 (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := ⋯
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
⊢ ∀ (i : σ), degreeOf i (Q.coeff m) < #(S (Option.some i))

Tactic:
intro i
      apply lt_of_le_of_lt _ (Hdeg (some i))
      simp only [degreeOf_eq_sup, Finset.sup_le_iff, mem_support_iff, ne_eq]
      intro e he
      set n := (embDomain Function.Embedding.some e).update none m with hn
      rw [eq_option_embedding_update_none_iff] at hn
      rw [hQ, ← hn.1, ← hn.2, optionEquivLeft_coeff_some_coeff_none, ← ne_eq,
        ← MvPolynomial.mem_support_iff] at he
      convert! Finset.le_sup he
      rw [← hn.2, some_apply]

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

Goal state before:
pp: case pos
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)

pp: case neg
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : ¬c ∈ S
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)

Tactic:
· have p'_len : p'.length = n := by simp_all
      obtain ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂, hp'⟩ :=
        ih p' S ha_not_in_S hc_in_S p'_len
      refine ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩
      simp [hp', comp_toPath_eq_cons]

Goal state after:
case neg
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : ¬c ∈ S
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
i : σ
⊢ (S i).Nonempty

Tactic:
rw [← Finset.card_pos]; exact Nat.zero_lt_of_lt (htS i)

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ #({a ∈ Ioc 0 k | a ∈ A}) ≤ k - 1

Tactic:
suffices {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)

Goal state after:
case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ s, ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
rw [← powerset_univ, powerset_card_disjiUnion, sum_disjiUnion]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ (↑m)⁻¹ ≤ ↑(#({x ∈ Ioc 0 n | x % m = 1})) / ↑n

Tactic:
have : (Icc 0 ((n - 1) / m)).image (· * m + 1) ⊆ {x ∈ Ioc 0 n | x % m = 1} := by
    simp only [subset_iff, mem_image, forall_exists_index, mem_filter, mem_Ioc, mem_Icc, and_imp]
    rintro _ y _ hy' rfl
    have hm : 2 ≤ m := hm.lt_of_le' hm'
    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]
    exact Nat.mul_le_of_le_div _ _ _ hy'

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}
⊢ (↑m)⁻¹ ≤ ↑(#({x ∈ Ioc 0 n | x % m = 1})) / ↑n
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
⊢ Set.Sized r ↑(∂ 𝒜) ↔ Set.Sized (r + 1) ↑𝒜

Tactic:
by
  refine ⟨fun h𝒜 s hs => ?_, Set.Sized.shadow⟩
  obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)
  rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]

Goal state after: