mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ (fun x ↦
        match x with
        | (g, g') =>
          ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
              invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
              left_inv := ⋯, right_inv := ⋯ },
            ⋯⟩)
      ((fun f ↦
          ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ },
            { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ }))
        f) =
    f

Tactic:
by
    ext x
    by_cases hx : x ∈ s
    · simp [hx]
    · rw [mem_prefixed.1 f.2, not_lt] at hx
      simp [hx]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶.IsBasis ((M.E \ I) \ B) (M.E \ I) ∧ B ⊆ M.E ↔ M✶.IsBase (M.E \ (I ∪ B)) ∧ I ∪ B ⊆ M.E)

Tactic:
union_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶.IsBasis ((M.E \ I) \ B) (M.E \ I) ∧ B ⊆ M.E ↔ M✶.IsBase (M.E \ (I ∪ B)) ∧ I ⊆ M.E ∧ B ⊆ M.E)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
union_subset_iff,

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X ⊆ (M ／ C).closure X \ X ∪ M.closure (C ∪ X) \ C ∩ X ∧
    (M ／ C).closure X \ X ∪ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X

Tactic:
union_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X ⊆ (M ／ C).closure X \ X ∪ M.closure (C ∪ X) \ C ∩ X ∧
    (M ／ C).closure X \ X ⊆ (M ／ C).closure X ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ M.closure (X ∪ C) \ C = M.E \ C ∧ X ⊆ M.E \ C ↔ (M.closure (X ∪ C) = M.E ∧ X ∪ C ⊆ M.E) ∧ Disjoint X C

Tactic:
union_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ M.closure (X ∪ C) \ C = M.E \ C ∧ X ⊆ M.E \ C ↔ (M.closure (X ∪ C) = M.E ∧ X ⊆ M.E ∧ C ⊆ M.E) ∧ Disjoint X C
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := ⋯
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := ⋯
hn : n none = d ∧ n.some = m
hm : ¬coeff n P = 0
⊢ d ≤ degreeOf none P

Tactic:
rw [MvPolynomial.degreeOf_eq_sup]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n none = d ∧ n.some = m
hm : ¬coeff n P = 0
⊢ d ≤ P.support.sup fun m ↦ m none
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
⊢ ∃ u, u ∈ S ∧ ∃ v, ¬v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
have ha_not_in_compl : a ∉ Sᶜ := by simpa
  have hb_in_compl : b ∈ Sᶜ := by simpa
  obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
  simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
  refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩

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

Goal state before:
pp: case cons
V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j b✝ c✝ : V
p : Path i b✝
e : b✝ ⟶ c✝
ih : 0 < weight (fun {i j} ↦ w) p
he : 0 < w e
⊢ 0 < weight (fun {i j} ↦ w) (p.cons e)

Tactic:
simpa [weight_cons] using mul_pos ih he

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Tactic:
exact ⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ {s ∈ 𝒜 | a ∈ s}

Tactic:
simp only [mem_memberSubfamily, mem_image, mem_filter]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1

Tactic:
have hm : 2 ≤ m := hm.lt_of_le' hm'

Goal state after:
m : ℕ
hm✝ : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: 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
⊢ A + B = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
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
⊢ ∀ (x : ℕ), x ∈ A + B
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t

Tactic:
· rintro ⟨v, hv, w, hw, rfl⟩
    exact union_subset_union hv hw

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ lowerClosure ↑(s ⊼ t) ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t

Tactic:
rw [coe_infs, lowerClosure_infs, LowerSet.mem_inf_iff]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
hℬ : s ∈ upperClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
truncatedInf_union h𝒜 hℬ,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
hℬ : s ∈ upperClosure ↑ℬ
⊢ #(𝒜.truncatedInf s ⊓ ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
by
  have : ∀ t : Finset α,
    (card α - #(truncatedSup {s} t) : ℚ) / ((card α - #t) * (card α).choose #t) =
    if t ⊆ s then (card α - #s : ℚ) / ((card α - #t) * (card α).choose #t) else 0 := by
    rintro t
    simp_rw [truncatedSup_singleton]
    split_ifs <;> simp
  simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq,
    ← eq_sub_iff_add_eq', supSum, ← sum_sub_distrib, ← sub_div]
  rw [sum_congr rfl fun t _ ↦ this t, sum_ite, sum_const_zero, add_zero, filter_subset_univ,
    sum_powerset, ← binomial_sum_eq ((card_lt_iff_ne_univ _).2 hs), eq_comm]
  refine sum_congr rfl fun n _ ↦ ?_
  rw [mul_div_assoc, ← nsmul_eq_mul]
  exact sum_powersetCard n s fun m ↦ (card α - #s : ℚ) / ((card α - m) * (card α).choose m)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
hsb : insert b ((t ∪ u.erase a) \ v) ∈ 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜

Tactic:
union_erase_of_mem hat,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
hsb : insert b ((t ∪ u) \ v) ∈ 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
⊢ ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)

Tactic:
refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
j : ι
hj : j ∈ cons i s hi
⊢ 2 * #(f' j) = Fintype.card (Finset α)
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
j : ι
hj : j ∈ cons i s hi
⊢ 2 * #(f' j) = 2 ^ Fintype.card α

Tactic:
exact (hf₁ _ hj).2.1

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s

Tactic:
mem_bipartiteBelow

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
inst✝² : Nontrivial V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.Preconnected
⊢ 0 < G.minDegree

Tactic:
by
  obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
  rw [hv]
  exact h.degree_pos_of_nontrivial v

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v' = c'

Tactic:
rw [ConnectedComponent.sound (hv'.mono h)]

Goal state after:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = c'
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (p.toSubgraph.neighborSet w).Finite

Tactic:
induction p with
  | nil =>
    rw [Walk.toSubgraph, neighborSet_singletonSubgraph]
    apply Set.toFinite
  | cons ha _ ih =>
    rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
    refine Set.Finite.union ?_ ih
    refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
    apply Set.toFinite

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
⊢ G.degree w ≤ (between (↑s) (↑s)ᶜ G).degree w + #sᶜ

Tactic:
have h_bipartite : (G.between s sᶜ).IsBipartiteWith s ↑(sᶜ) := by
    simpa using between_isBipartiteWith disjoint_compl_right
  simp_rw [← card_neighborFinset_eq_degree,
    ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint' h_bipartite hw)]
  exact card_le_card (neighborFinset_subset_between_union_compl hw)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
by_cases! huw : ¬G.Reachable u w
  · grind [dist_eq_zero_iff_eq_or_not_reachable, Reachable.trans, Adj.reachable]
  have : G.dist v w = 1 := dist_eq_one_iff_adj.mpr hadj
  have : G.dist w v = 1 := dist_eq_one_iff_adj.mpr hadj.symm
  have : G.dist u w ≤ G.dist u v + G.dist v w := hadj.reachable.dist_triangle_right u
  have : G.dist u v ≤ G.dist u w + G.dist w v := huw.dist_triangle_left v
  lia

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
v : V
w : W
hG : G.Connected
hH : H.Connected
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected

Tactic:
by
  obtain ⟨hG⟩ := hG; exact ⟨hG.sum_sup_edge hH.preconnected⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
⊢ (Subgraph.map f G'').Preconnected

Tactic:
by
  rw [Subgraph.preconnected_iff]
  intro ⟨u', u, hu, hfu⟩ ⟨v', v, hv, hfv⟩
  simp_rw [← hfu, ← hfv]
  exact (hpreconn.coe ⟨u, hu⟩ ⟨v, hv⟩).coe_subgraphMap f

Goal state after:
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[⟨y + 1, ⋯⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
exact p.isChain_adj_support.getElem _ _ |>.symm

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ Disjoint {v | v.isLeft = true} {w | w.isRight = true}

Tactic:
by simp [Set.disjoint_iff_forall_ne]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
⊢ (induce {v}ᶜ G).Connected

Tactic:
obtain ⟨u, adj_vu, hu⟩ := degree_eq_one_iff_existsUnique_adj.mp hdeg

Goal state after:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
⊢ (induce {v}ᶜ G).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (C.labelGraph k).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k

Tactic:
rw [EdgeLabeling.labelGraph]
  simp only [mem_edgeSet, fromEdgeSet_adj, Set.mem_ofPred_eq, Ne.eq_def]
  grind [Adj.ne]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ G.center = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ ∀ (x : α), x ∈ G.center
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊥.center = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ∀ (x : α), x ∈ ⊥.center
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊤.center = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ∀ (x : α), x ∈ ⊤.center
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ G.componentComplMk vK = G.componentComplMk wK

Tactic:
by
  rw [ConnectedComponent.eq]
  apply Adj.reachable
  exact a

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := ⋯
dis : K ∩ ↑C ⊆ ∅ := ⋯
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
⊢ ↑C = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
⊢ ∀ (x : V), x ∈ ↑C
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
h : ¬1 = 0
⊢ (s ∩ Function.support fun i ↦ 1).Infinite

Tactic:
by simpa [Function.support_const h]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ Nonempty (↑s ≃ ↑s ⊕ ↑s)

Tactic:
by
    rw [← Cardinal.eq, ← add_def, add_mk_eq_self]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : (t ∪ u).Finite
⊢ Even (t ∪ u).ncard

Tactic:
finite_union

Goal state after:
case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
⊢ Even (t ∪ u).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w

Tactic:
obtain ⟨w, hw⟩ := h hv

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
w : V
hw : (fun w ↦ M.Adj w✝ w) w ∧ ∀ (y : V), (fun w ↦ M.Adj w✝ w) y → y = w
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ Fintype.card α - 1 + 1 = Fintype.card α

Tactic:
Nat.sub_add_cancel

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ Fintype.card α = Fintype.card α

α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ 1 ≤ Fintype.card α
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| ((∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
      ∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) /
    2

Tactic:
enter [1, 2, 2, i, 2, j]; rw [if_congr (adj_comm G i j) rfl rfl]

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i j : V
| if G.Adj j i then x i * x i - x i * x j else 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
subst hvw
    use .nil

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case succ
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (n + 1) 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (decode (n + 1))

Tactic:
decode_option_succ

Goal state after:
case succ
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (n + 1) 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) =
    encode (Option.map some (decode n))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
⊢ f = g

Tactic:
funext a b; apply H

Goal state after: