mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#((↑H).toFinset * Z)) / ↑(#(↑H).toFinset) = ↑(#((↑H).toFinset * S)) / ↑(#(↑H).toFinset)

Tactic:
congr 3; simpa using congr(($hHZS).toFinset)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsLink G.IsLink E(H)

Tactic:
by
  rintro e he
  ext x y
  exact isLink_iff hHG he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.Inc G.Inc E(H)

Tactic:
by
  rintro e he
  ext x
  exact hHG.inc_congr he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
heq : V(G) = V(H) ∧ E(G) = E(H)
⊢ False

Tactic:
exact hGH.2 <| hGH.1.compatible.ext heq.1 heq.2

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h h' : G.IsLink e x y
⊢ y = y

Tactic:
rfl

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z

Tactic:
rfl

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hA₀ : A.Nonempty
hA₁ : ↑(#(A * A)) ≤ (2 - ε) * ↑(#A)
⊢ #A ≤ #A

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ V(G.induce (V(G) \ X)) = V(G) \ X

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ E(G.deleteVerts X) = {e | ∃ x y, G.IsLink e x y ∧ x ∉ X ∧ y ∉ X}

Tactic:
simp [edgeSet_eq_setOfPred_exists_isLink]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
⊢ G.Inc e x

Tactic:
obtain ⟨z, w, hzw⟩ := exists_isLink_of_mem_edgeSet h.1

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
z w : α
hzw : G.IsLink e z w
⊢ G.Inc e x
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
⊢ V(map f G) = V(map g G)

Tactic:
grind

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 α
G : SimpleGraph α
e : Sym2 α
u v x y : α
he : e = s(u, v) ∧ e ∈ G.edgeSet
hf : e = s(x, y) ∧ e ∈ G.edgeSet
⊢ u = x ∨ u = y

Tactic:
grind

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u✝ v✝ : α
e f : β
X Y : Set α
G : SimpleGraph α
u v : α
⊢ s(u, v) ∈ G.edgeSet ↔ ∃ x y, s(u, v) = s(x, y) ∧ s(u, v) ∈ G.edgeSet

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val✝ : ι
⊢ ↑(vertical v l) x (Sum.inl val✝) = Sum.elim v (↑l x) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val✝ : ι'
⊢ ↑(vertical v l) x (Sum.inr val✝) = Sum.elim v (↑l x) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val✝ : ι
⊢ ↑(l.horizontal v) x (Sum.inl val✝) = Sum.elim (↑l x) v (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val✝ : ι'
⊢ ↑(l.horizontal v) x (Sum.inr val✝) = Sum.elim (↑l x) v (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι
⊢ ↑(l.prod l') x (Sum.inl val✝) = Sum.elim (↑l x) (↑l' x) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι'
⊢ ↑(l.prod l') x (Sum.inr val✝) = Sum.elim (↑l x) (↑l' x) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case none
α : 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 α
C : (Unit → Option α) → κ
⊢ C (↑(diagonal (Option α) Unit) none) = C fun x ↦ none

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case htn
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}.Nonempty

pp: case refine_2.ht0
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ IsCompact {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop 0 a)}

pp: case refine_2.htcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}

Tactic:
· intro n
      exact ⟨pure _, mem_pure.mpr <| FP.head _⟩

Goal state after:
case refine_2.ht0
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ IsCompact {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop 0 a)}

case refine_2.htcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ M.Dep {e} ∧ e ∉ D ↔ M.IsLoop e ∧ e ∉ D

Tactic:
singleton_dep

Goal state after:
α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ M.IsLoop e ∧ e ∉ D ↔ M.IsLoop e ∧ e ∉ D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ＼ M.loops = M ↾ {e | M.IsNonloop e}

Tactic:
delete_eq_restrict,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M ↾ M.E \ M.loops = M ↾ {e | M.IsNonloop 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:
delete_eq_restrict,

Goal state after:
α : Type u_1
M : Matroid α
D C : Set α
⊢ (M ↾ M.E \ D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
delete_eq_restrict,

Goal state after:
α : Type u_1
e : α
M : Matroid α
D : Set α
⊢ (M ↾ M.E \ D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ {e}) ∧ e ∈ M.E ∧ e ∉ D
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop 0 a) ⊆ FP a

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
I : Set α
hI : N.Indep I
hNM : N ≤m M
⊢ M.Indep I

Tactic:
obtain ⟨C, D, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
I C D : Set α
hI : (M ／ C ＼ D).Indep I
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤m M
⊢ M.IsNonloop e

Tactic:
obtain ⟨C, D, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
e : α
C D : Set α
h : (M ／ C ＼ D).IsNonloop e
⊢ M.IsNonloop e
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 → (M✶.IsBasis ((M.E \ I) \ B) (M.E \ I) ∧ B ⊆ M.E ↔ M✶.IsBase (M.E \ (I ∪ B)) ∧ I ⊆ M.E ∧ B ⊆ M.E)

Tactic:
and_iff_right hI.subset_ground,

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶.IsBasis ((M.E \ I) \ B) (M.E \ I) ∧ B ⊆ M.E ↔ M✶.IsBase (M.E \ (I ∪ B)) ∧ B ⊆ M.E)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
h : m.subLTerm f = 0
⊢ False

Tactic:
simp only [h, degree_zero] at hf'

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
h : m.subLTerm f = 0
hf' : 0 = m.degree f
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ Disjoint {e} I

Tactic:
simpa using he.2

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Disjoint (J \ I) X

Tactic:
hIX.eq_of_subset_indep (hJY.indep.inter_right X) (subset_inter hIJ hIX.subset)
      inter_subset_right,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Disjoint (J \ (J ∩ X)) X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = M.closure (X ∪ C) \ (X ∪ C) ∪ M.closure (X ∪ C) \ C ∩ X

Tactic:
← contract_loops_eq,

Goal state after:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = (M ／ (X ∪ C)).loops ∪ M.closure (X ∪ C) \ C ∩ X
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case refine_1.inr
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
j : ι
hij : i ≠ j
⊢ (M j).Indep (Sigma.mk j ⁻¹' I ∪ Sigma.mk j ⁻¹' Sigma.mk i '' I₀)

Tactic:
rw [sigma_mk_preimage_image' hij, union_empty]

Goal state after:
case refine_1.inr
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
j : ι
hij : i ≠ j
⊢ (M j).Indep (Sigma.mk j ⁻¹' I)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n none = d ∧ n.some = m
⊢ coeff m (((optionEquivLeft R σ) P).coeff d) = 0

Tactic:
← hn.1,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n none = d ∧ n.some = m
⊢ coeff m (((optionEquivLeft R σ) P).coeff (n none)) = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ＼ D = M ＼ D ／ C

Tactic:
delete_eq_restrict,

Goal state after:
α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C

Tactic:
delete_eq_restrict,

Goal state after:
α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ↾ (M ／ C).E \ D = (M ↾ M.E \ D) ／ C
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ (M.E ∪ N.E)

Tactic:
inter_eq_self_of_subset_left hI.2.2

Goal state after:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (((optionEquivLeft R σ) P).coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
← hn.1,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : ¬coeff e (((optionEquivLeft R σ) P).coeff (n none)) = 0
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case nil
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✝ a b : V
⊢ height a ≤ height a

Tactic:
rfl

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

Goal state before:
pp: case nil.nil
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
⊢ Path.nil = Path.nil

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
rw [hQ, ← hn.1, ← hn.2, optionEquivLeft_coeff_some_coeff_none, ← ne_eq,
        ← MvPolynomial.mem_support_iff] at he

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : n ∈ P.support
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length ≤ p.length

Tactic:
apply shortest_path_spec

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

Goal state before:
pp: case refl.left
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ a = a

Tactic:
rfl

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

Goal state before:
pp: case refl.right
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ ⟨e, ⋯⟩ ≍ ⟨e, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case nil.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ : U
a✝ : (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩
⊢ ⟨u, Path.nil⟩ = ⟨u, Path.nil⟩

Tactic:
rfl

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 ι
s : S
hs : ι s • (ι s)⁻¹ • x = x
⊢ ⟨(ι ((labelling V ι).map ⟨s, hs⟩))⁻¹ • x, ⟨s, ⋯⟩⟩ = ⟨(ι s)⁻¹ • x, ⟨s, hs⟩⟩

Tactic:
rfl

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

Goal state before:
pp: case cons.cons.refl.refl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
hφx : φ.obj x₁ = φ.obj x₁
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
hφy : φ.obj y₁ = φ.obj y₁
hφe : φ.map e₁ ≍ φ.map e₁
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₁)
h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₁, e₁⟩
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₁, p₁.cons e₁⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mpr
inst✝ : DecidablePred fun x ↦ x ∈ Set.univ
hA : 0 ∈ Set.univ
⊢ {0}ᶜ ⊆ Set.univ

Tactic:
exact Set.subset_univ {0}ᶜ

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ (fun x1 x2 ↦ x1 + x2) a b = n

Tactic:
grind

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ (fun x1 x2 ↦ x1 + x2) a b = n

Tactic:
grind

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 α
u a : α
h : ¬(Disjoint u a ∧ u ≤ a)
⊢ a = a

Tactic:
rfl

Goal state after: