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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (↑(Finset.map f s) ∩ ↑(Finset.map f t)).Subsingleton

Tactic:
← coe_inter,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (↑(Finset.map f s ∩ Finset.map f t)).Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique ↑(insert a s)

Tactic:
push_cast
    exact hs.1.insert fun b hb _ => h _ hb

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
hv : v ∈ (p.takeUntil w hw).support
⊢ False

Tactic:
rw [Walk.mem_support_iff_exists_getVert] at hv

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
hv : ∃ n, (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.append q).support.tail.Nodup

Tactic:
tail_support_append,

Goal state after:
case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.support.tail ++ q.support.tail).Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
x✝ : ℕ
hs : p.length = x✝
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
induction hs : p.length using Nat.strongRec generalizing u v with

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ⊆ t
hc : ¬t ⊆ ↑s
fint : Fintype ↑t
a : s = t.toFinset
⊢ False

Tactic:
subst a; simp_all[Set.coe_toFinset, not_true_eq_false]

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u✝ hs).IsPath

Tactic:
exact ih.dropUntil hs

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
⊢ ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j = a ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j

Tactic:
by
      rw [Equiv.subtypeEquivCodomain_symm_apply_eq]

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
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
⊢ Disjoint (insert 0 A) (a +ᵥ A.subsetSum)

Tactic:
have := nonneg_of_mem_subsetSum (fun y hy ↦ (hA y hy).le)

Goal state after:
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
this : ∀ x ∈ A.subsetSum, 0 ≤ x
⊢ Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ toColex (cons a s ha) ≤ toColex (insert b s) ↔ a ≤ b

Tactic:
← cons_eq_insert _ _ hb,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ toColex (cons a s ha) < toColex (insert b s) ↔ a < b

Tactic:
← cons_eq_insert _ _ hb,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ toColex (cons a s ha) < toColex (cons b s hb) ↔ a < b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s t : Finset α
hf : StrictMono f
⊢ toColex (image f s) ≤ toColex (image f t) ↔ toColex s ≤ toColex t

Tactic:
simp [toColex_le_toColex, hf.le_iff_le, hf.injective.eq_iff]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ i ∈ s, pointCount P i.2

Tactic:
s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l },

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ c, ∑ a ∈ {p | p ∈ c}.toFinset, pointCount P (a, c).2

case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
step3 : ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, lineCount L i.1 = ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, pointCount P i.2
i : P × L
hi : i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset
⊢ i.1 ∉ i.2

Tactic:
exact Set.mem_toFinset.mp hi

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : A.rank + Bᵀ.rank ≤ Fintype.card (Fin 3)
⊢ False

Tactic:
rank_transpose,

Goal state after:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : A.rank + B.rank ≤ Fintype.card (Fin 3)
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i ∈ range d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
sum_range_sub,

Goal state after:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ gosperCatalan (d + 1) d.succ - gosperCatalan (d + 1) 0 = ↑d.succ.centralBinom / (↑d.succ + 1)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
⊢ U :: (↑p).dropLast.tail ++ [D] = ↑p

Tactic:
have : p.toList.dropLast.take 1 = [p.toList.head h'] := by
    rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
    · tauto
    · rename_i bal _
      cases s <;> simp at bal
    · tauto

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = ↑p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U])

Tactic:
take_of_length_le (show [U].length ≤ i by rwa [length_singleton]),

Goal state after:
case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D [U] ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U [U]
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, f z = ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, (zeta 𝕜) y z * f z

Tactic:
by
      congr with y
      rw [sum_congr rfl fun z hz ↦ ?_]
      rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]

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

Goal state before:
pp: case tail
p q b✝ c✝ : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p b✝
mq : b✝ = c✝.insidePart ∨ b✝ = c✝.outsidePart
ih : ↑p <:+: ↑b✝
⊢ ↑p <:+: ↑c✝

Tactic:
rename_i m r

Goal state after:
case tail
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
⊢ ↑p <:+: ↑r
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ (1 - K) * ↑(#A) ≤ expansion K S A

Tactic:
by
  rw [one_sub_mul, expansion]; have := card_le_card_mul_right hS (s := A); gcongr

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

Goal state before:
pp: n : ℕ
⊢ n.stirlingFirst n = 1

Tactic:
by
  induction n <;> simp only [*, stirlingFirst, stirlingFirst_eq_zero_of_lt (Nat.lt_succ_self _),
    mul_zero]

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

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

Tactic:
ih

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

Goal state before:
pp: case refine_1
⊢ Nat.cast =O[atTop] fun n ↦ ↑n / 3 - 2

Tactic:
trans fun n ↦ n / 3

Goal state after:
⊢ Nat.cast =O[atTop] fun n ↦ ↑n / 3

⊢ (fun n ↦ ↑n / 3) =O[atTop] fun n ↦ ↑n / 3 - 2
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case refine_2
⊢ IsBigOWith 12 atTop Nat.cast fun n ↦ ↑((n - 3) / 6)

Tactic:
simp only [IsBigOWith, norm_natCast, eventually_atTop]

Goal state after:
case refine_2
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ↑b ≤ 12 * ↑((b - 3) / 6)
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
hHG.isLink_iff he

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

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

Tactic:
hHG.isLink_iff he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
⊢ (∃ y, y ≠ x ∧ H.IsLink e x y) ↔ ∃ y, y ≠ x ∧ G.IsLink e x y

Tactic:
hHG.isLink_iff he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
⊢ K ≤ H

Tactic:
by
  refine (Compatible.of_le_le h' h.le).le_iff.mpr ⟨hsu, fun e he ↦ ?_⟩
  obtain ⟨u, v, huv⟩ := K.exists_isLink_of_mem_edgeSet he
  exact h.2 (huv.mono h') (hsu huv.left_mem) (hsu huv.right_mem) |>.edge_mem

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

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
x' : α
hx' : G.IsLink e x' x'
h : ∀ (z : α), G.Inc e z → z = x' ∨ z = y
hy' : G.IsLink e y x'
⊢ G.IsLink e x' y

Tactic:
exact hy'.symm

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Tactic:
by
  induction hm with
  | head' a => exact ⟨1, fun m hm => FP.cons a m hm⟩
  | tail' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    exact FP.tail _ _ (hn _ hm')
  | cons' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    rw [mul_assoc]
    exact FP.cons _ _ (hn _ hm')

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)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ a_1 ∈ FP (Stream'.drop (n + 1) a), a_1 ∈ FP (Stream'.drop n a)

Tactic:
rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]

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)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ a_1 ∈ FP (Stream'.drop n a).tail, a_1 ∈ FP (Stream'.drop n a)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
rw [← delete_inter_ground_eq, ← M.delete_inter_ground_eq D₂]
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  apply_fun (M.E \ Matroid.E ·) at h
  simp_rw [delete_ground, sdiff_sdiff_cancel_left inter_subset_right] at h
  assumption

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)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
⊢ I ⊆ univ.sigma Bs

Tactic:
rw [← univ_sigma_preimage_mk I]

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)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' I) ⊆ univ.sigma Bs
Module: Mathlib.Combinatorics.Matroid.Sum

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

Tactic:
rw [← univ_sigma_preimage_mk I]

Goal state after:
case h.refine_1
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' I) ⊆ univ.sigma Js
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : 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
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (⋯.unit⁻¹ • f)) = m.toSyn (m.degree f)

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq]

Goal state after:
case pos
σ : 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
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.degree (⋯.unit⁻¹ • f) = m.degree f
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 \ C)
⊢ (M ／ C).IsBasis I X

Tactic:
hdj.sdiff_eq_right,

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.Indep (I ∪ J) → (M ／ C).IsBasis I X
⊢ (M ／ C).IsBasis I X
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
q : Path r b✝
β : Type ?u.4
⊢ p.cons e = q.cons e

Tactic:
ih

Goal state after:
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
q : Path r b✝
β : Type ?u.4
⊢ Path.cons ?cons.cons✝ e = q.cons e

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
q : Path r b✝
β : Type ?u.4
⊢ Path r b✝
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case e_t
α : 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
h : a ∈ upperClosure ↑s
⊢ {b ∈ s | b ≤ a}.inf' ⋯ (⇑e ∘ id) = {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id

Tactic:
simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv,
    OrderIso.le_iff_le, id, inf'_map]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ u ≤ a

Tactic:
· cases ne_of_mem_of_not_mem hb ha hba

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ Disjoint v a

Tactic:
· cases ne_of_mem_of_not_mem hb ha hba

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

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

Tactic:
card_truncatedSup_union_add_card_truncatedSup_infs

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True
Module: Mathlib.Order.Birkhoff

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

Tactic:
have := Fintype.toOrderBot α

Goal state after:
case neg
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : Nonempty α
this : OrderBot α
⊢ α ↪o Set { a // SupIrred a }
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ ((b ⊔ u) \ v ⊔ v) \ u ∈ s

Tactic:
sdiff_sup_cancel (le_sup_of_le_left h.2),

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ (b ⊔ u) \ u ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ (a ⊔ v) \ u ∈ s

Tactic:
· cases ne_of_mem_of_not_mem hb ha hba

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ x ≤ 𝒜.vcDim, #(powersetCard x univ)

Tactic:
refine (card_le_card fun s hs ↦ mem_biUnion.2 ⟨#s, ?_⟩).trans card_biUnion_le

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ #s ∈ Iic 𝒜.vcDim ∧ s ∈ powersetCard (#s) univ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Connected ∨ Gᶜ.Preconnected

Tactic:
rw [or_iff_not_imp_left, G.connected_iff_exists_forall_reachable]

Goal state after:
V : Type u
G : SimpleGraph V
⊢ (¬∃ v, ∀ (w : V), G.Reachable v w) → Gᶜ.Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(w, v) ∉ (↑p.toPath).edges

Tactic:
Sym2.eq_swap

Goal state after:
case mp.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∉ (↑p.toPath).edges