mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
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:
by 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:
by 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:
by 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:
by simp

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : z ≠ y
hy : G.IsLink e y z
⊢ False

Tactic:
← h.eq_of_inc hy.inc_left,

Goal state after:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : z ≠ x
hy : G.IsLink e y z
⊢ False
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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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 ∈ ∅ → Std.Symm fun x x_1 ↦ False

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

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this✝¹ : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
this✝ : CompactSpace M'
this : Nonempty M'
⊢ ∃ m ∈ s, m * m = m

Tactic:
have : ∀ p : M', Continuous (· * p) := fun p =>
    ((continuous_const_mul p.1).comp continuous_subtype_val).subtype_mk _

Goal state after:
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this✝² : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x ↦ x * p
⊢ ∃ m ∈ s, m * m = m
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✝ H : Hypergraph α
f : α → β
⊢ ∀ ⦃e : Set β⦄, e ∈ image f '' E(H) → e ⊆ f '' V(H)

Tactic:
by
    rintro - ⟨e, he, rfl⟩
    exact image_mono he.subset_vertexSet

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

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_4
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)}
⊢ ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S

Tactic:
intro U hU V hV

Goal state after:
case refine_4
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)}
U : Ultrafilter M
hU : U ∈ S
V : Ultrafilter M
hV : V ∈ S
⊢ U * V ∈ S
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
s : Set M
hs : s ∈ U
⊢ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s} ∈ ↑U

Tactic:
← U_idem

Goal state after:
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
s : Set M
hs : s ∈ U * U
⊢ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s} ∈ ↑U
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.head'
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
b : Stream' M
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → b.head ∈ ↑p

Tactic:
| head' b =>

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X ∩ (Dᶜ ∩ M.E)) ∩ (Dᶜ ∩ M.E) = M.closure (X \ D) \ D

Tactic:
← inter_assoc X,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X ∩ Dᶜ ∩ M.E) ∩ (Dᶜ ∩ M.E) = M.closure (X \ D) \ D
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:
by 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:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
⊢ (M ／ I).Indep (J \ I)

Tactic:
by
  rwa [← (hJ.subset hIJ).union_indep_iff_contract_indep, union_eq_self_of_subset_left hIJ]

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

Goal state after:
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
I : Set α
hI : ∀ J_1 ⊆ I, J_1.Finite → (M ／ J).Indep J_1
e : α
heI : e ∈ I
⊢ {e}.Finite

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ C' ⊆ C' \ K ∪ K

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a✝ : ι
⊢ ∀ (x : α), x ∈ Prod.mk a✝ ⁻¹' I ↔ x ∈ Sigma.mk a✝ ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' I

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a✝ : ι
⊢ ∀ (x : α), x ∈ Prod.mk a✝ ⁻¹' X ↔ x ∈ Sigma.mk a✝ ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' X

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : α),
    x ∈ Sum.inl ⁻¹' I ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : α),
    x ∈ Sum.inl ⁻¹' X ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : β),
    x ∈ Sum.inr ⁻¹' I ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : β),
    x ∈ Sum.inr ⁻¹' X ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X

Tactic:
by 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
hf'0 : m.subLTerm f = 0
⊢ ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
by simp

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

Goal state before:
pp: case h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I✝ : Set α
a✝ : I✝ ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I✝ ↔ (N.disjointSum M ⋯).Indep I✝

Tactic:
simpa [union_comm] using ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩,
    fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

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

Goal state before:

Tactic:
simpa [union_comm] using ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩,
    fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
h1 : ∀ (b_1 : ↑{b}), m.toSyn (m.degree (↑b_1 * g b_1)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ∀ b_1 ∈ {b}, ¬m.degree b_1 ≤ c
⊢ b ∈ {b}

Tactic:
by 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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
h1 : m.toSyn (m.degree (↑⟨b, ⋯⟩ * g ⟨b, ⋯⟩)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ∀ b_1 ∈ {b}, ¬m.degree b_1 ≤ c
⊢ b ∈ {b}

Tactic:
by 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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ b ∈ {b}

Tactic:
by 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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ g ⟨b, ?m.142⟩ = 0 → 0 * ↑⟨b, ?m.142⟩ = 0

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ 0 < p.vertices.length

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
hn : 0 ≤ nil.length
⊢ nil = nil.comp nil

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
hn : p'.length.succ ≤ p'.length + 1
⊢ p'.cons e = (p'.cons e).comp nil

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
hn : p'.length.succ ≤ p'.length + 1
⊢ (p'.cons e).length = p'.length.succ

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b v : V
p₁ : Path a v
p₂ : Path v b
hn : p₁.length < (p₁.comp p₂).vertices.length
hn_le_len : p₁.length ≤ (p₁.comp p₂).length
⊢ v = (p₁.comp p₂).vertices[p₁.length]

Tactic:
by simp

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

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

Tactic:
simp [vertices_nil]

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

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
x✝ : Costar (SingleObj.star S)
fst✝ : SingleObj S
s : fst✝ ⟶ SingleObj.star S
⊢ ι s • (ι s)⁻¹ • x = x

Tactic:
by simp

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

Goal state before:
pp: U : Type ?u.2
inst✝⁴ : Quiver U
V : Type ?u.6
inst✝³ : Quiver V
φ : U ⥤q V
W : Type ?u.15
inst✝² : Quiver W
ψ : V ⥤q W
inst✝¹ : HasInvolutiveReverse U
inst✝ : HasInvolutiveReverse V
u : U
e : Star u
⊢ (fun e ↦ ⟨e.fst, reverse e.snd⟩) ((fun e ↦ ⟨e.fst, reverse e.snd⟩) e) = e

Tactic:
by simp

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

Goal state before:
pp: U : Type ?u.2
inst✝⁴ : Quiver U
V : Type ?u.6
inst✝³ : Quiver V
φ : U ⥤q V
W : Type ?u.15
inst✝² : Quiver W
ψ : V ⥤q W
inst✝¹ : HasInvolutiveReverse U
inst✝ : HasInvolutiveReverse V
u : U
e : Costar u
⊢ (fun e ↦ ⟨e.fst, reverse e.snd⟩) ((fun e ↦ ⟨e.fst, reverse e.snd⟩) e) = e

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
this : {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k
⊢ #(Ioo 0 k) = k - 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : 1 ∉ A
⊢ 1 - (↑1)⁻¹ ≤ 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜✝ : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
a : α
𝒜 : Finset (Finset α)
h𝒜₀ : p (nonMemberSubfamily a 𝒜)
h𝒜₁ : p (memberSubfamily a 𝒜)
⊢ ∀ s ∈ memberSubfamily a 𝒜, a ∉ s

Tactic:
by simp

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 1 ∉ ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜}) + #({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜

pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ s ∈ ↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}), s ∈ {s | a ∈ s}

Tactic:
← card_union_of_disjoint

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ s ∈ ↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}), s ∈ {s | a ∈ s}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 0 ∈ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ Set.univ = Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 1 ∉ Set.ofPred Even

Tactic:
by simp

Goal state after: