mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ∑ z ∈ S with (K - 1) * ↑(#A) < ↑(r z), ↑(#A) + ∑ z ∈ S with ↑(r z) ≤ (K - 1) * ↑(#A), (K - 1) * ↑(#A) =
    ↑l * ↑(#A) + (↑(#S) - ↑l) * (K - 1) * ↑(#A)

Tactic:
by
          simp [hk, ← not_lt, mul_assoc,
            ← S.card_filter_add_card_filter_not fun z ↦ (K - 1) * #A < r z]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
⊢ q ≤ p + q

Tactic:
by_cases h : p = 0

Goal state after:
case pos
p q : DyckWord
h : p = 0
⊢ q ≤ p + q

case neg
p q : DyckWord
h : ¬p = 0
⊢ q ≤ p + q
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ofTree p.toTree = p

Tactic:
by_cases h : p = 0

Goal state after:
case pos
p : DyckWord
h : p = 0
⊢ ofTree p.toTree = p

case neg
p : DyckWord
h : ¬p = 0
⊢ ofTree p.toTree = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.toTree.numNodes = p.semilength

Tactic:
by_cases h : p = 0

Goal state after:
case pos
p : DyckWord
h : p = 0
⊢ p.toTree.numNodes = p.semilength

case neg
p : DyckWord
h : ¬p = 0
⊢ p.toTree.numNodes = p.semilength
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: k : ℤ
⊢ 2 * ↑(pentagonal k) = k * (3 * k - 1)

Tactic:
by
  rw [natCast_pentagonal]
  exact Int.two_mul_ediv_two_of_even (by grind)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    (coeff (p.toFinsuppAntidiag i)) 1 +
      ∑' (i_1 : ℕ), (coeff (p.toFinsuppAntidiag i)) (f i (i_1 + 1) • X ^ (i * (i_1 + 1)))

Tactic:
suffices f i (Multiset.count i p.parts) =
        ∑' j, if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0 by
      simpa [toFinsuppAntidiag, hi, hi0, coeff_X_pow]

Goal state after:
case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingFirst n = (n + 1).choose 2

Tactic:
by
  induction n with
  | zero => simp only [zero_add, stirlingFirst_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)

Tactic:
rw [isLink_comm] at he

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : G.Compatible H
⊢ E(G ⊓ H) = E(G) ∩ E(H)

Tactic:
rw [G.edgeSet_inf]

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
h : G.Compatible H
⊢ {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} = E(G) ∩ E(H)
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: 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 * m = m

Tactic:
use m

Goal state after:
case h
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 : 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 = m
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case ht
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
m' : M
hm' : m' ∈ N
⊢ (fun x ↦ x * m) m'' * (fun x ↦ x * m) m' ∈ (fun x ↦ x * m) '' N

Tactic:
exact ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩

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

Goal state before:
pp: case refine_1.inr.convert_2
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), (↑i).Nonempty

pp: case refine_1.inr.convert_3
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsCompact ↑i

pp: case refine_1.inr.convert_4
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsClosed ↑i

Tactic:
exacts [fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
⊢ Sum.inr e = m.idxFun i

Tactic:
cases hm : idxFun m i with
    | inl a =>
      obtain ⟨b, hba⟩ := exists_ne a
      simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
    | inr f =>
      obtain ⟨a, b, hab⟩ := exists_pair_ne α
      simp only [Sum.inr.injEq]
      by_contra! hef
      simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)

Tactic:
obtain ⟨n', hn⟩ := FP.mul hm

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
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₂
⊢ ∀ (a : ι) (b : α a),
    ⟨a, b⟩ ∈ B₁ →
      ⟨a, b⟩ ∉ B₂ →
        ∃ a_3 b_1,
          (⟨a_3, b_1⟩ ∈ B₂ ∧ ⟨a_3, b_1⟩ ∉ B₁) ∧
            ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' insert ⟨a_3, b_1⟩ (B₁ \ {⟨a, b⟩}))

Tactic:
intro i e he₁ he₂

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₂
⊢ ∃ 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.Sum

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ I₀ ⊆ Sigma.mk i ⁻¹' I ∪ I₀

Tactic:
exact subset_union_right

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case e'_3
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 : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : n ∈ P.support
hn : n none = m ∧ n.some = e
⊢ e i = n (Option.some i)

Tactic:
rw [← hn.2, some_apply]

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

Goal state before:
pp: case nil
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
hp : shortestPath r r = Path.nil
⊢ r = r ∨ ∃ a, Nonempty (a ⟶ r)

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Tactic:
obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩

Goal state after:
case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.star u' ⟨u'', eu⟩ = ⟨c✝, ev⟩
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ {b ∈ s | a ≤ b}.sup' ⋯ id ≤ a

Tactic:
sup'_le_iff,

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ ∀ b ∈ {b ∈ s | a ≤ b}, id b ≤ a
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∉ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (s ∪ t).truncatedSup a = t.truncatedSup a

Tactic:
by rw [union_comm, truncatedSup_union_left ht hs]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
a b : α
h : Disjoint a b
⊢ {a} ○ {b} = {a ⊔ b}

Tactic:
simp [disjSups, filter_singleton, h]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
a b : α
h : ¬Disjoint a b
⊢ {a} ○ {b} = ∅

Tactic:
simp [disjSups, filter_singleton, h]

Goal state after:
Module: Mathlib.Order.Irreducible

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

Tactic:
by simp_rw [← inf_eq_left, inf_sup_left]; exact @h _ _

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case pos
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : IsEmpty α
⊢ α ↪o Set { a // SupIrred a }

Tactic:
exact OrderEmbedding.ofIsEmpty

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #𝒜 * #ℬ ≤ 2 ^ #(insert a s) * #(𝒜 ∩ ℬ)

Tactic:
rw [card_insert_of_notMem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ←
    card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add,
    add_comm (_ * _), add_add_add_comm]
  grw [mul_add_mul_le_mul_add_mul
    (card_le_card h𝒜.memberSubfamily_subset_nonMemberSubfamily) <|
      card_le_card hℬ.memberSubfamily_subset_nonMemberSubfamily, ← two_mul, pow_succ', mul_assoc]
  have h₀ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.nonMemberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_nonMemberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)
  have h₁ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.memberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_memberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)
  gcongr
  refine (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
    ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq ?_
  rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ 𝒜.vcDim ≤ ℬ.vcDim

Tactic:
unfold vcDim; gcongr

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ p, p.IsPath

Tactic:
obtain ⟨W⟩ := hr
  exact ⟨_, Path.isPath W.toPath⟩

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ hs.piecewise f ⁻¹' t
⊢ x ∈ ⋃ i, s i ∩ f i ⁻¹' t

Tactic:
rw [mem_preimage, piecewise_apply, ← mem_preimage] at hx

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ f (hs.index x) ⁻¹' t
⊢ x ∈ ⋃ i, s i ∩ f i ⁻¹' t
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''
u v : V
G : SimpleGraph V
e : Sym2 V
⊢ ∀ (a₁ a₂ : V),
    (fun v w ↦ ¬(G.deleteEdges {e}).Reachable v w) a₁ a₂ = (fun v w ↦ ¬(G.deleteEdges {e}).Reachable v w) a₂ a₁

Tactic:
simp [reachable_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
by
  cases nonempty_fintype V
  exact colorable_chromaticNumber G.colorable_of_fintype

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

Goal state before:
pp: V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ (completeBipartiteGraph V W).chromaticNumber = 2

Tactic:
← Nat.cast_two,

Goal state after:
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ (completeBipartiteGraph V W).chromaticNumber = ↑2
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
q : G.Walk v w
⊢ (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph

Tactic:
induction p <;> simp [*, sup_assoc]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
hc : 1 = G.dist u v
p : G.Walk u v
hp : p.length = G.dist u v
⊢ False

Tactic:
exact hnadj (Walk.exists_length_eq_one_iff.mp ⟨p, hc ▸ hp⟩)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
h₂ : p₂.IsSubwalk p₁
⊢ p₂.length = G.dist u' v'

Tactic:
refine (dist_le _).eq_of_not_lt' fun hh ↦ ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
h₂ : p₂.IsSubwalk p₁
hh : G.dist u' v' < p₂.length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
← huv,

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet u).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ y.1 ∈ G.neighborFinset x.1 ∧ y.2 ∈ {x.2} ∨ y.1 ∈ {x.1} ∧ y.2 ∈ H.neighborFinset x.2 ↔
    (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x

Tactic:
Finset.mem_singleton,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ y.1 ∈ G.neighborFinset x.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ y.2 ∈ H.neighborFinset x.2 ↔
    (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x
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
⊢ ¬(G ⊕g H).Reachable (Sum.inl v) (Sum.inr w)

Tactic:
rintro ⟨p⟩
  have hs : ∀ x : V ⊕ W, x ∉ Set.range .inl ↔ x ∈ Set.range .inr := by simp
  obtain ⟨⟨d, hadj⟩, _, hd1, hd2⟩ := p.exists_boundary_dart (Set.range .inl) (by simp) (by simp)
  simp only [hs] at hadj hd1 hd2
  obtain ⟨v', hv'⟩ := hd1
  obtain ⟨w', hw'⟩ := hd2
  rw [← hv', ← hw'] at hadj
  exact not_adj_sum_inl_inr _ _ hadj

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊔ H ⊔ K).Connected

Tactic:
by
  refine Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_
  · exact (top_induce_pair_connected_of_adj huv).preconnected
  · exact ⟨u, by simp [uH]⟩
  · exact ⟨v, by simp [vK]⟩

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

Goal state before:
pp: n : ℕ
⊢ (cycle n).tail.IsPath

Tactic:
refine isPath_iff_injective_get_support _ |>.mpr fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ ?_

Goal state after:
n : ℕ
x✝¹ x✝ : Fin (cycle n).tail.support.length
i : ℕ
hi : i < (cycle n).tail.support.length
j : ℕ
hj : j < (cycle n).tail.support.length
hij : (fun x ↦ (cycle n).tail.support.get x) ⟨i, hi⟩ = (fun x ↦ (cycle n).tail.support.get x) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ False

Tactic:
obtain ⟨e, he⟩ := c.edges.exists_mem_of_ne_nil <| by simp [hc.not_nil]

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
v : V
c : G.Walk v v
hc : c.IsCycle
e : Sym2 V
he : e ∈ c.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type ?u.21) → [Finite α] → Fintype α
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Tactic:
obtain ⟨T, hle, hT⟩ := h.exists_isTree_le

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type ?u.21) → [Finite α] → Fintype α
T : SimpleGraph V
hle : T ≤ G
hT : T.IsTree
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
h : G.IsTree
⊢ ∃ v, G.degree v = 1

Tactic:
by
  grind [G.exists_minimal_degree_vertex, minDegree_eq_one_of_nontrivial]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
v : V
⊢ (if u = t then if v = t then False else G.Adj s v else if v = t then G.Adj u s else G.Adj u v) ↔
    v ∈ G.neighborFinset u ∧ ¬v = t

Tactic:
split_ifs <;> simp_all [adj_comm]

Goal state after: