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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
⊢ nil.bypass.support <+ nil.support

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
⊢ nil.bypass.darts <+ nil.darts

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : G.IsMaximumIndepSet t
⊢ #t = G.indepNum

Tactic:
by
  rw [← isMaximumClique_compl] at tmc
  simp_rw [indepNum, ← isNClique_compl]
  exact Gᶜ.maximumClique_card_eq_cliqueNum t tmc

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u✝ : V
hp : ∀ e ∈ Walk.nil.edges, e ∈ H.edgeSet
pp : Walk.nil.IsPath
⊢ (Walk.nil.transfer H hp).IsPath

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
qc : nil.IsCycle
hq : ∀ e ∈ nil.edges, e ∈ H.edgeSet
⊢ (nil.transfer H hq).IsCycle

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case left
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49

Tactic:
exact sum_density_div_card_le_density_add_eps hPα hPε hε₁ hA hB

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 < 1

Tactic:
by
  calc
    _ ≤ (2 * ⌈4 / ε⌉₊ ^ 3 : ℝ)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 := by gcongr; exact min_le_left _ _
    _ = 2⁻¹ := by rw [mul_inv, inv_mul_cancel_right₀]; positivity
    _ < 1 := by norm_num

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
    (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
t : ℝ := ↑(G.edgeDensity U V)
⊢ 3 / 4 * ε ≤ |p - q|

Tactic:
have hrs : |r - s| ≤ ε / 5 := abs_density_star_sub_density_le_eps hPε hε₁ hUVne hUV

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
    (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
t : ℝ := ↑(G.edgeDensity U V)
hrs : |r - s| ≤ ε / 5
⊢ 3 / 4 * ε ≤ |p - q|
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ σₘ[A, B] ≤ ↑(#B)

Tactic:
rw [mulConst, div_le_iff₀' (by positivity)]

Goal state after:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * B)) ≤ ↑(#A) * ↑(#B)
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
⊢ Eₘ[univ, t] = Fintype.card α * #t ^ 2

Tactic:
by
  simp only [mulEnergy, univ_product_univ, Fintype.card, sq, ← card_product]
  let f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
  have : (↑((univ : Finset α) ×ˢ t ×ˢ t) : Set (α × α × α)).InjOn f := by
    rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h
    simp_rw [f, Prod.ext_iff] at h
    obtain ⟨h, rfl, rfl⟩ := h
    rw [mul_right_cancel h.1]
  rw [← card_image_of_injOn this]
  congr with a
  simp only [mem_filter, mem_product, mem_univ, true_and, mem_image,
    Prod.exists]
  refine ⟨fun h => ⟨a.1.1 * a.2.2⁻¹, _, _, h.1, by simp [f, mul_right_comm, h.2]⟩, ?_⟩
  rintro ⟨b, c, d, hcd, rfl⟩
  simpa [f, mul_right_comm]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ 𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) * (starRingEnd ℂ) (ψ a) =
    𝔼 i, ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ)) * (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) i

Tactic:
AddChar.sub_apply,

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ 𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) * (starRingEnd ℂ) (ψ a) =
    𝔼 i, ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ)) * ((∑ ψ ∈ u, ψ) i * (∑ ψ ∈ t \ u, ψ) (-i))
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case nil
hL : [].SortedLT
⊢ (map (fun i ↦ 2 ^ i) []).sum.bitIndices = []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
intros
    simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t

Tactic:
by
  simpa using toColex_sdiff_le_toColex_sdiff (inter_subset_left (s₁ := s)) inter_subset_right

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v w : ℙ F (m → F)
⊢ v.orthogonal w ↔ w.orthogonal v

Tactic:
induction v with | h v hv => induction w with | h w hw =>
  rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
· refine (lt_iff_exists_forall_lt.2 ⟨w, mem_erase.2 ⟨hmw.ne', hwt⟩, mt mem_of_mem_erase hws,
      fun b hbs hbt ↦ ?_⟩).le
    change b ∉ t.erase m at hbt
    rw [mem_erase, not_and_or, not_ne_iff] at hbt
    obtain rfl | hbt := hbt
    · assumption
    · by_contra! hwb
      exact hbt <| (hw <| hwb.lt_of_ne <| ne_of_mem_of_not_mem hwt hbt).1 <| mem_of_mem_erase hbs

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 : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z * w⁻¹ = x⁻¹ * y

Tactic:
mul_inv_eq_iff_eq_mul,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z = x⁻¹ * y * w
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ ∀ j < p.firstReturn, decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
intro j hj

Goal state after:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = if a = b then 1 else 0

Tactic:
by
  split_ifs with hab
  · simp [hab]
  by_cases hab : a ≤ b
  · simp [Icc_eq_cons_Ico hab, mu_eq_neg_sum_Ico_of_ne ‹_›]
  · exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hax ↦ hab <| hax.trans (mem_Icc.1 hx).2) _

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

Goal state before:
pp: case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ ∀ j < (↑p).length + 1,
    decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Tactic:
intro j hj

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : ↑a + 1 = ↑b + 1
⊢ a = b

Tactic:
add_left_inj

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : ↑a = ↑b
⊢ a = b
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2

Tactic:
Nat.choose_succ_succ (n + 1),

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ n + 1 + (n + 1).choose 2 = (n + 1).choose 1 + (n + 1).choose (succ 1)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)

Tactic:
have h := hasSum_pentagonalSeries R

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
⊢ HasSum (fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Enumerative.Stirling

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

Tactic:
Nat.choose_succ_succ (n + 1),

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

Goal state before:
pp: case calc_1
n : ℕ
⊢ ↑(n + 3) / 3 - 2 ≤ ↑(2 * (n / 6) + 1)

pp: case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))

Tactic:
· simp only [cast_add, cast_ofNat, cast_mul, cast_one, tsub_le_iff_right]
      rw [← div_add_one (three_ne_zero' ℝ), ← le_sub_iff_add_le, div_le_iff₀ (zero_lt_three' ℝ),
        add_assoc, add_sub_assoc, add_mul, mul_right_comm, add_sub_cancel_left]
      norm_cast
      rw [← mul_add_one]
      exact (Nat.lt_mul_div_succ _ <| by simp).le

Goal state after:
case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))
Module: Mathlib.Combinatorics.Graph.Basic

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

Tactic:
by
  obtain rfl | rfl := h'.eq_or_eq_of_isLink h <;> rfl

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

Goal state before:
pp: case e'_3.e'_3
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ V(G₂) = V(G₁)

pp: case e'_3.e'_4
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ G₂.IsLink = G₁.IsLink

pp: case e'_3.e'_5
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ E(G₂) = E(G₁)

Tactic:
· exact hV.symm

Goal state after:
case e'_3.e'_4
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ G₂.IsLink = G₁.IsLink

case e'_3.e'_5
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ E(G₂) = E(G₁)
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
f : Set α
hf : f.Nonempty
⊢ (Hypergraph.trivialOn f).IsTrivial

Tactic:
grind [trivialOn, IsTrivial]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: ⊢ ∀ {α : Type u} [Fintype α],
    (∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l) →
      ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
intro α

Goal state after:
α : Type u
⊢ ∀ [Fintype α],
    (∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l) →
      ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
delete_dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ M.Dep {e} ∧ Disjoint {e} D ↔ M.IsLoop e ∧ e ∉ D
Module: Mathlib.Combinatorics.Matroid.Minor.Order

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

Tactic:
contract_delete_contract_delete'

Goal state after:
α : Type u_1
M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁) = M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁)
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M N : Matroid α
x✝ : N ≤m M ∧ N.E ⊂ M.E
h : N ≤m M
hss : N.E ⊂ M.E
h' : M ≤m N
⊢ N.E = M.E

Tactic:
by rw [h'.antisymm h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (M ／ I ＼ (X \ I)).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
delete_dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (M ／ I).Dep D ∧ Disjoint D (X \ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B : Set ((i : ι) × α i)
hB : ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' B) ⊆ univ.sigma fun i ↦ (M i).E

Tactic:
apply sigma_mono Subset.rfl fun i ↦ (hB i).subset_ground

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
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
set n := (embDomain Function.Embedding.some e).update none m with hn

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 : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n = (embDomain Embedding.some e).update none m
⊢ 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:
| nil =>

Goal state after:
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 : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
q : Path r r
⊢ Path.nil = q

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
a b : Symmetrify V
⊢ Nonempty (Path a a)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_2
inst✝ : Quiver V
a b : V
⊢ nil.vertices.length = nil.length + 1

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
⊢ a ∈ nil.vertices

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
⊢ nil.vertices.head? = some a

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
h : nil.vertices ≠ []
⊢ nil.vertices.head h = a

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
⊢ nil.vertices[0] = a

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
h : nil.vertices ≠ []
⊢ nil.vertices.getLast h = a

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b c : V
p : Path a b
⊢ (p.comp nil).vertices = p.vertices.dropLast ++ nil.vertices

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
q : Path a a
x✝ : nil.length = 0 ∧ q.length = 0
hp : nil.length = 0
hq : q.length = 0
⊢ nil.comp q = nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
n : ℕ
hn : n ≤ nil.length
⊢ ∃ v p₁ p₂, nil = p₁.comp p₂ ∧ p₁.length = n

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝¹ : Quiver V
R : Type u_2
inst✝ : Monoid R
w : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path a b
⊢ weight (fun {i j} ↦ w) (p.comp nil) = weight (fun {i j} ↦ w) p * weight (fun {i j} ↦ w) nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j : V
⊢ 0 < weight (fun {i j} ↦ w) nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e
i j : V
⊢ 0 ≤ weight (fun {i j} ↦ w) nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v : V
hv : v ∈ nil.vertices
⊢ ∃ p₁ p₂, nil = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
| nil =>

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

Goal state before:
pp: case 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₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ →
      ⟨u, Path.nil⟩ = a₂

Tactic:
| nil =>

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

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

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
simp_rw [mem_disjSups]
  refine ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, ?_⟩
  rintro h _ ⟨a, ha, b, hb, hab, rfl⟩
  exact h _ ha _ hb hab

Goal state after: