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

Goal state before:
pp: case a
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ m ≤ #s

Tactic:
· exact mod_cast m_le_card_of_mem_chunk_parts (h𝒜 hs)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
⊢ p.dropUntil w h = (p.drop (List.idxOf w p.support)).copy ⋯ ⋯

Tactic:
apply ext_support
  induction p with
  | nil =>
    simp only [dropUntil, eq_mpr_eq_cast, support_nil, getVert_nil, drop, support_copy]
    grind [mem_support_nil_iff, support_nil]
  | @cons a _ _ _ p ih =>
    by_cases! h' : w = a
    · subst h'
      simp [dropUntil_first]
    · rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]
      grind

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
⊢ p.support.Disjoint q.tail.support

Tactic:
have hpq' := hpq.support_nodup

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.append q).support.Nodup
⊢ p.support.Disjoint q.tail.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p✝ : G.Walk v✝ u
hp : (cons h p✝).IsCircuit
⊢ G ≠ ⊥

Tactic:
rintro rfl; exact h

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i = 0

Tactic:
apply hp.getVert_injOn (by rw [Set.mem_ofPred]; lia) (by rw [Set.mem_ofPred]; lia)

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ p.getVert i = p.getVert 0
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(u, w) ∈ p.edges
⊢ w = p.snd

Tactic:
have hnil := edges_eq_nil.not.mp <| List.ne_nil_of_mem hmem
  rw [← cons_tail_eq _ hnil, edges_cons, List.mem_cons, Sym2.eq, Sym2.rel_iff'] at hmem
  have : u ∉ p.tail.support := by induction p <;> simp_all
  grind [fst_mem_support_of_mem_edges]

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
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil

Tactic:
refine ⟨fun hp v w hwp ↦ ?_, fun h ↦ .mk' ?_⟩
  · simp [w.isPath_iff_nil.mp <| isPath_of_isSubwalk hwp hp]
  · refine List.pairwise_iff_getElem.mpr fun i j _ _ _ _ ↦ ?_
    let p' := p.take j |>.drop i
    have : ¬p'.Nil := by grind [nil_drop_iff, take_length]
    have : p'.IsSubwalk p := isSubwalk_drop _ i |>.trans <| p.isSubwalk_take j
    grind [take_getVert, getVert_eq_support_getElem]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : G.CliqueFree n
s t : α
⊢ (G.replaceVertex s t).CliqueFree n

Tactic:
contrapose h
  have ⟨φ, hφ⟩ := topEmbeddingOfNotCliqueFree h
  rw [not_cliqueFree_iff_top_isContained]
  by_cases mt : t ∈ Set.range φ
  · obtain ⟨x, hx⟩ := mt
    by_cases ms : s ∈ Set.range φ
    · obtain ⟨y, hy⟩ := ms
      have e := @hφ x y
      simp_rw [hx, hy, adj_comm, not_adj_replaceVertex_same, top_adj, false_iff, not_ne_iff] at e
      rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h
    · unfold replaceVertex at hφ
      refine Embedding.isContained ⟨φ.setValue x s, fun {a b} ↦ ?_⟩
      simp only [Embedding.coeFn_mk, Embedding.setValue, not_exists.mp ms, ite_false]
      rw [apply_ite (G.Adj · _), apply_ite (G.Adj _ ·), apply_ite (G.Adj _ ·)]
      convert! @hφ a b <;> simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]
  · refine Embedding.isContained ⟨φ, ?_⟩
    simp_rw [Set.mem_range, not_exists, ← ne_eq] at mt
    conv at hφ => enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]
    exact hφ

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsTrail
⊢ p.IsTrail

Tactic:
rw [isTrail_def]

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsTrail
⊢ p.edges.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 ≤ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3

Tactic:
gcongr; exact min_le_left _ _

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

Goal state before:
pp: case one
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * 1 - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = 1 ∧ ↑1 ∣ ∑ i ∈ t, a i

Tactic:
simpa using exists_subset_card_eq hs

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
c : α
hct : c ∈ ofColex (toColex t)
hcs : c ∉ ofColex (toColex s)
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ ofColex (toColex u)
hdt : d ∉ ofColex (toColex t)
hcd : c ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
c : α
hct : c ∈ ofColex (toColex t)
hcs : c ∉ ofColex (toColex s)
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ ofColex (toColex u)
hdt : d ∉ ofColex (toColex t)
hcd : c ≤ d
had : a ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h1 : (crossProduct v) w = 0
⊢ ¬LinearIndependent F ![v, w]

Tactic:
h2

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h1 : (crossProduct v) w = 0
h2 : LinearIndependent F ![v, w]
⊢ False
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
⊢ LinearIndependent K ![D.rep, D'.rep] ↔ D ≠ D'

Tactic:
by
    rw [LinearIndependent.pair_iff' (rep_nonzero _)]
    refine ⟨fun h hD ↦ h 1 (by simp [hD]), fun h a hD ↦ h ?_⟩
    rw [eq_comm, ← mk_rep D, ← mk_rep D', mk_eq_mk_iff]
    suffices a ≠ 0 by refine ⟨(Ne.isUnit this).unit, by simp [← hD]⟩
    exact fun ha ↦ D'.rep_nonzero (by simp [← hD, ha])

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inl
α : 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
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
eq_of_subset_of_card_le this

Goal state after:
case inr.inr.inl
α : 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
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ toColex (s.erase a) ≤ toColex (s.erase a)

case inr.inr.inl
α : 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
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ #(s.erase a) ≤ #(t.erase m)
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

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

Tactic:
rw [← not_iff_not, mk_eq_mk_iff', not_exists, ← LinearIndependent.pair_iff' hw,
    ← crossProduct_ne_zero_iff_linearIndependent, ← cross_anticomm, neg_ne_zero]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
⊢ ∃ s, #s = r ∧ 𝒜 = initSeg s

Tactic:
by
  have hs := sup'_mem (ofColex ⁻¹' 𝒜) (LinearOrder.supClosed _) 𝒜 h𝒜₀ toColex
    (fun a ha ↦ by simpa using ha)
  refine ⟨_, h𝒜.1 hs, ?_⟩
  ext t
  rw [mem_initSeg]
  refine ⟨fun p ↦ ?_, ?_⟩
  · rw [h𝒜.1 p, h𝒜.1 hs]
    exact ⟨rfl, le_sup' _ p⟩
  rintro ⟨cards, le⟩
  obtain p | p := le.eq_or_lt
  · rwa [toColex_inj.1 p]
  · exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩

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
⊢ (v.cross w).orthogonal w

Tactic:
rw [cross_comm]
  exact cross_orthogonal_left h.symm

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ y, ∑ x, lineCount L (x, y).1 = ∑ i ∈ univ ×ˢ univ, pointCount P i.2

Tactic:
Finset.sum_product

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ y, ∑ x, lineCount L (x, y).1 = ∑ x, ∑ y, pointCount P (x, y).2
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
⊢ ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]
    -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
    intro x hx
    have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
    rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(catalan d.succ) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
| ind d hd =>

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

Goal state before:
pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Tactic:
· 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.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (X ^ ((i + 1) * (m + 1))).order

Tactic:
nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ ↑n < (X ^ ((i + 1) * (m + 1))).order
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ≥ x, ∑ z ≥ y, 1 x z * f z = f x

Tactic:
simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ (∑ x_1 > x, if x_1 ≤ x then f x else 0) = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
⊢ i ≤ d → ∃ a ∈ s, a + 1 = i

Tactic:
h2

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ ∃ a ∈ s, a + 1 = i
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
⊢ ¬IsFragment K S ∅

Tactic:
by
  simp [IsFragment, (connectivity_pos hK hS).ne]

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

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

Tactic:
by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;>
      · #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
        we need to re-enable model-based theory combination in `lia` for this to go through. -/
        lia +mbtc

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ Tendsto (fun n ↦ (X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order) atTop (𝓝 ⊤)

Tactic:
nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧)

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
⊢ Tendsto (fun n ↦ (X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order) atTop (𝓝 ⊤)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ Tendsto (fun i ↦ (-X ^ (i + k + 1)).order) atTop (𝓝 ⊤)

Tactic:
nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧)

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
⊢ Tendsto (fun i ↦ (-X ^ (i + k + 1)).order) atTop (𝓝 ⊤)
Module: Mathlib.Combinatorics.Graph.Delete

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

Tactic:
simp only [edgeSet_restrict]

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

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

Tactic:
by
  ext <;> simp

Goal state after:
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)
⊢ map f G = map g G

Tactic:
by
  refine Graph.ext (by grind) fun _ _ _ ↦ ⟨fun ⟨_, _, hvw, _, _⟩ ↦ ?_, fun ⟨_, _, hvw, _, _⟩ ↦ ?_⟩
  <;> grind [h hvw.left_mem, h hvw.right_mem, hvw.map]

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:
closure_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) ∩ (Dᶜ ∩ M.E) = M.closure (X \ D) \ D
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
⊢ x ∈ s →
    ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
            invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
            left_inv := ⋯, right_inv := ⋯ }
          x) <
      #s

Tactic:
intro hx

Goal state after:
case mp
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
⊢ ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
          invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
          left_inv := ⋯, right_inv := ⋯ }
        x) <
    #s
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ (X ∩ M.E) = M ／ I ＼ (X \ I)

Tactic:
hI.isBasis_inter_ground.contract_eq_contract_delete,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ ((X ∩ M.E) \ I) = M ／ I ＼ (X \ I)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
⊢ ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l

Tactic:
cases nonempty_fintype η
  obtain ⟨ι, _, hι⟩ := Line.exists_mono_in_high_dimension (Shrink.{0} η → α) κ
  refine ⟨ι × Shrink η, inferInstance, fun C ↦ ?_⟩
  obtain ⟨l, hl⟩ := hι fun x ↦ C fun (i, e) ↦ x i e
  refine ⟨l.toSubspace.reindex (equivShrink.{0} η).symm (Equiv.refl _) (Equiv.refl _), ?_⟩
  convert! hl.toSubspace.reindex
  simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
⊢ (M ／ C).Dep K

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (C ∩ M.E)

Goal state after:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ (M ／ C).Dep K
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case hlt
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Tactic:
obtain ⟨g, _⟩ := valid.contains
        have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
        exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩

Goal state after:
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 : σ
⊢ m.degree (P S i) = single i #S

Tactic:
by
  simp only [P]
  rw [degree_prod_of_regular]
  · simp [Finset.sum_congr rfl (fun r _ ↦ m.degree_X_sub_C i r)]
  · intro r _
    rw [m.monic_X_sub_C]
    exact isRegular_one

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • ω.size • f ![a, b] < 2 • ω.size • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x ↦ f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False

Tactic:
exact ne_of_lt impos rfl

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

Goal state before:
pp: case cons.inl
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
n : ℕ
hn : n ≤ p'.length + 1
h : n ≤ p'.length
⊢ ∃ v p₁ p₂, p'.cons e = p₁.comp p₂ ∧ p₁.length = n

Tactic:
obtain ⟨d, p₁, p₂, hp, hl⟩ := ih h

Goal state after:
case cons.inl
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
n : ℕ
hn : n ≤ p'.length + 1
h : n ≤ p'.length
d : V
p₁ : Path a d
p₂ : Path d b✝
hp : p' = p₁.comp p₂
hl : p₁.length = n
⊢ ∃ v p₁ p₂, p'.cons e = p₁.comp p₂ ∧ p₁.length = n
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons.cons
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₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (Path.cast ⋯ ⋯ (φ.mapPath p₁)).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
Path.cast_rfl_rfl

Goal state after:
case cons.cons
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₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
A : Finset ℕ
ε : ℝ
hε : 0 < ε
this : ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
hε₁ : ¬ε ≤ 1
n : ℕ
hn : 0 < n
hn' : ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

Tactic:
exact ⟨n, hn, hn'.trans_le (le_of_not_ge hε₁)⟩

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 α
⊢ (s ○ t).Nonempty → t.Nonempty

Tactic:
simp_rw [Finset.Nonempty, mem_disjSups]
  exact fun ⟨_, _, _, b, hb, _⟩ => ⟨b, hb⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ⊼ t)ᶜˢ = sᶜˢ ⊻ tᶜˢ

Tactic:
← image_compl

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ image compl (s ⊼ t) = image compl s ⊻ image compl t