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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (Walk.map f p).support[↑i]
⊢ u = v

Tactic:
rw! [

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (Walk.map f p).support[↑i]
⊢ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : v = w
⊢ (c.takeUntil w h).IsPath

pp: case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
· subst hvw
    simp

Goal state after:
case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsNClique n s
⊢ G.IsNClique n (map { toFun := Subtype.val, inj' := ⋯ } s)

Tactic:
rw [isNClique_iff] at cc ⊢

Goal state after:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique ↑s ∧ #s = n
⊢ G.IsClique ↑(map { toFun := Subtype.val, inj' := ⋯ } s) ∧ #(map { toFun := Subtype.val, inj' := ⋯ } s) = n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
⊢ completeGraph (Fin n) ⊑ G

Tactic:
have e := @hφ x y

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : (G.replaceVertex s t).Adj (φ x) (φ y) ↔ (completeGraph (Fin n)).Adj x y
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∈ Set.range ⇑φ
⊢ completeGraph (Fin n) ⊑ G

Tactic:
obtain ⟨y, hy⟩ := ms
      have e := @hφ x y
      simp_rw [hx, hy, adj_comm, not_adj_replaceVertex_same, top_adj, false_iff, not_ne_iff] at e
      rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ Gᶜ.IsClique s ↔ G.IsIndepSet s

Tactic:
by
  rw [isIndepSet_iff, isClique_iff]; repeat rw [Set.Pairwise]
  simp_all [compl_adj]

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

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
⊢ #tris ≤ #G.edgeFinset - #H.edgeFinset

Tactic:
← card_sdiff_of_subset (edgeFinset_mono hHG),

Goal state after:
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
⊢ #tris ≤ #(G.edgeFinset \ H.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ Gᶜ.IsIndepSet s ↔ G.IsClique s

Tactic:
by
  rw [isIndepSet_iff, isClique_iff]; repeat rw [Set.Pairwise]
  simp_all [compl_adj]

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 : V
p : G.Walk u v
hp : (Walk.map f p).IsPath
⊢ p.IsPath

Tactic:
rw [isPath_def]

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsPath
⊢ p.support.Nodup
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
hinj : Injective ⇑f
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle

Tactic:
by
  rw [isCycle_def, isCycle_def, isTrail_map_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
qc : (cons h✝ q).IsCycle
hq✝ : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
hq : s(u, v✝) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
⊢ ((cons h✝ q).transfer H hq✝).IsCycle

Tactic:
simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
hq✝ : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
hq : s(u, v✝) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
qc : q.IsPath ∧ s(u, v✝) ∉ q.edges
⊢ (q.transfer H ⋯).IsPath ∧ s(u, v✝) ∉ q.edges
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_inv_right]
  apply one_le_mulConst hA (by 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_nonneg : ∀ x ∈ A, 0 ≤ x
⊢ ∀ x ∈ A.subsetSum, 0 ≤ x

Tactic:
simpa [mem_subsetSum_iff] using fun B hB ↦ Finset.sum_nonneg fun x hx ↦ A_nonneg _ <| hB hx

Goal state after:
Module: Mathlib.Combinatorics.Colex

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

Tactic:
obtain rfl | hab := eq_or_ne a b
  · simp
  classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]

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

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)

Tactic:
· rw [apply_symm_apply]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A)

pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ ↑A ⊆ a •> ↑H

pp: case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ a •> ↑H = ↑H <• a

Tactic:
· simp only [invMulSubgroup, ← coe_mul, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,
      mem_coe, ← Nat.card_eq_fintype_card, H]
    rwa [Nat.card_eq_finsetCard, card_inv_mul_of_doubling_lt_three_halves h]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ ↑A ⊆ a •> ↑H

case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ a •> ↑H = ↑H <• a
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

Tactic:
rw! [

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ 0 < (range (↑p).length).length

Tactic:
rw [length_range, length_pos_iff]

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ↑p ≠ []
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case pos
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a = b
h : ¬1 = 0
⊢ a ≤ b

Tactic:
exact hab.le

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell) =
    n.succ * ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell

Tactic:
Finset.mul_sum

Goal state after:
n : ℕ
p : (n + 1).Partition
⊢ ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell) =
    ∑ i ∈ p.parts.toFinset, n.succ * (n.choose (i - 1) * (p.parts.erase i).bell)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
pq : p < q
⊢ p.semilength < q.semilength

Tactic:
obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq
  apply lt_of_le_of_ne (monotone_semilength plq)
  contrapose pnq
  replace pnq := congr(2 * $(pnq))
  simp_rw [two_mul_semilength_eq_length] at pnq
  exact DyckWord.ext ((infix_of_le plq).eq_of_length pnq)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

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

Tactic:
by
  rcases k with (_ | _) | _ <;> grind [pentagonal_def]

Goal state after:
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:
rw [one_sub_mul, expansion]; have := card_le_card_mul_right hS (s := A); gcongr

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
vertexSet✝ : Set α
IsLink✝ : β → α → α → Prop
edgeSet✝ : Set β
isLink_symm✝ : ∀ ⦃e : β⦄, e ∈ edgeSet✝ → Std.Symm (IsLink✝ e)
eq_or_eq_of_isLink_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink✝ e x y → IsLink✝ e v w → x = v ∨ x = w
h : ∀ (e : β), e ∈ edgeSet✝ ↔ ∃ x y, IsLink✝ e x y
left_mem_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink✝ e x y → x ∈ vertexSet✝
hE :
  ∀ (e : β),
    e ∈
        E({ vertexSet := vertexSet✝, IsLink := IsLink✝, edgeSet := edgeSet✝, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink✝ }) ↔
      ∃ x y,
        { vertexSet := vertexSet✝, IsLink := IsLink✝, edgeSet := edgeSet✝, isLink_symm := isLink_symm✝,
              eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝, edge_mem_iff_exists_isLink := h,
              left_mem_of_isLink := left_mem_of_isLink✝ }.IsLink
          e x y
⊢ {
      vertexSet :=
        V({ vertexSet := vertexSet✝, IsLink := IsLink✝, edgeSet := edgeSet✝, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink✝ }),
      IsLink :=
        { vertexSet := vertexSet✝, IsLink := IsLink✝, edgeSet := edgeSet✝, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink✝ }.IsLink,
      edgeSet :=
        E({ vertexSet := vertexSet✝, IsLink := IsLink✝, edgeSet := edgeSet✝, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink✝ }),
      isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ } =
    { vertexSet := vertexSet✝, IsLink := IsLink✝, edgeSet := edgeSet✝, isLink_symm := isLink_symm✝,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝, edge_mem_iff_exists_isLink := h,
      left_mem_of_isLink := left_mem_of_isLink✝ }

Tactic:
| _ _ _ _ _ _ h _ =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.IsNonloopAt e x
⊢ H.IsNonloopAt e x

Tactic:
obtain ⟨y, hne, hy⟩ := h

Goal state after:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
y : α
hne : y ≠ x
hy : G.IsLink e x y
⊢ H.IsNonloopAt e x
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

pp: case neg
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
case neg =>
      refine ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
      rintro (_ | ⟨a⟩)
      · rfl
      · exact (h ⟨a⟩).elim

Goal state after:
case pos
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
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₂]

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

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

Tactic:
by
  rw [delete_eq_restrict, restrict_isCircuit_iff, and_congr_right_iff, subset_sdiff,
    and_iff_right_iff_imp]
  exact fun h _ ↦ h.subset_ground

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
hE : M.E ⊆ N.E
⊢ M = N

Tactic:
obtain ⟨C, D, rfl⟩ := h
  rw [delete_ground, contract_ground, subset_sdiff, subset_sdiff] at hE
  rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ m.toSyn (m.degree (m.reduce hb f)) ≠ m.toSyn (m.degree f)

Tactic:
intro K

Goal state after:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.toSyn (m.degree (m.reduce hb f)) = m.toSyn (m.degree f)
⊢ False
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
hb' : ∃ i, m.degree (b i) = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
obtain ⟨i, hb0⟩ := hb'

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
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α), ∀ C ⊆ M.E, M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

pp: α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

Tactic:
· rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      sdiff_inter, sdiff_eq_empty.2 (M.closure_subset_ground _), union_empty]

Goal state after:
α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : 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
⊢ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + (r' + (monomial (m.degree f)) (m.leadingCoeff f))

Tactic:
simp [← add_assoc, ← H'.1, subLTerm]

Goal state after:
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 → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
⊢ ∀ J ⊆ Sigma.mk i ⁻¹' I, J.Finite → (M i).Indep J

Tactic:
intro J hJI hJ

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 : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ (M i).Indep J
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons.inr
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_eq_end : v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
| inr h_eq_end =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ nonMemberSubfamily a 𝒜 ↔ s ∈ 𝒜 ∧ a ∉ s

Tactic:
simp [nonMemberSubfamily]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
⊢ memberSubfamily a (image (insert a) 𝒜) = 𝒜

Tactic:
ext s
  simp only [mem_memberSubfamily, mem_image]
  refine ⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩
  rintro ⟨⟨t, ht, hts⟩, hs⟩
  rwa [← insert_erase_invOn.2.injOn (h𝒜 _ ht) hs hts]

Goal state after:
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 (#univ + 1), #(powersetCard x univ) • (↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
card_powersetCard,

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 (#univ + 1), (#univ).choose x • (↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ (n : ℕ), 0 < n → (↑m)⁻¹ ≤ ↑(#({a ∈ Ioc 0 n | a ∈ {n | n % m = 1}})) / ↑n

Tactic:
intro n hn

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ (↑m)⁻¹ ≤ ↑(#({a ∈ Ioc 0 n | a ∈ {n | n % m = 1}})) / ↑n
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n / ↑m ≤ ↑((n - 1) / m + 1 - 0)

pp: case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1

Tactic:
Nat.sub_zero,

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n / ↑m ≤ ↑((n - 1) / m + 1)

case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) → ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
rintro ⟨u, rfl, htu, hsuA⟩

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t u : Finset α
htu : Disjoint t u
hsuA : t ∪ u ∈ 𝒜
⊢ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = #u