mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
⊢ coeff t f = 0

Tactic:
rw [hf]

Goal state after:
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
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
⊢ coeff t ((linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h) = 0
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
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
⊢ ⟨(ι ((labelling V ι).map ⟨s, hs⟩))⁻¹ • x, ⟨s, ⋯⟩⟩ = ⟨v, ⟨s, hs⟩⟩

Tactic:
have : (ι s)⁻¹ • x = v := by rw [← hs, inv_smul_smul]

Goal state after:
V : Type u_1
M : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
this : (ι s)⁻¹ • x = v
⊢ ⟨(ι ((labelling V ι).map ⟨s, hs⟩))⁻¹ • x, ⟨s, ⋯⟩⟩ = ⟨v, ⟨s, hs⟩⟩
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v

Tactic:
le_sdiff_right.1 h'.2,

Goal state after:
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ ⊥ ⊔ u) \ ⊥ = (a ⊔ u) \ ⊥
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑(s ∪ t)

Tactic:
rw [coe_union, upperClosure_union]

Goal state after:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑s ⊓ upperClosure ↑t
Module: Mathlib.Order.Irreducible

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : s.sup f = a
⊢ ∃ i ∈ s, f i = a

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simpa [ha.ne_bot] using h.symm
  | insert i s _ ih =>
    simp only [exists_mem_insert] at ih ⊢
    rw [sup_insert] at h
    exact (ha.2 h).imp_right ih

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + 1

Tactic:
refine mem_upShadow_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = 1 ↔ #t✝ = #t + 1
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ b ⊓ c ≤ a → b ≤ a ∨ c ≤ a

Tactic:
simp_rw [← sup_eq_left, sup_inf_left]

Goal state after:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
⊢ s.Intersecting ↔ (s.Pairwise fun a b ↦ ¬Disjoint a b) ∧ s ≠ {⊥}

Tactic:
by
  refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩
  · rintro rfl
    exact intersecting_singleton.1 h rfl
  have := h.1.eq ha hb (Classical.not_not.2 hab)
  rw [this, disjoint_self] at hab
  rw [hab] at hb
  exact
    h.2
      (eq_singleton_iff_unique_mem.2
        ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)

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

Goal state before:
pp: case mpr.inr.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)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ insert j t

pp: case mpr.inr.inr.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)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert j t

pp: case mpr.inr.inr.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
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ insert j t

Tactic:
· apply mem_insert_of_mem
    rw [z lt]
    refine mem_erase_of_ne_of_mem (lt_of_le_of_lt ?_ lt).ne' ha
    apply min'_le _ _ (mem_of_mem_erase ‹_›)

Goal state after:
case mpr.inr.inr.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)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert j t

case mpr.inr.inr.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
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ insert j t
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
x✝ : x ∈ range (hs.piecewise f)
y : α
hy : hs.piecewise f y = x
⊢ x ∈ ⋃ i, range (f i)

Tactic:
by simpa [IndexedPartition.piecewise_apply] using ⟨hs.index y, y, hy⟩

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

Goal state before:
pp: 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
⊢ (n - 1).choose (n - r) < #𝒜ᶜˢ

Tactic:
card_compls,

Goal state after:
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
⊢ (n - 1).choose (n - r) < #𝒜
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_4.e'_1
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] 𝒜ᶜˢ)
⊢ n = Fintype.card (Fin n)

pp: case inr.convert_2
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] 𝒜ᶜˢ)
⊢ Fintype (Fin n)

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:
· rw [Fintype.card_fin]

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 ↑(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
⊢ G.chromaticNumber ≤ ↑(card V) - 1

Tactic:
obtain ⟨a, b, hne, _⟩ := ne_top_iff_exists_not_adj.mp hh

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
⊢ G.chromaticNumber ≤ ↑(card V) - 1
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
⊢ y ∉ w.support

Tactic:
classical
  exact fun hy ↦ hw.not_mem_edges_of_not_reachable huy hvy <| w.edges_takeUntil_subset_edges hy <|
    mem_edges_of_not_reachable_deleteEdges (w.takeUntil y hy) huy

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

Goal state before:
pp: case inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝) w → (Sum.inl val✝).isRight ≠ w.isRight

Tactic:
cases w

Goal state after:
case inl.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inl val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inl val✝).isRight

case inl.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : V
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inr val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inr val✝).isRight
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝) w → (Sum.inr val✝).isRight ≠ w.isRight

Tactic:
cases w

Goal state after:
case inr.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inl val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inl val✝).isRight

case inr.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inr val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inr val✝).isRight
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
⊢ v ∈ s

Tactic:
have nhw : w ∉ s := Set.disjoint_right.mp h.disjoint hw

Goal state after:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
nhw : w ∉ s
⊢ v ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : G.Adj v w
⊢ v ∈ s

Tactic:
apply h.mem_of_adj at hadj
  have nhw : w ∉ s := Set.disjoint_right.mp h.disjoint hw
  simpa [hw, nhw] using hadj

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 < ↑k

Tactic:
exact hk

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : ↑H.verts
inst✝ : Fintype ↑(H.neighborSet ↑v)
hv : H.degree ↑v = 0
hn : H.verts.Nontrivial
⊢ False

Tactic:
have := hn.coe_sort

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : ↑H.verts
inst✝ : Fintype ↑(H.neighborSet ↑v)
hv : H.degree ↑v = 0
hn : H.verts.Nontrivial
this : Nontrivial ↑H.verts
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) →
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
rintro ⟨i', ⟨hl, _⟩ | ⟨_, hl⟩⟩

Goal state after:
case inl
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

case inr
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ G.dist u v = 0 ↔ u = v

Tactic:
by simp [hr]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ 1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    w'.ofBoxProdLeft.length + 1 +
      (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length

Tactic:
add_comm w'.ofBoxProdLeft.length 1,

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ 1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    1 + w'.ofBoxProdLeft.length +
      (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
have hadj1 := ((show i - 1 + 1 = i by lia) ▸
    p.toSubgraph_adj_getVert (by lia : (i - 1) < p.length)).symm
  ext v
  simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
    Prod.swap_prod_mk]
  refine ⟨?_, by aesop⟩
  rintro ⟨i', ⟨hl1, hl2⟩ | ⟨hr1, hr2⟩⟩
  · apply hpc.getVert_injOn' (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hl1
    simp_all
  · apply hpc.getVert_injOn (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hr2
    aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
⊢ H.Preconnected

Tactic:
rintro b₁ b₂

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
⊢ H.Reachable b₁ b₂
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h✝ : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
⊢ {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}

Tactic:
rwa [Finset.filter_erase, ← Finset.subset_empty, ← Finset.subset_insert_iff,
    LawfulSingleton.insert_empty_eq] at h

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

Goal state before:
pp: case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ s ∪ t = s ∪ t

Tactic:
rw [Set.union_assoc]

Goal state after:
case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ (s ∪ t) = s ∪ t
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
simp_rw [show x = y + 1 by grind [Fin.sub_val_of_le]]

Goal state after:
case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨y + 1, ⋯⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case notNil
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ ¬(f w).Nil

pp: case memEdges
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ ((f a).firstDart ⋯).edge ∈ G.edgeFinset

pp: case inj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

pp: case surj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = b

Tactic:
case notNil => exact not_nil_of_ne (by simpa using hw)

Goal state after:
case memEdges
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ ((f a).firstDart ⋯).edge ∈ G.edgeFinset

case inj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

case surj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = b
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
⊢ extremalNumber n H' ≤ extremalNumber n H

Tactic:
rw [← Fintype.card_fin n, extremalNumber_le_iff]
  intro _ _ h'
  contrapose! h'
  exact h.trans (IsContained.of_extremalNumber_lt_card_edgeFinset h')

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
x y : V → α
⊢ x ⬝ᵥ adjMatrix α G *ᵥ y = ∑ i, ∑ j, if G.Adj i j then x i * y j else 0

Tactic:
simp [dotProduct, mulVec, mul_sum]

Goal state after: