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

Goal state before:
pp: case refine_1
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
fst✝¹ : Finset V
snd✝¹ : V → V → Bool
property✝¹ :
  (∀ (a b : V), (fst✝¹, snd✝¹).2 a b = true → G.Adj a b) ∧
    (∀ (a b : V), (fst✝¹, snd✝¹).2 a b = true → a ∈ (fst✝¹, snd✝¹).1) ∧
      ∀ (a b : V), (fst✝¹, snd✝¹).2 a b = (fst✝¹, snd✝¹).2 b a
fst✝ : Finset V
snd✝ : V → V → Bool
property✝ :
  (∀ (a b : V), (fst✝, snd✝).2 a b = true → G.Adj a b) ∧
    (∀ (a b : V), (fst✝, snd✝).2 a b = true → a ∈ (fst✝, snd✝).1) ∧ ∀ (a b : V), (fst✝, snd✝).2 a b = (fst✝, snd✝).2 b a
⊢ (fun H ↦ { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ })
        ⟨(fst✝¹, snd✝¹), property✝¹⟩ =
      (fun H ↦ { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ })
        ⟨(fst✝, snd✝), property✝⟩ →
    ⟨(fst✝¹, snd✝¹), property✝¹⟩ = ⟨(fst✝, snd✝), property✝⟩

Tactic:
simp [funext_iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G'.degree v ≤ G.degree v

Tactic:
rw [← card_neighborSet_eq_degree]

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G'.degree v ≤ Fintype.card ↑(G.neighborSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : ↑G'.verts
inst✝¹ : Fintype ↑(G'.coe.neighborSet v)
inst✝ : Fintype ↑(G'.neighborSet ↑v)
⊢ G'.coe.degree v = G'.degree ↑v

Tactic:
rw [← card_neighborSet_eq_degree]

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : ↑G'.verts
inst✝¹ : Fintype ↑(G'.coe.neighborSet v)
inst✝ : Fintype ↑(G'.neighborSet ↑v)
⊢ Fintype.card ↑(G'.coe.neighborSet v) = G'.degree ↑v
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ (cons h p').darts
⊢ d.toProd.1 ∈ (cons h p').support

Tactic:
by
    simp only [support_cons, darts_cons, List.mem_cons] at hd ⊢
    rcases hd with rfl | hd
    · exact .inl rfl
    · exact .inr (dart_fst_mem_support_of_mem_darts _ hd)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk v✝ w), (p✝.reverseAux q).append r = p✝.reverseAux (q.append r)
q : G.Walk u✝ w
⊢ ((cons h p✝).reverseAux q).append r = (cons h p✝).reverseAux (q.append r)

Tactic:
simp [ih (cons h.symm q)]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ u ∈ p.support

Tactic:
by subst_vars; exact h

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).support <+: p.support

Tactic:
takeUntil_eq_take,

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ ((p.take (List.idxOf u p.support)).copy ⋯ ⋯).support <+: p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).darts <+: p.darts

Tactic:
takeUntil_eq_take,

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ ((p.take (List.idxOf u p.support)).copy ⋯ ⋯).darts <+: p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate u h).Nil ↔ c.Nil

Tactic:
simp [← length_eq_zero_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support ↔ ∃ n, p.getVert n = u ∧ n ≤ p.length

Tactic:
classical
  exact Iff.intro
    (fun h ↦ ⟨_, p.getVert_length_takeUntil h, p.length_takeUntil_le_length h⟩)
    (fun ⟨_, h, _⟩ ↦ h ▸ getVert_mem_support _ _)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
⊢ p.support[k]? = q.support[k]?

Tactic:
rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]
    exact congrArg some (h k hk)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ t, G.IsNClique n t
⊢ completeGraph (Fin n) ↪g G

Tactic:
apply Embedding.induce (h.choose : Set α) |>.comp

Goal state after:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ t, G.IsNClique n t
⊢ completeGraph (Fin n) ↪g induce (↑h.choose) G
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case ind
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
by_cases! hw : ∃ w, w ∈ p.support ∧ w ∈ q.support ∧ w ≠ u ∧ w ≠ v
  · classical
    have ⟨w, hwp, hwq, hwu, hwv⟩ := hw
    by_cases! p.takeUntil w hwp ≠ q.takeUntil w hwq
    · have := ih _ (hs ▸ length_takeUntil_lt_length hwp hwv) (hp.takeUntil hwp) (hq.takeUntil hwq)
      grind [isSubwalk_takeUntil, IsSubwalk.trans]
    · have := ih _ (hs ▸ length_dropUntil_lt_length hwp hwu) (hp.dropUntil hwp) (hq.dropUntil hwq)
        <| by grind [take_spec]
      grind [isSubwalk_dropUntil, IsSubwalk.trans]
  · refine ⟨u, v, p, q, p.isSubwalk_rfl, q.isSubwalk_rfl, ?_⟩
    refine hp.isCycle_append (isPath_reverse_iff q |>.mpr hq) (fun _ ↦ ?_) ?_
    · grind [dropLast_support_concat, IsPath.support_nodup, support_reverse, cons_tail_support]
    · grind [length_reverse, eq_of_length_le_one]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v✝ w v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
by subst_vars; exact h

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 ≤ σₘ[A, B]

Tactic:
by
  rw [mulConst, one_le_div₀]
  · exact mod_cast card_le_card_mul_right hB
  · simpa

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ (#A).choose 2 ≤ (#(A.erase 0) + 1).choose 2

Tactic:
tsub_le_iff_right.1 <| pred_card_le_card_erase

Goal state after:
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ (#(A.erase ?m.107) + 1).choose 2 ≤ (#(A.erase 0) + 1).choose 2

M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ M
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t

Tactic:
simpa using toColex_sdiff_le_toColex_sdiff (inter_subset_left (s₁ := s)) inter_subset_right

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
⊢ LinearIndependent K ![D.rep, D'.rep] ↔ D ≠ D'

Tactic:
LinearIndependent.pair_iff' (rep_nonzero _)

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
⊢ (∀ (a : K), a • D.rep ≠ D'.rep) ↔ D ≠ D'
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ ↑(numDerangements (n + 1 + 1)) = (↑(n + 1) + 1) * ↑(numDerangements (n + 1)) - (-1) ^ (n + 1)

Tactic:
simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
    ring

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
have := fintypeOfNotInfinite hf

Goal state after:
case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x✝ y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
⊢ x ∈ ↑A⁻¹ * ↑A → x⁻¹ ∈ ↑A⁻¹ * ↑A

Tactic:
simp only [Set.mem_mul, Set.mem_inv, coe_inv, forall_exists_index, mem_coe,
      and_imp]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x✝ y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
⊢ ∀ (x_1 : G), x_1⁻¹ ∈ A → ∀ x_2 ∈ A, x_1 * x_2 = x → ∃ x_3, x_3⁻¹ ∈ A ∧ ∃ y ∈ A, x_3 * y = x⁻¹
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Tactic:
exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

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
a : G
ha : a ∈ A
⊢ A ⊆ a •> (A⁻¹ * A)

Tactic:
rw [← smul_mul_assoc]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> A⁻¹ * A
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ (↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head
      h =
    U

Tactic:
head_cons

Goal state after:
case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ s = U
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
b : ℕ
| if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else (∑' (j : ℕ), (X ^ (b + 1)) ^ j) * (1 - X ^ (b + 1))

Tactic:
tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
b : ℕ
| if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n k : ℕ
⊢ (n + 1).stirlingFirst (k + 1) = n * n.stirlingFirst (k + 1) + n.stirlingFirst k

Tactic:
by
  rfl

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

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
⊢ (n + 1 + 1).stirlingSecond 1 = 1

Tactic:
stirlingSecond,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
⊢ (0 + 1) * (n + 1).stirlingSecond (0 + 1) + (n + 1).stirlingSecond 0 = 1
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
refine ⟨fun hin ↦ ?_, fun hin ↦ ?_⟩
  on_goal 2 => rw [isLink_comm] at he
  all_goals rw [← hHG.isLink_congr hin] at he; exact he.right_mem

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 : 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
⊢ (fun x ↦ x * m) '' N ⊆ N

Tactic:
rintro _ ⟨m', hm', rfl⟩

Goal state after:
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
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl.inl
η : 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
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : α
hm : m.idxFun i = Sum.inl val✝
⊢ Sum.inl a = Sum.inl val✝

Tactic:
simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl.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
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : η
hm : m.idxFun i = Sum.inr val✝
⊢ Sum.inl a = Sum.inr val✝

Tactic:
simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i

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

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

Tactic:
by
  rw [dep_iff, dep_iff, delete_indep_iff, delete_ground, subset_sdiff]; tauto

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

Goal state before:
pp: α : Type u_1
M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ ≤m M₃

Tactic:
exact ⟨C₂ ∪ C₁ \ D₂, D₂ ∪ D₁, by rw [contract_delete_contract_delete']⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) ↔ ∃ B, (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) ∧ I ⊆ B

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨B, hB, hIB⟩ i ↦ (hB i).indep.subset (preimage_mono hIB)⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
⊢ ∃ B, (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) ∧ I ⊆ B
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finitary
J : Set α
hJ : M.IsBasis' J C
⊢ (M ／ C).Finitary

Tactic:
suffices (M ／ J).Finitary by
    rw [hJ.contract_eq_contract_delete]
    infer_instance

Goal state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finitary
J : Set α
hJ : M.IsBasis' J C
⊢ (M ／ J).Finitary
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma M).Indep J
⊢ (Matroid.sigma M).Indep I

Tactic:
simp only [sigma_indep_iff] at hI ⊢

Goal state after:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
⊢ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
⊢ ¬m.degree (b i) ≤ c

Tactic:
convert! hf i

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
⊢ c = m.degree f
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] < f ![r 0, r 1]

Tactic:
apply lt_of_le_of_ne (mcf.right (r 0) (r 1)).left

Goal state after:
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] ≠ f ![r 0, r 1]
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case cons.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝¹ c✝ : V
p : Path r b✝¹
e : b✝¹ ⟶ c✝
ih : ∀ (q : Path r b✝¹), p = q
b✝ : V
q : Path r b✝
f : b✝ ⟶ c✝
⊢ p.cons e = q.cons f

Tactic:
rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
          rw [ih]

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

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
a b b✝ c✝ : Symmetrify V
q : Path a b✝
e : b✝ ⟶ c✝
ih : Nonempty (Path a b✝)
⊢ Nonempty (Path a c✝)

Tactic:
| cons q e ih =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ

Tactic:
simp_rw [memberSubfamily, filter_union, image_union]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b : α
hb : b ∈ ↑s
hba : b ≤ a
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a

Tactic:
exact hba.trans' <| inf'_le id <| mem_filter.2 ⟨hb, ‹_›⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 ↦ x1 ⊓ x2) ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b})).sup' ⋯ fun x ↦ id x) =
    ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun i ↦ id i.1 ⊓ id i.2

Tactic:
sup'_image

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ ((fun x ↦ id x) ∘ Function.uncurry fun x1 x2 ↦ x1 ⊓ x2) =
    ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun i ↦ id i.1 ⊓ id i.2
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupPrime ⊥
⊢ False

Tactic:
exact not_supPrime_bot ha

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

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

Tactic:
induction k generalizing 𝒜 s with
  | zero =>
    refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩
    rintro ⟨t, ht, hst, hcard⟩
    rwa [← eq_of_subset_of_card_le hst hcard.ge]
  | succ k ih =>
    simp only [Function.comp_apply, Function.iterate_succ]
    refine ih.trans ?_
    clear ih
    constructor
    · rintro ⟨t, ht, hts, hcardst⟩
      obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
      refine ⟨u, hu, hut.trans hts, ?_⟩
      rw [← hcardst, hcardtu, add_right_comm]
      rfl
    · rintro ⟨t, ht, hts, hcard⟩
      obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1)
        (by lia)
      refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
      rw [hu, ← hcard, add_right_comm]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ 2 * #s ≤ Fintype.card α

Tactic:
refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_
  rw [Nat.two_mul, card_disjUnion, card_map]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t

Tactic:
rw [zero_add]

Goal state after: