mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.append q).support.Nodup
⊢ p.support.Disjoint q.tail.support

Tactic:
rw [support_append] at hpq'

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.tail.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n

Tactic:
classical
  refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
  push_cast
  exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : G.IsClique ↑t
⊢ #t ≤ G.cliqueNum

Tactic:
exact le_csSup G.finite_cliqueNum_bddAbove (Exists.intro t ⟨tc, rfl⟩)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.bypass.darts <+ p.darts

Tactic:
induction p with
  | nil => simp!
  | cons _ _ ih =>
    dsimp! only
    split_ifs
    · exact darts_dropUntil_suffix_darts .. |>.sublist.trans ih |>.cons _
    · simpa

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hp : (Walk.map f p).IsTrail ∧ ¬p.Nil ∧ (List.map (⇑f) p.support.tail).Nodup
⊢ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup

Tactic:
exact hp.imp .of_map <| .imp_right <| .of_map f

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
q : G.Walk u u
qc : q.IsCycle
hq : ∀ e ∈ q.edges, e ∈ H.edgeSet
⊢ (q.transfer H hq).IsCycle

Tactic:
by
  cases q with
  | nil => simp at qc
  | cons _ q =>
    simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq
    simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
    exact ⟨qc.1.transfer hq.2, qc.2⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case a
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ #G.edgeFinset ≤ (Fintype.card α).choose 2

Tactic:
exact card_edgeFinset_le_card_choose_two

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 ↦ (x, x_1))
          ({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
            match x with
            | (y, z) => G.Adj y z})))

Tactic:
rw [card_image_of_injective _ (Prod.mk_right_injective _)]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))
Module: Mathlib.Combinatorics.Additive.Randomisation

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) =
    ∑ t, (𝔼 a, ∏ ψ ∈ t, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, ↑(c ψ)

Tactic:
expect_mul,

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) =
    ∑ x, 𝔼 i, (∏ ψ ∈ x, (d ψ * ψ i + (starRingEnd ℂ) (d ψ * ψ i)) / 2) * ∏ ψ ∈ xᶜ, ↑(c ψ)
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
r : ℕ
⊢ Sized r ∅

Tactic:
by simp [Sized]

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

Goal state before:
pp: α : Type u_1
s : Finset α
r : ℕ
⊢ Sized r {s} ↔ #s = r

Tactic:
by simp [Sized]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
⊢ b < w

Tactic:
by_contra! hwb

Goal state after:
case inr.inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
hwb : w ≤ b
⊢ False
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v

Tactic:
induction v with | h v hv =>
  rw [cross_mk_of_cross_eq_zero]
  rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z * w⁻¹ = x⁻¹ * y

Tactic:
rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← hzxwy, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).1 < n + 1

Tactic:
have := fst_le ijh.2

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
this : (↑ijh).1 ≤ n
⊢ (↑ijh).1 < n + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ ([U] ++ ↑p).length

Tactic:
singleton_append,

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ (U :: ↑p).length
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D ([U] ++ List.take (i - 1) ↑p) < count U ([U] ++ List.take (i - 1) ↑p)

Tactic:
singleton_append,

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (U :: List.take (i - 1) ↑p) < count U (U :: List.take (i - 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: ⊢ Nat.bell 0 = 1

Tactic:
simp [Nat.bell]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x

Tactic:
mu_apply,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ (if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜) a x) = -∑ x ∈ Ico a b, (mu 𝕜) a x
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
    ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x

Tactic:
tsum_powMulProdOneSubPow _ hx hsum h,

Goal state after:
case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))

Tactic:
← sub_eq_iff_eq_add

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ (↑(n + 3) / 3 - 2) * ↑(rothNumberNat ((n + 3 - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat (n + 3))

Tactic:
calc
      _ ≤ (↑(2 * (n / 6) + 1) : ℝ) * rothNumberNat (n / 6) :=
        mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
      _ ≤ (ruzsaSzemerediNumberNat (6 * (n / 6) + 3) : ℝ) := ?_
      _ ≤ _ := by grw [Nat.mul_div_le]

Goal state after:
case calc_1
n : ℕ
⊢ ↑(n + 3) / 3 - 2 ≤ ↑(2 * (n / 6) + 1)

case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ G₁.IsLink e x y ↔ G₂.IsLink f x y

Tactic:
isLink_iff_inc,

Goal state after:
case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ (G₁.Inc e x ∧ G₁.Inc e y ∧ ∀ (z : α), G₁.Inc e z → z = x ∨ z = y) ↔ G₂.IsLink f x y
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ (G₁.Inc e x ∧ G₁.Inc e y ∧ ∀ (z : α), G₁.Inc e z → z = x ∨ z = y) ↔ G₂.IsLink f x y

Tactic:
isLink_iff_inc,

Goal state after:
case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ (G₁.Inc e x ∧ G₁.Inc e y ∧ ∀ (z : α), G₁.Inc e z → z = x ∨ z = y) ↔
    G₂.Inc f x ∧ G₂.Inc f y ∧ ∀ (z : α), G₂.Inc f z → z = x ∨ z = y
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x
x✝² : β
x✝¹ x✝ : α
⊢ G₁.IsLink x✝² x✝¹ x✝ ↔ G₂.IsLink x✝² x✝¹ x✝

Tactic:
isLink_iff_inc,

Goal state after:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x
x✝² : β
x✝¹ x✝ : α
⊢ (G₁.Inc x✝² x✝¹ ∧ G₁.Inc x✝² x✝ ∧ ∀ (z : α), G₁.Inc x✝² z → z = x✝¹ ∨ z = x✝) ↔
    G₂.Inc x✝² x✝¹ ∧ G₂.Inc x✝² x✝ ∧ ∀ (z : α), G₂.Inc x✝² z → z = x✝¹ ∨ z = x✝
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ M ↾ M.E \ D = M ↔ Disjoint D M.E

Tactic:
restrict_eq_self_iff,

Goal state after:
α : Type u_1
M : Matroid α
D : Set α
⊢ M.E \ D = M.E ↔ Disjoint D M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M.E \ (M ＼ (D₁ ∩ M.E)).E = M.E \ (M ＼ (D₂ ∩ M.E)).E
⊢ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
simp_rw [delete_ground, sdiff_sdiff_cancel_left inter_subset_right] at h

Goal state after:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ D₁ ∩ M.E = D₂ ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
⊢ M.IsBase B ∧ Disjoint B D

pp: case refine_2
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ M.IsBasis B (M.E \ D)

Tactic:
· have hss := h.subset
    rw [subset_sdiff] at hss
    have hcl := h.isBasis_closure_right
    rw [hD.closure_compl, isBasis_ground_iff] at hcl
    exact ⟨hcl, hss.2⟩

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ M.IsBasis B (M.E \ D)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_3
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
⊢ ∀
    p ∈
      { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ::ₘ
        Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines,
    ↑p.line none = Sum.elim s.focus (↑(map some l') none)

Tactic:
simp_rw [Multiset.mem_cons, Multiset.mem_map]
      rintro _ (rfl | ⟨q, hq, rfl⟩)
      · simp only [vertical_apply]
      · simp only [prod_apply, s.is_focused q hq]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
h' : M.Indep (I ∪ J) → (M ／ C).IsBasis I X
⊢ (M ／ C).IsBasis I X

Tactic:
imp_iff_right h_ind

Goal state after:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
h' : (M ／ C).IsBasis I X
⊢ (M ／ C).IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M ＼ D).IsCocircuit (K \ D)

Tactic:
rw [isCocircuit_def, dual_delete]
  exact hK.isCircuit.contract_isCircuit hD

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

Goal state before:
pp: case succ
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)

Tactic:
by_cases hc_in_S : c ∈ S

Goal state after:
case pos
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)

case neg
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : ¬c ∈ S
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℕ
hx : x ∈ {0}ᶜ
⊢ x ∉ A → schnirelmannDensity A < 1

Tactic:
hx'

Goal state after:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℕ
hx : x ∈ {0}ᶜ
hx' : x ∉ A
⊢ schnirelmannDensity A < 1
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))
⊢ ∑ x ∈ range (card α + 1), ↑(card α) * ↑((card α).choose x) / ((↑(card α) - ↑x) * ↑((card α).choose x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
← mul_div

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))
⊢ ∑ x ∈ range (card α + 1), ↑(card α) * (↑((card α).choose x) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Data.Finset.Sups

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

Tactic:
simp only [← coe_inj, coe_filter, coe_infs, ← mem_coe, Set.sep_infs_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ (if h : a ∈ upperClosure ↑s then e ({b ∈ s | b ≤ a}.inf' ⋯ id) else e ⊥) =
    if h : e a ∈ upperClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id else ⊥

Tactic:
map_finset_inf',

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ (if h : a ∈ upperClosure ↑s then {b ∈ s | b ≤ a}.inf' ⋯ (⇑e ∘ id) else e ⊥) =
    if h : e a ∈ upperClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id else ⊥
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : a = b \ v ⊔ v
⊢ a = b

Tactic:
sdiff_sup_cancel hb.2

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : a = b
⊢ a = b
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
⊢ birkhoffSet a = ↑(OrderIso.lowerSetSupIrred a)

Tactic:
have : Subsingleton (OrderBot α) := inferInstance

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
this : Subsingleton (OrderBot α)
⊢ birkhoffSet a = ↑(OrderIso.lowerSetSupIrred a)
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
ha : ⊥ ∉ ↑s ∧ ⊥ᶜ ∉ ↑s
⊢ (↑{⊤}).Intersecting

Tactic:
rw [coe_singleton]

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
ha : ⊥ ∉ ↑s ∧ ⊥ᶜ ∉ ↑s
⊢ {⊤}.Intersecting