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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.darts.Nodup
h : (cons h✝ p').support.Nodup
⊢ (cons h✝ p').darts.Nodup

Tactic:
simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.darts.Nodup
h : u✝ ∉ p'.support ∧ p'.support.Nodup
⊢ { fst := u✝, snd := v✝, adj := h✝ } ∉ p'.darts ∧ p'.darts.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
⊢ (p.takeUntil (p.getVert n) h).support[n] ∈ (p.takeUntil (p.getVert n) h).support.dropLast

Tactic:
← List.getElem_dropLast h₁,

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
⊢ (p.takeUntil (p.getVert n) h).support.dropLast[n] ∈ (p.takeUntil (p.getVert n) h).support.dropLast
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
obtain ⟨a, b, c, -, -, -, hs⟩ := card_eq_three.1 h.card_eq

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∉ S
⊢ ∃ i ∈ s, (eval x) (f i) ≠ 0

Tactic:
simpa [hS, not_forall, Classical.not_imp] using hx

Goal state after:
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
u v : ℙ K V
h : u.submodule = v.submodule
⊢ u = v

Tactic:
by
  induction u using ind with | h u hu =>
  induction v using ind with | h v hv =>
  rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
  exact ((mk_eq_mk_iff K v u hv hu).2 h).symm

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ : toColex t₂ < toColex t₁ ∧ #t₂ = #s
⊢ toColex t₂ ≤ toColex s

Tactic:
mem_initSeg

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : #s = #t₁ ∧ toColex t₁ ≤ toColex s
ht₂ : toColex t₂ < toColex t₁ ∧ #t₂ = #s
⊢ toColex t₂ ≤ toColex s
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ t ∈ initSeg (𝒜.sup' h𝒜₀ ⇑toColex)

Tactic:
mem_initSeg

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ #(𝒜.sup' h𝒜₀ ⇑toColex) = #t ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
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:
exact cross_orthogonal_right h

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p✝ q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
p : P
h₂ : p ∈ l₂
⊢ lineCount L p = n

Tactic:
refine or_not.elim (fun h₃ => ?_) fun h₃ => (HasLines.lineCount_eq_pointCount h h₃).trans hl₃

Goal state after:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p✝ q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
p : P
h₂ : p ∈ l₂
h₃ : p ∈ l₃
⊢ lineCount L p = n
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ 1 ∈ ↑A⁻¹ * ↑A

Tactic:
have ⟨x, hx⟩ : A.Nonempty := nonempty_of_doubling h

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x✝ y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
hx : x ∈ A
⊢ 1 ∈ ↑A⁻¹ * ↑A
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)) < 3 / 2 * ↑(#A)
⊢ ↑(A.invMulSubgroup h) = ↑A * ↑A⁻¹

Tactic:
rw [invMulSubgroup_eq_inv_mul, eq_comm]
  norm_cast
  exact mul_inv_eq_inv_mul_of_doubling_lt_two (by qify at h ⊢; linarith)

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

Goal state before:
pp: n : ℕ
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Tactic:
simp only [gosperCatalan, tsub_self, Nat.centralBinom_zero, Nat.cast_one, mul_one, Nat.cast_add,
    Nat.sub_zero, one_mul, Nat.cast_zero, mul_zero, zero_sub, neg_add_rev]

Goal state after:
n : ℕ
⊢ ↑(n + 1).centralBinom * (2 * (↑n + 1) - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑(n + 1).centralBinom * (-1 + -↑n) / (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑(n + 1).centralBinom / (↑n + 2)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).1 < n.succ

pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n.succ

Tactic:
· simp_wf; have := fst_le ijh.2; lia

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n.succ
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}, (count x (replicate m n))!

Tactic:
simp only [Finset.prod_singleton, count_replicate_self]

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ x, n.choose ↑x.fst * ((↑x.snd).parts.erase (↑x.fst + 1)).bell =
    ∑ x, n.choose (↑x.snd - 1) * (x.fst.parts.erase ↑x.snd).bell

Tactic:
refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_

Goal state after:
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∀ (x : (i : Fin n.succ) × { p // ↑i + 1 ∈ p.parts }),
    n.choose ↑x.fst * ((↑x.snd).parts.erase (↑x.fst + 1)).bell =
      n.choose (↑(n.sigmaPartitionWithPartEquiv x).snd - 1) *
        ((n.sigmaPartitionWithPartEquiv x).fst.parts.erase ↑(n.sigmaPartitionWithPartEquiv x).snd).bell
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := ⋯
H : Subgroup G := ⋯
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
⊢ A ∩ z⁻¹ •> A ⊆ z⁻¹ •> A

Tactic:
exact inter_subset_right

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

Goal state before:
pp: case h'
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := ⋯
H : Subgroup G := ⋯
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
⊢ A ∩ w •> A ⊆ w •> A

Tactic:
exact inter_subset_right

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

Goal state before:
pp: case refine_1
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 ↦ x ^ ((k + 1) * x_1)) atTop (𝓝 0)

Tactic:
exact hx.comp (strictMono_mul_left_of_pos (by simp)).tendsto_atTop

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

Goal state before:
pp: n : ℕ
x✝ : n + 2 ≠ 0
⊢ Even ((n + 1).largeSchroder + ∑ i ≤ n + 1, i.largeSchroder * (n + 1 - i).largeSchroder)

Tactic:
refine .add (even_largeSchroder n.succ_ne_zero) <| even_sum _ fun k hk ↦ ?_

Goal state after:
n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k ∈ Iic (n + 1)
⊢ Even (k.largeSchroder * (n + 1 - k).largeSchroder)
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia

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

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

Tactic:
#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.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
⊢ 1 ∈ n⁻¹ •> N

Tactic:
simpa [mem_inv_smul_finset_iff]

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

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0

Tactic:
#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.Schroder

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0

Tactic:
#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.Graph.Delete

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H.restrict F) ⊆ E(G.restrict F)

Tactic:
simp [inter_subset_left.trans h.edgeSet_mono]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.Inc e x
⊢ G.IsLoopAt e x ∨ G.IsNonloopAt e x

Tactic:
simp [isNonloopAt_iff_inc_not_isLoopAt, h, em]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y

Tactic:
simp_rw [← hIsLink, ← hedgeSet]

Goal state after:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ E(G) ↔ ∃ x y, G.IsLink e x y
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case refine_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) ∅
⊢ (⋂₀ ∅).Nonempty

Tactic:
rw [Set.sInter_empty]

Goal state after:
case refine_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) ∅
⊢ Set.univ.Nonempty
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
⊢ (∃ c, ∀ (x : η' → α'), (C fun x_1 ↦ eα (Sum.elim id (⇑eα.symm ∘ x ∘ ⇑eη) (l.idxFun (eι.symm x_1)))) = c) ↔
    ∃ c, ∀ (x : η → α), C (⇑eα ∘ ↑l x ∘ ⇑eι.symm) = c

Tactic:
exact exists_congr fun c ↦ (eη.arrowCongr eα).symm.forall_congr <| by aesop

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

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

Tactic:
funext i
  cases i <;> rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

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

Tactic:
funext i
  cases i <;> rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

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

Tactic:
funext i
  cases i <;> rfl

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2.htd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
⊢ U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)} → U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}

Tactic:
hU

Goal state after:
case refine_2.htd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
⊢ U ∈ S → ∀ y ∈ S, U * y ∈ S

Tactic:
hU

Goal state after:
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
⊢ ∀ y ∈ S, U * y ∈ S
Module: Mathlib.Combinatorics.Hindman

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

Tactic:
Stream'.corec_eq,

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

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

Tactic:
exact Set.inter_subset_left (Set.Nonempty.some_mem _)

Goal state after:
Module: Mathlib.Combinatorics.Hindman

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

Tactic:
Stream'.corec_eq,

Goal state after:
case h.tail'
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.cons (elem p) (Stream'.corec elem succ (succ p))).tail = Stream'.corec elem succ (succ p)
Module: Mathlib.Combinatorics.Hindman

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

Tactic:
Stream'.corec_eq,

Goal state after:
case h.cons'.refine_1
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.cons (elem p) (Stream'.corec elem succ (succ p))).tail = Stream'.corec elem succ (succ p)
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
⊢ M ／ C ＼ D = M ／ (C ∩ M.E) ＼ ((D ∩ M.E) \ C)

Tactic:
by simp [delete_eq_delete_iff, inter_assoc, inter_sdiff_assoc]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ (M ／ C ＼ D).E
⊢ M = M ／ C ＼ D

Tactic:
rw [delete_ground, contract_ground, subset_sdiff, subset_sdiff] at hE

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ／ C ＼ D
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case pos
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
⊢ (fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩))
      ((fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s)) x) =
    x

Tactic:
have : g ⟨x, hx⟩ < #s := by simpa using (g ⟨x, hx⟩).2
          simp [hx, this]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b

Tactic:
classical
    rw [degree_monomial, if_neg]
    · ext d
      rw [tsub_add_cancel_of_le hbf]
    · simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → ↥S) → κ), ∃ l, Line.IsMono C l
⊢ ∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c

Tactic:
specialize hι fun v => C <| ∑ i, v i

Goal state after:
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∃ l, Line.IsMono (fun v ↦ C (∑ i, ↑(v i))) l
⊢ ∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ K ⊆ I ∪ X

Tactic:
rwa [union_comm]

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

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

Tactic:
wlog hCE : C ⊆ M.E with aux

Goal state after:
case inr
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α), ∀ C ⊆ M.E, M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)