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

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ ∃ a b c, ¬a = b ∧ ¬a = c ∧ ¬b = c

Tactic:
Subtype.ext_iff

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ ∃ a b c, ¬↑a = ↑b ∧ ¬↑a = ↑c ∧ ¬↑b = ↑c
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ order P L + Fintype.card { x // x = ⟨p, ⋯⟩ } = order P L + Fintype.card { x // ↑x = p }

Tactic:
Subtype.ext_iff

Goal state after:
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)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ ∑ i ∈ A⁻¹ * A, 1 / 2 * ↑(#A) = 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A))

Tactic:
simp only [sum_const, nsmul_eq_mul, mul_comm]

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

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

Tactic:
smul_finset_subset_mul (by simpa)

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

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
⊢ (↑p).head h = U

Tactic:
rcases p with - | s; · tauto
  rw [head_cons]
  by_contra f
  rename_i _ nonneg
  simpa [s.dichotomy.resolve_left f] using nonneg 1

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : ↑(#(∅⁻¹ * ∅)) ≤ K * ↑(#∅)
hA₂ : ↑(#(∅ * ∅⁻¹)) ≤ K * ↑(#∅)
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑∅ * ↑∅⁻¹

pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

Tactic:
· exact ⟨⊥, inferInstance, ∅, by simp; positivity⟩

Goal state after:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)

Tactic:
· rw [← mul_assoc, ← uniformBell_mul_eq _ hn]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a : α
⊢ (mu 𝕜) a a = 1

Tactic:
by simp [mu_apply]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
⊢ zeta 𝕜 * mu' 𝕜 = 1

Tactic:
by
  ext a b
  calc
    _ = ∑ x ∈ Icc a b, mu' 𝕜 x b := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).1]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu'_left ..

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
x : ℕ
⊢ x ∣ g x

Tactic:
by_cases hx : x ∈ s
  · specialize hprod x hx
    contrapose hprod
    have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx)
    rw [map_add, (summable_genFun_term' f hx0).map_tsum _ (WithPiTopology.continuous_coeff _ _)]
    rw [show (0 : R) = 0 + ∑' (i : ℕ), 0 by simp]
    congrm (?_ + ∑' (i : ℕ), ?_)
    · suffices g x ≠ 0 by simp [this]
      contrapose hprod
      simp [hprod]
    · rw [map_smul, coeff_X_pow]
      apply smul_eq_zero_of_right
      suffices g x ≠ x * (i + 1) by simp [this]
      contrapose hprod
      simp [hprod]
  · suffices g x = 0 by simp [this]
    contrapose! hx
    exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 <| by simpa using hx

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

Goal state before:
pp: p q : DyckWord
⊢ q ≤ p + q

Tactic:
by
  by_cases h : p = 0
  · simp [h]
  · have := semilength_outsidePart_lt h
    exact (le_add_self p.outsidePart q).trans
      (Relation.ReflTransGen.single (Or.inr (outsidePart_add h).symm))

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

Goal state before:
pp: case inl
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1
⊢ f x.1 y.1 * g x.2 y.2 = 0

Tactic:
simp [apply_eq_zero_of_not_le hxy]

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

Goal state before:
pp: case inr
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.2 ≤ y.2
⊢ f x.1 y.1 * g x.2 y.2 = 0

Tactic:
simp [apply_eq_zero_of_not_le hxy]

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

Goal state before:
pp: k : ℤ
⊢ 2 * ↑(pentagonal k) = k * (3 * k - 1)

Tactic:
rw [natCast_pentagonal]
  exact Int.two_mul_ediv_two_of_even (by grind)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)

Tactic:
simp only [Inc, banana_isLink, exists_and_left, and_congr_right_iff]
  aesop

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
⊢ Sum.inl a = m.idxFun i

Tactic:
obtain ⟨b, hba⟩ := exists_ne a
    cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.cons'
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 → b.head * n ∈ ↑p

Tactic:
rintro p rfl
    have := Set.inter_subset_right (ih (succ p) ?_)
    · simpa only using! this
    rw [Stream'.corec_eq, Stream'.tail_cons]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_1
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
p : AlmostMono C'
x : α
⊢ C (↑(p.line.prod (map some l')) (some x)) = p.color

Tactic:
rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_2
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
x : α
⊢ C (↑(vertical s.focus (map some l')) (some x)) = C' s.focus

Tactic:
rw [vertical_apply, ← congr_fun (hl' x), Line.map_apply]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
⊢ x ∈ S → C (#s • x + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0) = c

Tactic:
xs

Goal state after:
case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ C (#s • x + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0) = c
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case h.refine_2
ι : 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 Js ⊆ X

Tactic:
rw [← univ_sigma_preimage_mk X]
      exact sigma_mono rfl.subset fun i ↦ (hJs i).1.subset

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
use g' +
      Finsupp.single i (monomial (m.degree f - m.degree (b i)) ((hb i).unit⁻¹ * m.leadingCoeff f))

Goal state after:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∃ r,
    f =
        (Finsupp.linearCombination (MvPolynomial σ R) b)
            (g' + Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) +
          r ∧
      (∀ (i_1 : ι),
          m.toSyn
              (m.degree
                (b i_1 *
                  (g' + Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f)))
                    i_1)) ≤
            m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
inter_assoc

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
⊢ D ∩ (M.E ∩ Cᶜ) = D ∩ (M.E ∩ Cᶜ)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
inter_assoc

Goal state after:
α : Type u_1
M : Matroid α
D C : Set α
⊢ C ∩ (M.E ∩ Dᶜ) = C ∩ (M.E ∩ Dᶜ)
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
u : U
⊢ φ.symmetrify.costar u = ⇑(symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)

Tactic:
rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyCostar (φ.obj u))]

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u = Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case nil.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₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
h : φ.obj u = φ.obj y₂ ∧ φ.mapPath Path.nil ≍ (φ.mapPath p₂).cons (φ.map e₂)
⊢ ⟨u, Path.nil⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
exfalso

Goal state after:
case nil.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₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
h : φ.obj u = φ.obj y₂ ∧ φ.mapPath Path.nil ≍ (φ.mapPath p₂).cons (φ.map e₂)
⊢ False
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst✝ : MulAction M W
φ : SchreierGraph V ι ⥤q SchreierGraph W ι
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := ⟨s, ⋯⟩
h : ι ↑(φ.map e) • φ.obj v = φ.obj (ι s • v)
⊢ (φ ⋙q labelling W ι).map e = (labelling V ι).map e

Tactic:
rw [φm]

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

Goal state before:
pp: case cons.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₁ 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₂
h : φ.obj y₁ = φ.obj u ∧ (φ.mapPath p₁).cons (φ.map e₁) ≍ φ.mapPath Path.nil
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨u, Path.nil⟩

Tactic:
exfalso

Goal state after:
case cons.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₁ 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₂
h : φ.obj y₁ = φ.obj u ∧ (φ.mapPath p₁).cons (φ.map e₁) ≍ φ.mapPath Path.nil
⊢ False
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
⊢ schnirelmannDensity A ≤ 1 - (↑k)⁻¹

Tactic:
by
  rcases k.eq_zero_or_pos with rfl | hk'
  · simpa using schnirelmannDensity_le_one
  apply schnirelmannDensity_le_of_le k hk'.ne'
  rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne']
  gcongr
  rw [← Nat.cast_pred hk', Nat.cast_le]
  suffices {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)
  rw [← Ioo_insert_right hk', filter_insert, if_neg hk]
  exact filter_subset _ _

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ ∀ ⦃x : α⦄, (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x

Tactic:
exact fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_4
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
hn : n ≤ Fintype.card α
h𝒜 : Set.Sized (Fintype.card α - n) ↑𝒜
⊢ Set.Sized n ↑𝒜ᶜˢ

Tactic:
by simpa only [Nat.sub_sub_self hn] using h𝒜.compls

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

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

Tactic:
by
  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.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h : 𝒜 ⊆ ℬ
x✝ : Finset α
⊢ x✝ ∈ 𝒜.shatterer → x✝ ∈ ℬ.shatterer

Tactic:
simpa using Shatters.mono_left h

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

Goal state before:
pp: 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

pp: 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

Tactic:
· have huv' := G.reachable_or_compl_adj .. |>.resolve_left huv
    have hvw' := G.reachable_or_compl_adj .. |>.resolve_left fun hvw ↦ huv <| huw.trans hvw.symm
    exact huv'.reachable.trans hvw'.reachable

Goal state after:
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.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r s : Setoid α
| r ≤ s

Tactic:
rw [← mkClasses_classes r, ← mkClasses_classes s]

Goal state after:
α : Type u_1
r s : Setoid α
| mkClasses r.classes ⋯ ≤ mkClasses s.classes ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
hc : G.Colorable n
⊢ (SimpleGraph.map (⇑f) G).Colorable n

Tactic:
obtain ⟨C⟩ := hc

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
⊢ (SimpleGraph.map (⇑f) G).Colorable n
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inl
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

Tactic:
convert! Nat.zero_le _

Goal state after:
case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ #𝒜 = 0
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
⊢ card (Fin i) ≤ card α

Tactic:
simpa using h.le

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

Goal state before:
pp: case inl
V : Type u
h✝ : Finite V
⊢ ⊤.chromaticNumber = ENat.card V

pp: case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V

Tactic:
· have := Fintype.ofFinite ‹_›
    simp

Goal state after:
case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
hxy : s(x, y) ∈ w.edges
⊢ s(x, y) ∈ (w.dropUntil y ⋯).edges

Tactic:
simpa using (w.dropUntil y _).reverse.mem_edges_of_not_reachable_deleteEdges hvy

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ False

Tactic:
refine hw.not_mem_support_of_not_reachable (x := y) ?_ ?_ hxw

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable u x

case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable v x
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
s : Finset V
h : G.IsClique ↑s
hc : card α ≤ s.card
C : G.Coloring α
a✝¹ : α
a✝ : a✝¹ ∈ Set.univ
⊢ ↑(card α) ≤ (induce (↑s) G).chromaticNumber

Tactic:
by simp_all [← induce_eq_top]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x✝ : Set (Sym2 V)
hk : x✝.encard < ↑k
⊢ x✝.encard < ↑l

Tactic:
grw [← hkl]; exact hk

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
w : ↥t
| #(G.neighborFinset ↑w)

Tactic:
rw [isBipartiteWith_bipartiteBelow h w.prop]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
w : ↥t
| #(bipartiteBelow G.Adj s ↑w)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ (between s sᶜ G).Adj v w ∨ w ∈ s

Tactic:
between_adj

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ (between s sᶜ G).Adj w v ∨ v ∈ sᶜ

Tactic:
between_adj

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ