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

Goal state before:
pp: p✝ q✝ : DyckWord
h : p✝ ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
⊢ p = q

Tactic:
have h₁ := infix_of_le pq

Goal state after:
p✝ q✝ : DyckWord
h : p✝ ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
h₁ : ↑p <:+: ↑q
⊢ p = q
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
e : β
⊢ e ∈ E(H) → e ∈ E(G)

Tactic:
he

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
e : β
he : e ∈ E(H)
⊢ e ∈ E(G)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsLoopAt G.IsLoopAt E(H)

Tactic:
rintro e he
  ext x
  exact hHG.isLoopAt_congr he

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ ∀ ⦃e : β⦄, e ∈ E → Std.Symm (G.IsLink e)

Tactic:
by simpa [show E = E(G) by simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]]
      using G.isLink_symm

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ V(G.deleteVerts X) = V(G) \ X

Tactic:
unfold deleteVerts
  rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case hts
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x ↦ x * m) m' ∈ N

Tactic:
exact N_mul _ hm' _ hm

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
⊢ ∃ a b, (⟨a, b⟩ ∈ B₂ ∧ ⟨a, b⟩ ∉ B₁) ∧ ∀ (i_1 : ι), (M i_1).IsBase (Sigma.mk i_1 ⁻¹' insert ⟨a, b⟩ (B₁ \ {⟨i, e⟩}))

Tactic:
have hf_ex := (h₁ i).exchange (h₂ i) ⟨he₁, by simpa⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
hf_ex : ∃ y ∈ Sigma.mk i ⁻¹' B₂ \ Sigma.mk i ⁻¹' B₁, (M i).IsBase (insert y (Sigma.mk i ⁻¹' B₁ \ {e}))
⊢ ∃ a b, (⟨a, b⟩ ∈ B₂ ∧ ⟨a, b⟩ ∉ B₁) ∧ ∀ (i_1 : ι), (M i_1).IsBase (Sigma.mk i_1 ⁻¹' insert ⟨a, b⟩ (B₁ \ {⟨i, e⟩}))
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) X

Tactic:
by
  simpa [isBasis'_iff_isBasis_inter_ground, inter_sdiff_assoc, ← sdiff_inter_distrib_right] using
    (hIX.contract_isBasis'_sdiff_sdiff_of_subset hJI).isBasis_inter_ground

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ I \ C ∪ J ⊆ X \ C ∪ J

pp: case refine_2
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (I \ C ∪ J)

pp: case refine_3
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (I \ C) J

pp: case refine_4
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) J

pp: case refine_5
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) (C \ J)

Tactic:
rotate_left

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (I \ C ∪ J)

case refine_3
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (I \ C) J

case refine_4
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) J

case refine_5
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) (C \ J)

case refine_1
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ I \ C ∪ J ⊆ X \ C ∪ J
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I

Tactic:
have hJ' : M.IsBasis' J C := by
    simpa [inter_eq_self_of_subset_left subset_union_right] using (isBasis'_restrict_iff.1 hJ).1

Goal state after:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
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) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
⊢ ¬coeff e (Q.coeff m) = 0 → e i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
he

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
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: case zero
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = 0
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
obtain rfl := eq_of_length_zero p h_len

Goal state after:
case zero
V : Type u_1
inst✝ : Quiver V
a : V
S : Set V
ha_not_in_S : ¬a ∈ S
p : Path a a
hb_in_S : a ∈ S
h_len : p.length = 0
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
a✝ : i ∈ h.support
⊢ (eval x) (h i • Alon.P (S i) i) = 0

Tactic:
rw [smul_eq_mul, map_mul]

Goal state after:
case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
a✝ : i ∈ h.support
⊢ (eval x) (h i) * (eval x) (Alon.P (S i) i) = 0
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons.cons
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₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cast ⋯ hφy ((φ.mapPath p₁).cons (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
Path.cast_cons,

Goal state after:
case cons.cons
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₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (Path.cast ⋯ ⋯ (φ.mapPath p₁)).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩
Module: Mathlib.Order.Irreducible

Goal state before:
pp: case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : ¬SupIrred a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
rw [not_supIrred] at ha

Goal state after:
case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t u : Finset α
htu : Disjoint t u
hsuA : t ∪ u ∈ 𝒜
⊢ #((t ∪ u) \ t) = #u

Tactic:
union_sdiff_cancel_left htu

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t u : Finset α
htu : Disjoint t u
hsuA : t ∪ u ∈ 𝒜
⊢ #u = #u
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ #s + #(map { toFun := compl, inj' := ⋯ } s) = #s + #s

Tactic:
card_map

Goal state after:
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ #s + #s = #s + #s
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
this : s.disjUnion (map { toFun := compl, inj' := ⋯ } s) ⋯ = Finset.univ
⊢ #s + #s = #s + #(map { toFun := compl, inj' := ⋯ } s)

Tactic:
card_map

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
this : s.disjUnion (map { toFun := compl, inj' := ⋯ } s) ⋯ = Finset.univ
⊢ #s + #s = #s + #s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t u : Finset α
ha : a ∉ s
ht : t ∈ 𝒜
hu : u ∈ 𝒜
hts : t = s
hus : u = insert a s
⊢ collapse 𝒜 a f s = f t + f u

Tactic:
subst hts; subst hus; simp_rw [collapse_eq ha, if_pos ht, if_pos hu]

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

Goal state before:
pp: case refine_2
α : 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 ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)

Tactic:
rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]

Goal state after:
case refine_2
α : 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 ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ #(image (fun a ↦ insert a s) sᶜ)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤
    (f₃ (s ∩ t) + f₃ (insert a s ∩ insert a t)) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›)
        (union_mem_sups ‹_› ‹_›) rfl (insert_union_distrib _ _ _).symm

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤
    (f₃ (s ∩ t) + f₃ (insert a s ∩ insert a t)) * (f₄ (s ∪ t) + f₄ (insert a s ∪ insert a t))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
⊢ t ⊆ s → s ∈ ↑𝒜.shatterer → t ∈ ↑𝒜.shatterer

Tactic:
simpa using Shatters.mono_right

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ Disjoint ((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) ℬ

Tactic:
simp only [ℬ, disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ ∀ ⦃a_1 : Finset α⦄,
    (memberSubfamily a 𝒜).Shatters a_1 ∨ (nonMemberSubfamily a 𝒜).Shatters a_1 →
      ∀ x ∈ (memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer, ¬insert a x = a_1
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:
by
  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.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
hreach : G.Reachable u v
this : G.deleteEdges {s(u, v)} < G
⊢ s(u, v) ∈ G.edgeSet

Tactic:
grind [edgeSet_strict_mono this, edgeSet_deleteEdges]

Goal state after:
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:
by
  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: n : ℕ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree n
⊢ (completeMultipartiteGraph V).Colorable (n - 1)

Tactic:
by
  cases n with
  | zero => exact absurd hc not_cliqueFree_zero
  | succ n =>
  have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
  apply (coloring V).colorable.mono
  have := not_cliqueFree_of_le_card V f le_rfl
  contrapose! this
  exact hc.mono this

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s, G.degree v + ∑ v ∈ s, G.degree v = ∑ x ∈ s, G.degree x + ∑ x ∈ t, G.degree x

Tactic:
add_right_inj

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s, G.degree v = ∑ x ∈ t, G.degree x
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ Walk.map (cons h✝ w).toSubgraph.hom (cons ⋯ (Walk.map (Subgraph.inclusion ⋯) w.mapToSubgraph)) = cons h✝ w

Tactic:
Walk.map,

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ cons ⋯ (Walk.map (cons h✝ w).toSubgraph.hom (Walk.map (Subgraph.inclusion ⋯) w.mapToSubgraph)) = cons h✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ 0 < w.length

Tactic:
simp [hw]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ 1 < w.length

Tactic:
simp [hw]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.dist u v ≤ G.dist u v

Tactic:
obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_dist
  rw [← hw, ← Walk.length_map (.ofLE h)]
  apply dist_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G □ H).degree x = G.degree x.1 + H.degree x.2

Tactic:
rw [degree, degree, degree, neighborFinset_boxProd, Finset.card_disjUnion]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G.neighborFinset x.1 ×ˢ {x.2}).card + ({x.1} ×ˢ H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2.patches.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (hu' : u ∈ {x | x ∈ (Nonempty.some ⋯).support}) (hv' : v ∈ {x | x ∈ (Nonempty.some ⋯).support}),
    (induce {x | x ∈ (Nonempty.some ⋯).support} G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
simp only [Set.mem_ofPred_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩

Goal state after: