mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (coeff n)
      ((-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))) =
    0

Tactic:
apply coeff_of_lt_order

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n <
    ((-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))).order
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommRing α
s : Finset α
x✝ : α × α × α
inst✝ : Fact (IsUnit 2)
x a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h₁ : y + b = x + a
h₂ : y + 2 * b = x + 2 * a
⊢ x = y

Tactic:
linear_combination 2 * h₁.symm - h₂.symm

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ 0 ≤ ((-1) ^ (k + 1)).order

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ 0 ≤ (∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ 0 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
⊢ Coprime 2 (2 * n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ 2 * ↑⟨n, ⋯⟩ ≤ 2 * n

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

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

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

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

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

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

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ 0 < 2 * 3

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ 3⁻¹ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case hx
x : ℕ
hx : 9 ≤ x
⊢ 0 < ↑((x - 3) / 6)

Tactic:
simp

Goal state after:
case hx
x : ℕ
hx : 9 ≤ x
⊢ 6 ≤ x - 3
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
h : X ⊆ V(G)
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, (noEdge X β).IsLink e x y → G.IsLink e x y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, (G.restrict E₀).IsLink e x y → G.IsLink e x y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
h : E(G) ⊆ E₀
⊢ V(G.restrict E₀) = V(G)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.restrict E(G) ≤ G

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤ G

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ E(G.restrict E(G)) = E(G)

Tactic:
simp

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

Goal state before:
pp: case vertexSet_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict (E(G) ∩ F) ≤ G

Tactic:
simp

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

Goal state before:
pp: case isLink_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, (noEdge ∅ β).IsLink e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ noEdge ∅ β ≤ G

Tactic:
constructor <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict F ≤ G

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ V(G.restrict (E(G) ∩ F)) = V(G.restrict F)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ E(G.restrict (E(G) ∩ F)) = E(G.restrict F)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → x ∈ V(⊥) → e ∈ E(⊥)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ G.restrict F ≤ G

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict F₁ ≤ G

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₁ ∩ F₂) ≤ G

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ V((G.restrict F₁).restrict F₂) = V(G.restrict (F₁ ∩ F₂))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G✝ H : Graph α β
F✝ F₀ : Set β
X : Set α
G : Graph α β
F : Set β
⊢ E(G.restrict (E(G) \ F)) = E(G) \ F

Tactic:
simp

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:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ E(G.restrict F) = E(G.deleteEdges (E(G) \ F))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.induce V(G) ≤ G

Tactic:
simp

Goal state after:
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:
simp_rw [isLink_iff_inc, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, G.IsLink e x y

Tactic:
← hedgeSet

Goal state after:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ E(G) ↔ ∃ x y, G.IsLink e x y
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
x y z u v w : α
e f : β✝
G H : Graph α β✝
vertexSet : Set α
β : Type u_3
⊢ ∀ ⦃e : β⦄, e ∈ ∅ → Std.Symm fun x x_1 ↦ False

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
x y z u v w : α
e f : β✝
G H : Graph α β✝
vertexSet : Set α
β : Type u_3
⊢ ∀ ⦃e : β⦄ ⦃x : α⦄ ⦃y : α⦄ ⦃v w : α⦄, False → False → x = v ∨ x = w

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
x y z u v w : α
e f : β✝
G H : Graph α β✝
vertexSet : Set α
β : Type u_3
⊢ ∀ (e : β), e ∈ ∅ ↔ ∃ x y, False

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : α
edgeSet : Set β
⊢ ∀ (e : β) (x : α), (banana u v edgeSet).Inc e x ↔ (banana v u edgeSet).Inc e x

Tactic:
by simp [or_comm]

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

Goal state before:
pp: case hV
α : Type u_1
β : Type u_2
u v x✝ : α
⊢ x✝ ∈ V(banana u v ∅) ↔ x✝ ∈ V(noEdge {u, v} β)

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
u v : α
e✝ : β
x✝ y✝ : α
⊢ (banana u v ∅).IsLink e✝ x✝ y✝ ↔ (noEdge {u, v} β).IsLink e✝ x✝ y✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
v : α
edgeSet : Set β
⊢ V(bouquet v edgeSet) = {v}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).IsLink e x y ↔ e ∈ edgeSet ∧ x = v ∧ y = v

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ x = v

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ x = v ∧ y = v

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = v

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
v : α
⊢ bouquet v ∅ = noEdge {v} β

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
w : α
hzw : G.IsLink e x w
⊢ f x = f x ∨ f x = f w

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
z : α
hzw : G.IsLink e z x
⊢ f x = f z ∨ f x = f x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e : β
x y : α'
f : α → α'
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α'⦄, Relation.Map (G.IsLink e) f f x y → Relation.Map (G.IsLink e) f f v w → x = v ∨ x = w

Tactic:
rintro e - - - - ⟨x, y, hxy, rfl, rfl⟩ ⟨z, w, hzw, rfl, rfl⟩
    obtain rfl | rfl := hxy.left_eq_or_eq hzw <;> simp

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

Goal state before:
pp: case hV
α : Type u_1
β : Type u_4
G : Graph α β
a : α
⊢ a ∈ V(map id G) ↔ a ∈ V(G)

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_4
G : Graph α β
a : β
b c : α
⊢ (map id G).IsLink a b c ↔ G.IsLink a b c

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
u v : α
e f : β
X Y : Set α
inst✝ : G.Simple
V : Set α
⊢ ∀ ⦃e f : β⦄ ⦃x y : α⦄, (noEdge V β).IsLink e x y → (noEdge V β).IsLink f x y → e = f

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
x y : α✝
e e' f : Set α✝
H : Hypergraph α✝
α : Type u_4
⊢ ∀ ⦃e : Set α⦄, e ∈ ∅ → e ⊆ ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e e' f✝ : Set α
H : Hypergraph α
f : Set α
⊢ ∀ ⦃e : Set α⦄, e ∈ ∅ → e ⊆ f

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e e' f✝ : Set α
H : Hypergraph α
f : Set α
⊢ ∀ ⦃e : Set α⦄, e ∈ 𝒫 f → e ⊆ f

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
e f : Set α
⊢ e ∈ E(completeOn f) ↔ e ⊆ f

Tactic:
simp

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

Goal state before:
pp: case hR
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ (M ↾ M.E \ D₁).E \ D₂ ⊆ M.E \ D₁

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ Disjoint ∅ M.E

Tactic:
exact empty_disjoint _

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
⊢ (M ＼ {e}).Indep I ↔ M.Indep I ∧ e ∉ I

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
D : Set α
⊢ e ∈ M.E ∧ e ∉ D → (e ∉ M.closure ((M.E \ D) \ {e}) ↔ e ∉ M.closure ((M.E \ D) \ {e}))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥s
⊢ (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨↑(↑f ↑x), ⋯⟩) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥s)
⊢ (fun x ↦ ⟨↑(↑f ↑x), ⋯⟩) ((fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩) n) = n

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥sᶜ)
⊢ ¬↑(↑f ((Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩)) < #s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M = M ／ ∅ ＼ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : ℕ
hn : n < Fintype.card ↥sᶜ
⊢ (fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩) ((fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) ⟨n, hn⟩) = ⟨n, hn⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ¬↑n < #s
⊢ ↑n - #s < Fintype.card ↥sᶜ

Tactic:
simp

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ¬↑n < #s
⊢ ↑n - #s < Fintype.card X - #s
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (M✶ ／ X)✶ = M ＼ X

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ／ X ＼ Y)✶ = M✶ ＼ X ／ Y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ＼ X ／ Y)✶ = M✶ ／ X ＼ Y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ C₁ ／ (C₂ \ C₁)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hts' : #t ≤ #s
⊢ False

Tactic:
· exact hts <| ht.subset_of_card_le_card hs hts'

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → B ⊆ M.E → (M✶.IsBase (M.E \ (I ∪ B)) ↔ M✶.IsBase (M.E \ (I ∪ B)))

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
⊢ (M j).IsBase (Sigma.mk j ⁻¹' (B₁ \ {⟨i, e⟩}) ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})

Tactic:
preimage_sdiff

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ Sigma.mk j ⁻¹' {⟨i, e⟩} ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
⊢ ∀ (x : ?m.254 i), {⟨i, x⟩} = Sigma.mk i '' {x}

Tactic:
simp

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

Goal state before:
pp: case h.right.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
i : ι
hb0 : m.degree (b i) = 0
⊢ ∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * (Finsupp.single i (⋯.unit⁻¹ • f)) i_1)) ≤ m.toSyn (m.degree f)

Tactic:
intro j

Goal state after:
case h.right.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
i : ι
hb0 : m.degree (b i) = 0
j : ι
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case e'_5
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono
    (fun x ↦
      C fun x_1 ↦
        match x_1 with
        | (i, e) => x i e)
    l
x✝ : ι × Shrink.{0, u_7} η → α
⊢ x✝ = ⇑(Equiv.refl α).symm ∘ x✝ ∘ ⇑(Equiv.refl (ι × Shrink.{0, u_7} η))

Tactic:
simp

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

Goal state before:
pp: case h.right.right
σ : 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
⊢ ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
simp

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

Goal state before:
pp: σ : 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
⊢ ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
simp

Goal state after: