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

Goal state before:
pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ p.nest.firstReturn = (↑p).length + 1

Tactic:
rw [firstReturn, findIdx_eq]

Goal state after:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ decide
        (count U (List.take ((range (↑p.nest).length)[(↑p).length + 1] + 1) ↑p.nest) =
          count D (List.take ((range (↑p.nest).length)[(↑p).length + 1] + 1) ↑p.nest)) =
      true ∧
    ∀ (j : ℕ) (hji : j < (↑p).length + 1),
      decide
          (count U (List.take ((range (↑p.nest).length)[j] + 1) ↑p.nest) =
            count D (List.take ((range (↑p.nest).length)[j] + 1) ↑p.nest)) =
        false

p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (range (↑p.nest).length).length
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
⊢ Summable fun j ↦ f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))

Tactic:
by
  apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top
  apply tendsto_order_genFun_term_atTop_nhds_top

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
⊢ (mu 𝕜) (ofDual (toDual b)) (ofDual (toDual a)) = (mu 𝕜) b a

Tactic:
ofDual_toDual

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

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < p.firstReturn + 1
⊢ count D (List.take i ↑p) < count U (List.take i ↑p)

Tactic:
show i = i - 1 + 1 by lia

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 + 1 < p.firstReturn + 1
⊢ count D (List.take (i - 1 + 1) ↑p) < count U (List.take (i - 1 + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p✝ q✝ : DyckWord
h : p✝ ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
h₁ : ↑p <:+: ↑q
h₂ : ↑q <:+: ↑p
⊢ p = q

Tactic:
exact DyckWord.ext <| h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

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
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun n ↦ ∑ x_1 ∈ Finset.range n, (aux k (x_1 + 1) x - aux k x_1 x)) atTop (𝓝 (0 - aux k 0 x))

Tactic:
Finset.sum_range_sub (aux k · x)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun n ↦ aux k n x - aux k 0 x) atTop (𝓝 (0 - aux k 0 x))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h : HasProd (fun n ↦ 1 - X ^ (n + 1)) (∏' (b : ℕ), (1 - X ^ (b + 1)))
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)

Tactic:
rw [tprod_one_sub_X_pow' R, HasProd, tendsto_iff_coeff_tendsto] at h

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h :
  ∀ (d : ℕ),
    Tendsto (fun i ↦ (coeff d) (∏ b ∈ i, (1 - X ^ (b + 1)))) (SummationFilter.unconditional ℕ).filter
      (𝓝 ((coeff d) (pentagonalSeries R)))
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)
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)

Goal state after:
n : ℕ
α : Type := Fin (2 * n + 1)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)
Module: Mathlib.Combinatorics.Graph.Lattice

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

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

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr.inr
η : 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
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ Sum.inr e = Sum.inr f

Tactic:
simp only [Sum.inr.injEq]

Goal state after:
case inr.inr
η : 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
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ e = f
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)
x : X
hx✝ : x ∈ sᶜ
hx : #s ≤ ↑(↑f x)
⊢ (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩) ⟨x, hx✝⟩) = ⟨x, hx✝⟩

Tactic:
simp [Nat.sub_add_cancel hx]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (M✶✶ ＼ X)✶ = M✶✶✶ ／ X

Tactic:
dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶ ／ X = M✶✶✶ ／ X
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_4
α : 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
⊢ (Multiset.map AlmostMono.color
      ({ line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ::ₘ
        Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines)).Nodup

Tactic:
Multiset.map_cons,

Goal state after:
case neg.refine_4
α : 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
⊢ ({ line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ }.color ::ₘ
      Multiset.map AlmostMono.color
        (Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines)).Nodup
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨ι × Shrink η, inferInstance, fun C ↦ ?_⟩

Goal state after:
case intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
⊢ ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case refine_5
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X
h' : ∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
⊢ X ⊆ univ.sigma fun i ↦ (M i).E

Tactic:
exact fun ⟨i,x⟩ hx ↦ by simpa using h'' i hx

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

Goal state before:
pp: case cons
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
b✝ : V
p : Path r b✝
e : b✝ ⟶ b
hp : shortestPath r b = p.cons e
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)

Tactic:
· exact Or.inr ⟨_, ⟨⟨e, p, hp⟩⟩⟩

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

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
⊢ IsSStronglyConnected V

Tactic:
intro i j
  obtain ⟨p₁⟩ := h_sc i i₀
  obtain ⟨p₂⟩ := h_sc j₀ j
  let p : Path i j := p₁.comp (e₀.toPath.comp p₂)
  have hp_pos : 0 < p.length := by
    simpa [p, Path.length_comp, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
      Nat.succ_pos (p₁.length + p₂.length)
  exact ⟨p, hp_pos⟩

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

Goal state before:
pp: σ : 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
a✝ :
  ∀ (y : MvPolynomial σ R),
    (invImage (fun x ↦ ⋯.wrap (m.toSyn (m.degree x))) Acc.wfRel).1 y f →
      ∃ g r,
        y = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree y)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ i, m.degree (b i) = 0
hf0 : ¬f = 0
hf✝ : ∃ i, m.degree (b i) ≤ m.degree f
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
⊢ ↑(⋯.wrap (m.toSyn (m.degree (m.reduce ⋯ f)))) < ↑(⋯.wrap (m.toSyn (m.degree f)))

pp: σ : 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
a✝ :
  ∀ (y : MvPolynomial σ R),
    (invImage (fun x ↦ ⋯.wrap (m.toSyn (m.degree x))) Acc.wfRel).1 y f →
      ∃ g r,
        y = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree y)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ i, m.degree (b i) = 0
hf0 : ¬f = 0
hf : ¬∃ i, m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
⊢ ↑(⋯.wrap (m.toSyn (m.degree (m.subLTerm f)))) < ↑(⋯.wrap (m.toSyn (m.degree f)))

Tactic:
· exact deg_reduce
  · apply degree_sub_LTerm_lt
    intro hf0
    apply hf'0
    simp only [subLTerm, sub_eq_zero]
    nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0]
    simp

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

Goal state before:
pp: 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
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hxPrev : v ∈ pPrev.vertices
hxe_ne : v ≠ (pPrev.cons e).end
q₁ : Path a v
q₂ : Path v b✝
h_prev : pPrev = q₁.comp q₂
h_not_tail : ¬v ∈ q₂.vertices.tail
q₂' : Path v (pPrev.cons e).end := q₂.cons e
⊢ ¬v ∈ q₂'.vertices.tail

Tactic:
grind [vertices_cons, end_cons]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
⊢ a ∈ ↑((fun a ↦ { carrier := {b | ↑b ≤ a}, lower' := ⋯ }) ((fun s ↦ (↑s).toFinset.sup Subtype.val) s)) ↔ a ∈ ↑s

Tactic:
dsimp

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
⊢ a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ } ↔ a ∈ ↑s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s

Tactic:
rintro ⟨t, ht, hts, hcard⟩
      obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1)
        (by lia)
      refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
      rw [hu, ← hcard, add_right_comm]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₁ : UsefulCompression U V
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)

Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
  refine card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, ?_⟩
  obtain hU' | hU' := eq_or_lt_of_le (succ_le_iff.2 hU.card_pos)
  · rw [← hU'] at same_size
    have : erase U x = ∅ := by rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
    have : erase V (min' V hV) = ∅ := by
      rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]
    rw [‹erase U x = ∅›, ‹erase V (min' V hV) = ∅›]
    exact isCompressed_self _ _
  refine h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)
  · rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]
  · rwa [← card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt]
  · rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]
  · exact (Finset.max'_subset _ <| erase_subset _ _).trans_lt (max_lt.trans_le <| le_max' _ _ <|
      mem_erase.2 ⟨(min'_lt_max'_of_card _ (by rwa [← same_size])).ne', max'_mem _ _⟩)

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

Goal state before:
pp: V : Type u
⊢ ⊥.Preconnected ↔ Subsingleton V

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [Preconnected]⟩
  contrapose! h
  simp [nontrivial_iff.mp h, Preconnected, reachable_bot]

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

Goal state before:
pp: V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w : V
hw : w ≠ v
p : G.Walk v w
⊢ v ∈ G.support

Tactic:
cases p with
  | nil => contradiction
  | @cons _ w => exact ⟨w, ‹_›⟩

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

Goal state before:
pp: V : Type u
⊢ (completeGraph V).Connected ↔ Nonempty V

Tactic:
simp [connected_iff]

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

Goal state before:
pp: case inr.convert_5
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝³ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r (↑𝒜 ∪ ↑(∂^[n - 2 * r] 𝒜ᶜˢ))

Tactic:
Set.sized_union

Goal state after:
case inr.convert_5
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝³ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r ↑𝒜 ∧ Set.Sized r ↑(∂^[n - 2 * r] 𝒜ᶜˢ)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
⊢ ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset

Tactic:
← Finset.sum_subset hsub,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
⊢ ∑ x ∈ G.support.toFinset, G.degree x = 2 * #G.edgeFinset

V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
⊢ ∀ x ∈ s ∪ t, x ∉ G.support.toFinset → G.degree x = 0
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄,
      v_1 ∈ w.toSubgraph.verts → ∀ ⦃w_1 : V⦄, w_1 ∈ w.toSubgraph.verts → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    ∀ (x y : V),
      ¬(s(x, y) ∈ G.edgeSet ∧
          s(x, y) ∉ w.edges ∧ Sym2.lift ⟨fun v_1 w_1 ↦ v_1 ∈ w.support ∧ w_1 ∈ w.support, ⋯⟩ s(x, y))

Tactic:
Sym2.lift_mk,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄,
      v_1 ∈ w.toSubgraph.verts → ∀ ⦃w_1 : V⦄, w_1 ∈ w.toSubgraph.verts → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    ∀ (x y : V), ¬(s(x, y) ∈ G.edgeSet ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ (μ * f) a * (μ * g) b ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))

Tactic:
dsimp

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ μ a * f a * (μ b * g b) ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
rw [penultimate, ← getVert_reverse] at hr

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph.Connected

Tactic:
induction p with
  | nil => apply singletonSubgraph_connected
  | @cons _ w _ h p ih =>
    apply Subgraph.connected_sup (subgraphOfAdj_connected h).preconnected ih.preconnected
    exists w
    simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this✝ : (hasse α).Adj a b
this : (hasse α).Adj b c
⊢ False

Tactic:
have := hc (by simp) (by simp) hac

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this✝¹ : (hasse α).Adj a b
this✝ : (hasse α).Adj b c
this : (hasse α).Adj a c
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ (u v : V) (x y : G.Path u v), x = y
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
⊢ p = ↑q

Tactic:
specialize hu v w ⟨p, hp⟩ q

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
hc : G.Connected
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
hu : ⟨p, hp⟩ = q
⊢ p = ↑q
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
this✝ : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
this : u' = (tail.takeUntil u' hh).snd
⊢ s(u', v') ∈ (cons ⋯ tail.tail).edges.head?

Tactic:
simp [this, snd_takeUntil head.ne]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ {x | H.Free x}

Tactic:
rw [mem_filter, ← free_congr .refl (.map e G)]

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ {x | H.Free x}

Tactic:
rw [mem_filter, ← free_congr .refl (.map e G)]

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G).compl = adjMatrix α Gᶜ

Tactic:
by aesop (add simp [Matrix.compl])

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

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
⊢ F.Reachable u v ↔ G.Reachable u v

Tactic:
refine ⟨.mono h.prop.left, fun ⟨p⟩ ↦ ?_⟩

Goal state after:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
⊢ F.Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ ¬Even p.length ↔ (¬c u = true ↔ c v = true)

Tactic:
c.even_length_iff_congr p

Goal state after:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ ¬(c u = true ↔ c v = true) ↔ (¬c u = true ↔ c v = true)