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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
GV : Set α
GL : β → α → α → Prop
GE : Set β
isLink_symm✝¹ : ∀ ⦃e : β⦄, e ∈ GE → Std.Symm (GL e)
eq_or_eq_of_isLink_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, GL e x y → GL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝¹ : ∀ (e : β), e ∈ GE ↔ ∃ x y, GL e x y
left_mem_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y : α⦄, GL e x y → x ∈ GV
HV : Set α
HL : β → α → α → Prop
HE : Set β
isLink_symm✝ : ∀ ⦃e : β⦄, e ∈ HE → Std.Symm (HL e)
eq_or_eq_of_isLink_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, HL e x y → HL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝ : ∀ (e : β), e ∈ HE ↔ ∃ x y, HL e x y
left_mem_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y : α⦄, HL e x y → x ∈ HV
h :
  { vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝¹ } ≤s
    { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝, left_mem_of_isLink := left_mem_of_isLink✝ }
u v :
  ↑V({ vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝¹ })
hadj :
  { vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
          eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
          edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹,
          left_mem_of_isLink := left_mem_of_isLink✝¹ }.toSimpleGraph.Adj
    u v
⊢ (⋯ ▸
        { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
            edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝,
            left_mem_of_isLink := left_mem_of_isLink✝ }.toSimpleGraph).Adj
    u v

Tactic:
obtain ⟨hne, hadj⟩ := toSimpleGraph_adj .. ▸ hadj
    obtain ⟨hle, h⟩ := h
    simp only at h
    subst GV
    simp [toSimpleGraph_adj, hne, hadj.mono hle]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ Subspace.IsMono C l.toSubspaceUnit ↔ IsMono C l

Tactic:
simp only [Subspace.IsMono, toSubspaceUnit_apply, IsMono]
  exact exists_congr fun c ↦ ⟨fun h a ↦ h fun _ ↦ a, fun h a ↦ h _⟩

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
hNM : N ≤r M
⊢ N = M ＼ (M.E \ N.E)

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM; rw [delete_compl, restrict_ground_eq]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ (D₂ ∪ D₁) = M ＼ D₂ ＼ D₁

Tactic:
delete_delete

Goal state after:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ (D₂ ∪ D₁) = M ＼ (D₂ ∪ D₁)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
and_iff_left_of_imp Indep.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
I D : Set α
⊢ M.Indep I ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ (M ＼ D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D

Tactic:
rw [delete_eq_restrict, restrict_isCircuit_iff, and_congr_right_iff, subset_sdiff,
    and_iff_right_iff_imp]
  exact fun h _ ↦ h.subset_ground

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ s
⊢ x = ↑(↑l ⟨x, xs⟩ i)

Tactic:
rw [hs, Finset.mem_filter] at hi

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ l.idxFun i = none
⊢ x = ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α), ∀ C ⊆ M.E, M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
⊢ M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)

Tactic:
aux _ _ inter_subset_right,

Goal state after:
case inr
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α), ∀ C ⊆ M.E, M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
⊢ M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ (C ∩ M.E)) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D

Tactic:
rw [contract_delete_contract', sdiff_eq_left.mpr h]

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

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

Tactic:
delete_delete

Goal state after:
α : Type u_1
M : Matroid α
C D C' D' : Set α
⊢ M ／ (C ∪ C' \ D) ＼ (D ∪ D') = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
delete_delete

Goal state after:
α : Type u_1
M : Matroid α
D C D' : Set α
⊢ M ／ (C \ D) ＼ (D ∪ D') = M ／ (C \ D) ＼ (D ∪ D')
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
⊢ ∃ s, (∀ (i : σ), s i ∈ S i) ∧ (eval s) f ≠ 0

Tactic:
by_contra! Heval

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
⊢ False
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case pos
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
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_in_prefix : v ∈ pPrev.vertices
h_eq_end : v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
exact h_case₁ h_eq_end

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

Goal state before:
pp: case cons.inr
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
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_eq_end : v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
exact h_case₁ h_eq_end

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝓓 a 𝒜

Tactic:
by
  simp_rw [mem_compression, erase_idem, and_self_iff]
  refine (em _).imp_right fun h => ⟨h, ?_⟩
  rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)]

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

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
dsimp [f, hf]

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose (i + 1)))⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹

Tactic:
div_mul_cancel_right₀

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ (↑(card α) - ↑n)⁻¹ = (↑(card α) - ↑n)⁻¹

case hb
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ ↑((card α).choose n) ≠ 0
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : SemilatticeSup α
inst✝ : DecidableLE α
s t : Finset α
a : α
⊢ {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}

Tactic:
simp only [← coe_inj, coe_filter, coe_sups, ← mem_coe, Set.sep_sups_le]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
s t : Finset α
a : α
inst✝ : DecidableEq α
⊢ a ∈ upperClosure (↑s ∪ ↑t) ↔ a ∈ upperClosure ↑s ∨ a ∈ upperClosure ↑t

Tactic:
upperClosure_union,

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
s t : Finset α
a : α
inst✝ : DecidableEq α
⊢ a ∈ upperClosure ↑s ⊓ upperClosure ↑t ↔ a ∈ upperClosure ↑s ∨ a ∈ upperClosure ↑t
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a : α
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s

Tactic:
by
  rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
by
  rw [mem_shadow_iterate_iff_exists_card]
  constructor
  · rintro ⟨u, rfl, htu, hsuA⟩
    exact ⟨_, hsuA, subset_union_left, by rw [union_sdiff_cancel_left htu]⟩
  · rintro ⟨s, hs, hts, rfl⟩
    refine ⟨s \ t, rfl, disjoint_sdiff, ?_⟩
    rwa [union_sdiff_self_eq_union, union_eq_right.2 hts]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ #t = r - #(s \ t)

Tactic:
rw [card_sdiff_of_subset hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
⊢ (∃ a, Ici a = s) → InfIrred s

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
a : α
⊢ InfIrred (Ici a)
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ (∃ a, Iic a = s) → SupIrred s

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
a : α
⊢ SupIrred (Iic a)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    (↑(#((𝒜 ∪ ℬ).truncatedSup s)) + ↑(#((𝒜 ⊼ ℬ).truncatedSup s))) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
      (↑(#(𝒜.truncatedSup s)) + ↑(#(ℬ.truncatedSup s))) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))

Tactic:
← Nat.cast_add,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))
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 }
⊢ (fun a ↦ { carrier := {b | ↑b ≤ a}, lower' := ⋯ }) ((fun s ↦ (↑s).toFinset.sup Subtype.val) s) = s

Tactic:
by
        ext a
        dsimp
        refine ⟨fun ha ↦ ?_, fun ha ↦ ?_⟩
        · obtain ⟨i, hi, ha⟩ := a.2.supPrime.le_finset_sup.1 ha
          exact s.lower ha (Set.mem_toFinset.1 hi)
        · exact le_sup (Set.mem_toFinset.2 ha)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    (↑(#((𝒜 ∪ ℬ).truncatedInf s)) + ↑(#((𝒜 ⊻ ℬ).truncatedInf s))) / (↑(#s) * ↑((card α).choose #s)) =
      (↑(#(𝒜.truncatedInf s)) + ↑(#(ℬ.truncatedInf s))) / (↑(#s) * ↑((card α).choose #s))

Tactic:
← Nat.cast_add,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ ∑ i ∈ range (#s + 1), ↑((#s).choose i) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ∑ j ∈ range (#s + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t))

Tactic:
eq_comm

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ ∑ j ∈ range (#s + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ∑ i ∈ range (#s + 1), ↑((#s).choose i) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑i) * ↑((card α).choose i))
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : 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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
this : x ∉ u
⊢ u ⊆ s

Tactic:
rwa [← erase_eq_of_notMem ‹x ∉ u›, ← subset_insert_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ ↑s ∪ compl ⁻¹' ↑s = univ

Tactic:
refine eq_univ_of_forall fun a => ?_

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∪ compl ⁻¹' ↑s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
⊢ collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0

Tactic:
by
  rw [collapse, filter_collapse_eq ha]
  split_ifs <;> simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

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
⊢ ∀ (x : V), x ∈ G.support

Tactic:
intro v

Goal state after:
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
⊢ v ∈ G.support
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ ∀ (v w : V), (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w

Tactic:
intro v

Goal state after:
V : Type u
G : SimpleGraph V
v : V
⊢ ∀ (w : V), (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w
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✝
⊢ (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩

Tactic:
simpa using! hab

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

Goal state before:
pp: case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + #(A \ B) = #A

Tactic:
add_comm,

Goal state after:
case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #(A \ B) + #B = #A
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + i = r

Tactic:
rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Set.univ.Nonempty

Tactic:
rw [← Set.nonempty_iff_univ_nonempty]

Goal state after:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Nonempty (G.Walk u v)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
e : Sym2 V
he : G.IsBridge e
⊢ Nontrivial V

Tactic:
cases e with

Goal state after:
case h
V : Type u
G : SimpleGraph V
u v : V
he : G.IsBridge s(u, v)
⊢ Nontrivial V
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr
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) < #𝒜
⊢ False

Tactic:
have : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ) := disjoint_right.2 fun A hAbar hA ↦ by
    simp only [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
    obtain ⟨C, hC, hAC, _⟩ := hAbar
    exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)

Goal state after:
case inr
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] 𝒜ᶜˢ)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : completeGraph (Fin n) ↪g completeGraph ℕ := ⋯
⊢ ∀ (v : V), (f.toHom.comp C) v < n

Tactic:
intro v

Goal state after:
case h
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : completeGraph (Fin n) ↪g completeGraph ℕ := Embedding.completeGraph Fin.valEmbedding
v : V
⊢ (f.toHom.comp C) v < n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ ∀ {v w : V}, G.Adj v w → 0 ≠ 0

Tactic:
intro v

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v : V
⊢ ∀ {w : V}, G.Adj v w → 0 ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: 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
⊢ ∀ {v w : V ⊕ W}, (completeBipartiteGraph V W).Adj v w → v.isRight ≠ w.isRight

Tactic:
intro v

Goal state after:
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
v : V ⊕ W
⊢ ∀ {w : V ⊕ W}, (completeBipartiteGraph V W).Adj v w → v.isRight ≠ w.isRight
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
⊢ G.support ⊆ s ∪ t

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v : V
⊢ v ∈ G.support → v ∈ s ∪ t
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
w : V
⊢ w ∈ G.neighborFinset v ↔ w ∈ {w ∈ t | G.Adj v w}

Tactic:
mem_neighborFinset,

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
w : V
⊢ G.Adj v w ↔ w ∈ {w ∈ t | G.Adj v w}
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
v : V
⊢ v ∈ G.neighborFinset w ↔ v ∈ {v ∈ s | G.Adj v w}

Tactic:
mem_neighborFinset,

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
v : V
⊢ G.Adj w v ↔ v ∈ {v ∈ s | G.Adj v w}