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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]

Tactic:
· rw [getElem?_pos _ _ <| by grind, Option.some_inj]
    by_cases hi' : i = p₁.length
    · have := h <| i - 1
      grind [not_nil_iff_lt_length, snd_darts_getElem]
    have := h i
    grind [fst_darts_getElem]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Tactic:
simpa [isTrail_def] using h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
this : ((p.take (p.length - 1)).take n).IsPath
⊢ (p.take n).IsPath

Tactic:
by
    rwa [take_take, isPath_copy, show min (p.length - 1) n = n by omega] at this

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
w✝ : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ s) y → w✝ ≤ y → y ≤ w✝
u v : V
p : G.Walk u v
hp : p.IsTrail
right✝ : p.length = w✝
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsTrail
⊢ p'.length ≤ p.length

Tactic:
have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝¹ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
this✝ : s.Finite
x : V
w✝ : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ s) y → w✝ ≤ y → y ≤ w✝
u v : V
p : G.Walk u v
hp : p.IsTrail
right✝ : p.length = w✝
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsTrail
this : w✝ ≤ p'.length → p'.length ≤ w✝
⊢ p'.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsPath ∧ p.length = n}
this : s.Finite
x : V
w✝ : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ s) y → w✝ ≤ y → y ≤ w✝
u v : V
p : G.Walk u v
hp : p.IsPath
right✝ : p.length = w✝
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsPath
⊢ p'.length ≤ p.length

Tactic:
have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝¹ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsPath ∧ p.length = n}
this✝ : s.Finite
x : V
w✝ : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ s) y → w✝ ≤ y → y ≤ w✝
u v : V
p : G.Walk u v
hp : p.IsPath
right✝ : p.length = w✝
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsPath
this : w✝ ≤ p'.length → p'.length ≤ w✝
⊢ p'.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ G.IsClique (Subtype.val '' A)

Tactic:
simp only [Set.Pairwise, Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
  intro _ ⟨_, ainA⟩ _ ⟨_, binA⟩ anb
  exact S.adj_sub (c ainA binA (Subtype.coe_ne_coe.mp anb)).2.2

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False

Tactic:
have hl := hpc.three_le_length

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
⊢ (↑(toTriangle (a, b, c)) ∩ ↑(toTriangle (x, y, z))).Subsingleton

Tactic:
have := ne_of_apply_ne _ h'

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : (a, b, c) ≠ (x, y, z)
⊢ (↑(toTriangle (a, b, c)) ∩ ↑(toTriangle (x, y, z))).Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ s, (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
· obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
    exact ⟨_, toTriangle_is3Clique hz, hxy⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * (↑(#A) * ↑(#A)) = ↑(#(A / A)) * ↑(#A)

Tactic:
rw [← mul_assoc, divConst_mul_card]

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u ⬝ᵥ (crossProduct v) w = det ![u, v, w]

Tactic:
rw [vec3_dotProduct, cross_apply, det_fin_three]
  dsimp only [Matrix.cons_val]
  ring

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
← not_le,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ ¬toColex t ≤ toColex s ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
⊢ ∃ b ∈ ofColex (toColex t), b ∉ ofColex (toColex s) ∧ a ≤ b

Tactic:
· have hst : s ≠ t := ne_of_mem_of_not_mem' has hat
    refine ⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩
    simpa [mem_symmDiff, h hst] using max'_mem _ <| symmDiff_nonempty.2 hst

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w ≠ 0
⊢ (mk F v hv).cross (mk F w hw) = mk F ((crossProduct v) w) h

Tactic:
by
  rw [cross_mk, dif_neg h]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ w.orthogonal (v.cross w)

Tactic:
rw [orthogonal_comm]
  exact cross_orthogonal_right h

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

pp: case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : ¬#sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

Tactic:
· rw [hs₃, Nat.le_zero]
      rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢
      rw [hs₃]
      rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
      exact fun p =>
        Exists.elim (exists_line p) -- If `s = univ`, then show `s.bUnion t = univ`
        fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩

Goal state after:
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : ¬#sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: s : DyckStep
⊢ s = U ∨ s = D

Tactic:
cases s <;> tauto

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

Goal state before:
pp: case e'_6
p : DyckWord
s : DyckStep
⊢ (s == U) = decide ¬(s == D) = true

Tactic:
cases s <;> tauto

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ 0 < p.firstReturn

Tactic:
← not_le,

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ¬p.firstReturn ≤ 0
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case a
n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
ha0 : a ≠ 0
⊢ a * (count a p.parts * p.parts.bell) = (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)

Tactic:
have hsum : (p.parts.erase a).sum + a = n + 1 := by
      simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (cons_erase (mem_dedup.mp ha))

Goal state after:
case a
n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
ha0 : a ≠ 0
hsum : (p.parts.erase a).sum + a = n + 1
⊢ a * (count a p.parts * p.parts.bell) = (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
⊢ ↑p <:+: ↑r

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Goal state after:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ ↑p <:+: ↑0

case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
⊢ ↑p <:+: ↑r
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ ↑p <:+: ↑0

pp: case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
⊢ ↑p <:+: ↑r

Tactic:
· rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih

Goal state after:
case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
⊢ ↑p <:+: ↑r
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
⊢ p.semilength ≤ r.semilength

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Goal state after:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ p.semilength ≤ semilength 0

case tail.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
⊢ p.semilength ≤ r.semilength
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ p.semilength ≤ semilength 0

pp: case tail.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
⊢ p.semilength ≤ r.semilength

Tactic:
· rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih

Goal state after:
case tail.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
⊢ p.semilength ≤ r.semilength
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

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

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))

Tactic:
· apply Multipliable.tendsto_prod_tprod_nat
    convert h (k + 1) using 4
    ring

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
A : Finset G
hA : t + 1 ≤ #A
⊢ (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) < (κ + 1) / ((κ + 1) / (1 - K)) * (↑t + 1)

Tactic:
by gcongr; exact Nat.lt_floor_add_one _

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb✝ : b ∈ n⁻¹ •> N
hb : a * b ∈ a •> n⁻¹ •> N
this : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty
⊢ a * b ∈ n⁻¹ •> N

Tactic:
simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a) this] using! hb

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 ∩ E(G)) = G.restrict F

Tactic:
inter_comm,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict (E(G) ∩ F) = G.restrict F
Module: Mathlib.Combinatorics.Graph.Delete

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

Tactic:
inter_comm,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Module: Mathlib.Combinatorics.Graph.Delete

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

Tactic:
inter_comm,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₁ᶜ ∩ F₂ᶜ ∩ E(G)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : 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 α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨ι, _inst, fun C => (hι C).resolve_left ?_⟩

Goal state after:
α : 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 α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
⊢ ¬∃ s, s.lines.card = Fintype.card κ + 1
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint (X \ D ∩ M.E) D

Tactic:
inter_comm,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint (M.E ∩ (X \ D)) D
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (m.subLTerm f)) ≤ m.toSyn (m.degree f)

Tactic:
by
  apply le_trans degree_sub_le
  simp only [sup_le_iff, le_refl, true_and]
  apply degree_monomial_le

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
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J

Tactic:
have hss : X \ I ⊆ (M✶ ＼ I).coloops := fun e he ↦ by
    rw [← dual_contract, dual_coloops, ← IsLoop, ← singleton_dep, hI.indep.contract_dep_iff,
      singleton_union, and_iff_right (by simpa using he.2), hI.indep.insert_dep_iff,
      hI.closure_eq_closure]
    exact sdiff_subset_sdiff_left (M.subset_closure X) he

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
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₂
⊢ ∀ a ∈ B₁ \ B₂, ∃ b ∈ B₂ \ B₁, (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) (insert b (B₁ \ {a}))

Tactic:
by
    simp only [mem_sdiff, Sigma.exists, and_imp, Sigma.forall]
    intro i e he₁ he₂
    have hf_ex := (h₁ i).exchange (h₂ i) ⟨he₁, by simpa⟩
    obtain ⟨f, ⟨hf₁, hf₂⟩, hfB⟩ := hf_ex
    refine ⟨i, f, ⟨hf₁, hf₂⟩, fun j ↦ ?_⟩
    rw [← union_singleton, preimage_union, preimage_sdiff]
    obtain (rfl | hne) := eq_or_ne i j
    · simpa only [show ∀ x, {⟨i,x⟩} = Sigma.mk i '' {x} by simp,
        preimage_image_eq _ sigma_mk_injective, union_singleton]
    rw [preimage_singleton_eq_empty.2 (by simpa), preimage_singleton_eq_empty.2 (by simpa),
      sdiff_empty, union_empty]
    exact h₁ j

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

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M.Indep (I ∪ J) ∧ I ∪ J ⊆ R ∪ C) ∧ Disjoint C I

Tactic:
have hJC := hJ'.subset

Goal state after:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
hJC : J ⊆ C
⊢ (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M.Indep (I ∪ J) ∧ I ∪ J ⊆ R ∪ C) ∧ Disjoint C I
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
r : R
a✝ : r ∈ S
⊢ IsRegular 1

Tactic:
exact isRegular_one

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := ⋯
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
⊢ ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) r = 0

Tactic:
· intro x hx
    rw [Iff.symm sub_eq_iff_eq_add'] at hf
    rw [← hf, map_sub, Heval x hx, zero_sub, neg_eq_zero,
      linearCombination_apply, map_finsuppSum, Finsupp.sum, Finset.sum_eq_zero]
    intro i _
    rw [smul_eq_mul, map_mul]
    convert! mul_zero _
    rw [Alon.P, _root_.map_prod]
    apply Finset.prod_eq_zero (hx i)
    simp

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

Tactic:
subst this

Goal state after:
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⟩⟩
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : (p, q) ∈ Finset.antidiagonal t
⊢ coeff (p, q).1 (h i) * coeff (p, q).2 (∏ r ∈ S i, (X i - C r)) = 0

Tactic:
simp only [Finset.mem_antidiagonal] at hpq

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : p + q = t
⊢ coeff (p, q).1 (h i) * coeff (p, q).2 (∏ r ∈ S i, (X i - C r)) = 0