mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (M ／ I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)

Tactic:
indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (∃ B, (M ／ I).IsBase B ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.IsBase B ∧ J ∪ I ⊆ B
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ C ⊆ M.E \ D

Tactic:
by simpa [hCE, subset_sdiff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)

Tactic:
by
  rw [contract_eq_contract_iff, delete_ground, ← sdiff_inter_distrib_right, sdiff_eq, sdiff_eq,
    inter_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ M.IsBasis
        ((fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I)
        ((fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X) ∧
      N.IsBasis
        ((fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I)
        ((fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X) ↔
    M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)

Tactic:
convert! Iff.rfl <;> exact ext <| by simp

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

Goal state before:
pp: case succ.inr
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < n + 1
a : V
e : a ⟶ b
⊢ Nonempty (Path r b)

Tactic:
· rcases ih a (lt_of_lt_of_le (height_lt e) (Nat.lt_succ_iff.mp hn)) with ⟨p⟩
        exact ⟨p.cons e⟩

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b : WideSubquiver.toType V (geodesicSubtree r)⦄ (a_1 : a ⟶ b),
    (shortestPath r a).length < (shortestPath r b).length

Tactic:
rintro a b ⟨e, p, h⟩

Goal state after:
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length < (shortestPath r b).length
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
hf'0 : ¬m.subLTerm f = 0
hf0 : m.degree f = 0
⊢ False

Tactic:
apply hf'0

Goal state after:
σ : 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
hf0 : m.degree f = 0
⊢ m.subLTerm f = 0
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (↑⟨b, ⋯⟩ * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c

Tactic:
simp only at h1

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ m.degree (∏ r ∈ S, (X i - C r)) = single i #S

Tactic:
rw [degree_prod_of_regular]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∑ i_1 ∈ S, m.degree (X i - C i_1) = single i #S

R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∀ i_1 ∈ S, IsRegular (m.leadingCoeff (X i - C i_1))
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ (P S i).support
hP : P S i = (rename fun x ↦ i) (P S ())
⊢ ∃ e ≤ #S, m = single i e

Tactic:
hP,

Goal state after:
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ ((rename fun x ↦ i) (P S ())).support
hP : P S i = (rename fun x ↦ i) (P S ())
⊢ ∃ e ≤ #S, m = single i e
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₂
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₁, p₁.cons e₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ →
    ⟨y₁, p₁.cons e₁⟩ = ⟨u, Path.nil⟩

Tactic:
intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      exfalso
      obtain ⟨h, h'⟩ := h
      rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h'
      exact (Path.cons_ne_nil _ _) h'

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
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
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : g.totalDegree ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
rw [hg, ← degree_degLexDegree,
    degree_mul_of_isRegular_right hi (by simp only [(Alon.monic_P ..).leadingCoeff_eq_one,
      isRegular_one]),
    Alon.degree_P, map_add, degree_degLexDegree, degree_single, ht'] at this

Goal state after:
case neg
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
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: case mp
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t

Tactic:
exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case pos
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∈ A
⊢ n ∈ A + B

Tactic:
exact ⟨n, by simp [hnA], 0, ⟨hB, rfl⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
⊢ a ≤ s.truncatedSup a

Tactic:
rw [truncatedSup]
  split_ifs with h
  · obtain ⟨ℬ, hb, h⟩ := h
    exact h.trans <| le_sup' id <| mem_filter.2 ⟨hb, h⟩
  · exact le_top

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u : Finset α
⊢ s ○ t ○ u = s ○ u ○ t

Tactic:
simp_rw [disjSups_assoc, disjSups_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
h : a ∈ 𝓒 u v s
ha : a ∉ s
⊢ (a ⊔ v) \ u ∈ s

Tactic:
rw [mem_compression] at h
  obtain h | ⟨-, b, hb, hba⟩ := h
  · cases ha h.1
  unfold compress at hba
  split_ifs at hba with h
  · rwa [← hba, sdiff_sup_cancel (le_sup_of_le_left h.2), sup_sdiff_right_self,
      h.1.symm.sdiff_eq_left]
  · cases ne_of_mem_of_not_mem hb ha hba

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

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint c c

Tactic:
rwa [disjoint_self]

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

Goal state before:
pp: case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty

Goal state after:
case intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
r : ℕ
inst✝ : Finite α
val✝ : Fintype α
hr : r > 0
h₁ : IsInitSeg ∅ r
⊢ IsInitSeg (∂ ∅) (r - 1)

case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s

Tactic:
by
  refine mem_filter.trans <| and_iff_right_of_imp fun h ↦ ?_
  simp_rw [mem_biUnion, mem_powerset]
  exact h.exists_superset

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this✝ : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
‹erase U x = ∅›,

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this✝ : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed ∅ (V.erase (V.min' hV)) 𝒜
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r : Setoid α
a : α
⊢ ∀ (y : Set α), y ∈ r.classes ∧ a ∈ y → y = {x | r x a}

Tactic:
rintro y ⟨⟨_, rfl⟩, ha⟩
    ext x
    exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩

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

Goal state before:
pp: n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
classical
  -- Are there any compressions we can make now?
  set usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t | UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 𝒜}
  obtain husable | husable := usable.eq_empty_or_nonempty
  -- No. Then where we are is the required set family.
  · refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
    rw [eq_empty_iff_forall_notMem] at husable
    by_contra h
    exact husable ⟨U, V⟩ <| mem_filter.2 ⟨mem_univ _, hUV, h⟩
  -- Yes. Then apply the smallest compression, then keep going
  obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ #t.1) husable
  rw [mem_filter] at hUV
  have h₂ : ∀ U₁ V₁, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜 := by
    rintro U₁ V₁ huseful hUcard
    by_contra h
    exact hUcard.not_ge <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩
  have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂
  obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
  have := familyMeasure_compression_lt_familyMeasure hmax hUV.2.2
  obtain ⟨t, q1, q2, q3, q4⟩ := UV.kruskal_katona_helper (𝓒 U V 𝒜) (h.uvCompression hUV')
  exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
⊢ IsPartition s

Tactic:
by
  refine ⟨h₃, fun a ↦ existsUnique_of_exists_of_unique (h₂ a) ?_⟩
  intro b₁ b₂ hb₁ hb₂
  apply h₁.elim hb₁.1 hb₂.1
  simp only [Set.not_disjoint_iff]
  exact ⟨a, hb₁.2, hb₂.2⟩

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right✝ : ∀ (y_1 : Set α), (fun b ↦ b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
⊢ {x | (mkClasses c ⋯) x y} ∈ c

Tactic:
← eq_eqv_class_of_mem _ hb hy

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right✝ : ∀ (y_1 : Set α), (fun b ↦ b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
⊢ b ∈ c
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ H.Adj ((C (G.connectedComponentMk a✝)) ⟨a✝, ⋯⟩) ((C (G.connectedComponentMk b✝)) ⟨b✝, ⋯⟩)

Tactic:
convert (C (G.connectedComponentMk _)).map_rel h using 3 <;>
      rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ (∃ y, y.supp = ↑(G.connectedComponentMk v)) ∧ v ∈ G.connectedComponentMk v

Tactic:
exact ⟨⟨G.connectedComponentMk v, rfl⟩, rfl⟩

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

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

Tactic:
chromaticNumber_le_iff_colorable

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable (n + 1) ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.chromaticNumber ≤ ↑1

Tactic:
chromaticNumber_le_iff_colorable

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.Colorable 1
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.reverse.toSubgraph = p.toSubgraph

Tactic:
by
  induction p with
  | nil => simp
  | cons _ _ _ =>
    simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
    rw [sup_comm]
    congr
    ext <;> simp [-Set.bot_eq_empty]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v

Tactic:
(Order.one_le_iff_pos.mpr h).ge_iff_eq'

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v = 1 ↔ G.Adj u v
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
h : i ≠ 0
h' : i < p.length
⊢ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

Tactic:
hp.neighborSet_toSubgraph_internal h h'

Goal state after:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2
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
h : i ≠ 0
h' : i < p.length
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

Tactic:
have : p.getVert (i - 1) ≠ p.getVert (i + 1) := by
    intro h
    have := hp.getVert_injOn (by rw [Set.mem_ofPred_eq]; lia) (by rw [Set.mem_ofPred_eq]; lia) h
    lia

Goal state after:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
this : p.getVert (i - 1) ≠ p.getVert (i + 1)
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ ↑wG.length + ↑wH.length = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
by simp only [hwG, hwH]

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

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
⊢ (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber

Tactic:
refine eq_max chromaticNumber_le_sum_left chromaticNumber_le_sum_right fun {d} hG hH => ?_

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
d : ℕ∞
hG : G.chromaticNumber ≤ d
hH : H.chromaticNumber ≤ d
⊢ (G ⊕g H).chromaticNumber ≤ d
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: ⊢ pathGraph 2 = ⊤

Tactic:
by
  ext u v
  fin_cases u <;> fin_cases v <;> simp [pathGraph]

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

Goal state before:
pp: case refine_1.inl.inr.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inl i ∈ left
j : V
hj : Sum.inr j ∈ right
⊢ G.Adj i j

Tactic:
simpa using h hi hj

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

Goal state before:
pp: case refine_1.inr.inl.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : Sum.inl j ∈ right
⊢ G.Adj i j

Tactic:
simpa using h hi hj

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

Goal state before:
pp: case inr
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
u : V
p : (sSup Hs).Walk u u
hp : p.IsCycle
H : SimpleGraph V
hH : H ∈ Hs
hpH : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ False

Tactic:
exact h_acyc H hH (p.transfer H hpH) <| Walk.IsCycle.transfer hp hpH

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

Goal state before:
pp: case refine_1
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ sSup c ≤ G

Tactic:
grind [sSup_le_iff]

Goal state after: