mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
n : ℤ
inst✝ : t.IsLE X n
a✝ : ℤ
⊢ t.IsLE ((t.eTruncGE.obj (WithBotTop.coe a✝)).obj X) n

Tactic:
dsimp

Goal state after:
case coe
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
n : ℤ
inst✝ : t.IsLE X n
a✝ : ℤ
⊢ t.IsLE ((t.truncGE a✝).obj X) n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X) ≫
      (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X) ≫ (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTGEIsoGELT a b).hom.app X ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X) ≫
      (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X) ≫ (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTGEIsoGELT a b).hom.app X ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α),
    x ∈ A ∧ { toFun := singleton, inj' := ⋯ } x = u →
      ∀ (x : α), x ∈ A ∧ { toFun := singleton, inj' := ⋯ } x = v → u ≠ v → G.IsUniform ε u v

Tactic:
dsimp

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α), x ∈ A ∧ {x} = u → ∀ (x : α), x ∈ A ∧ {x} = v → ¬u = v → G.IsUniform ε u v
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ G.edgeDensity s t + Gᶜ.edgeDensity s t = 1

Tactic:
by
  rw [edgeDensity_def, edgeDensity_def, ← add_div, div_eq_one_iff_eq]
  · exact mod_cast card_interedges_add_card_interedges_compl _ h
  · positivity

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ δ✝ : 𝕜
u v : Finset α
ε δ : 𝕜
a b : α
ab : G.Adj a b
U : Finset α
UP : U ∈ P.parts
V : Finset α
VP : V ∈ P.parts
xU : a ∈ U
yV : b ∈ V
UV : U ≠ V
GUV : G.IsUniform ε U V
εUV : δ ≤ ↑(G.edgeDensity U V)
⊢ δ ≤ ↑(G.edgeDensity V U)

Tactic:
edgeDensity_comm

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ δ✝ : 𝕜
u v : Finset α
ε δ : 𝕜
a b : α
ab : G.Adj a b
U : Finset α
UP : U ∈ P.parts
V : Finset α
VP : V ∈ P.parts
xU : a ∈ U
yV : b ∈ V
UV : U ≠ V
GUV : G.IsUniform ε U V
εUV : δ ≤ ↑(G.edgeDensity U V)
⊢ δ ≤ ↑(G.edgeDensity U V)
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.edgeFinset \ G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) =
    #G.edgeFinset + G.degree s - G.degree t

Tactic:
card_sdiff_of_subset inc,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset - #(G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) =
    #G.edgeFinset + G.degree s - G.degree t
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.edgeFinset \ G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
card_sdiff_of_subset inc,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset - #(G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
hi : i < p.darts.length
⊢ p.darts[i].toProd.2 = p.support.tail[i]

Tactic:
by
  grind [map_snd_darts]

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

Goal state before:
pp: case nil.mp
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ nil.IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv

Tactic:
rintro ⟨_ | _, _, ⟨⟩⟩

Goal state after:
case nil.mp.nil
V : Type u_1
G : SimpleGraph V
u : V
⊢ ∃ (hu : u = u) (hv : u = u), nil = nil.copy hu hv
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length < k
⊢ p.support[k]? = q.support[k]?

Tactic:
replace hk : p.length + 1 ≤ k := hk

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length + 1 ≤ k
⊢ p.support[k]? = q.support[k]?
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
x✝ : α
⊢ (∃ (x : x✝ ∈ F), ⟨x✝, ⋯⟩ ∈ A) → ∀ ⦃y : α⦄, (∃ (x : y ∈ F), ⟨y, ⋯⟩ ∈ A) → x✝ ≠ y → G.Adj x✝ y

Tactic:
⟨_, ainA⟩

Goal state after:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
⊢ ∀ ⦃y : α⦄, (∃ (x : y ∈ F), ⟨y, ⋯⟩ ∈ A) → x✝ ≠ y → G.Adj x✝ y
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ Set.InjOn p.getVert {i | i ≤ p.length - 1}

Tactic:
by
  intro n hn m hm hnm
  simp only [Set.mem_ofPred_eq] at *
  have := hpc.three_le_length
  have : p.length - n = p.length - m := Walk.length_reverse _ ▸ hpc.reverse.getVert_injOn
    (by simp only [Walk.length_reverse, Set.mem_ofPred_eq]; lia)
    (by simp only [Walk.length_reverse, Set.mem_ofPred_eq]; lia)
    (by simp [Walk.getVert_reverse, show p.length - (p.length - n) = n by lia, hnm,
      show p.length - (p.length - m) = m by lia])
  lia

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
⊢ (SimpleGraph.map (⇑e) G).cliqueSet 1 = map e.toEmbedding '' G.cliqueSet 1

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Tactic:
· ext
    simp [e.exists_congr_left]

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n
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'
hinj : Injective ⇑f
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Path.map f hinj ⟨p, hp⟩ = Path.map f hinj ⟨p', hp'⟩
⊢ ⟨p, hp⟩ = ⟨p', hp'⟩

Tactic:
simp only [Path.map, Subtype.mk.injEq] at h

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Walk.map f p = Walk.map f p'
⊢ ⟨p, hp⟩ = ⟨p', hp'⟩
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - 1 / 10) * (1 - 9⁻¹) * ε ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (↑(#(G.nonuniformWitness ε U V)) / ↑(#U))

Tactic:
gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ ∑ b ∈ insert a B, b = a +ᵥ ∑ b ∈ B, b

Tactic:
rw [sum_insert (fun h => a_notin_A (hB h))]; simp

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

Goal state before:
pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ↑(m * n) ∣ ∑ x ∈ ℬ, ∑ i ∈ x, a i

pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ (↑ℬ).PairwiseDisjoint fun x ↦ x

Tactic:
Int.natCast_mul,

Goal state after:
case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ↑m * ↑n ∣ ∑ x ∈ ℬ, ∑ i ∈ x, a i

case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ (↑ℬ).PairwiseDisjoint fun x ↦ x
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x

Tactic:
let instTop (a : α) : TopologicalSpace (β a) := ⊥
  have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
  let e (s : Finset α) : Set ((a : α) → β a) := {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
  have (s : Finset α) : s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ x, f x = g t x} = e s := by simp [e]
  have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
  have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_ofPred_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
  simpa using! CompactSpace.iInter_nonempty he' he''

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 =
    ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 2 -
        ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 1 +
      (v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2 -
        v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1)

Tactic:
dsimp

Goal state after:
case h₀
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 1 * (v 0 * w 1 - v 1 * w 0) - u 2 * (v 2 * w 0 - v 0 * w 2) =
    (u 2 * v 0 - u 0 * v 2) * w 2 - (u 0 * v 1 - u 1 * v 0) * w 1 +
      (v 1 * (u 0 * w 1 - u 1 * w 0) - v 2 * (u 2 * w 0 - u 0 * w 2))
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
      u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 0 -
        ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 2 +
      (v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0 -
        v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2)

Tactic:
dsimp

Goal state after:
case h₁
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 2 * (v 1 * w 2 - v 2 * w 1) - u 0 * (v 0 * w 1 - v 1 * w 0) =
    (u 0 * v 1 - u 1 * v 0) * w 0 - (u 1 * v 2 - u 2 * v 1) * w 2 +
      (v 2 * (u 1 * w 2 - u 2 * w 1) - v 0 * (u 0 * w 1 - u 1 * w 0))
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s ≤ toColex t ↔ ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩
  · set m := (s ∆ t).max' (symmDiff_nonempty.2 hst)
    by_contra hmt
    have hms : m ∈ s := by
      simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst
    have ⟨b, hbt, hbs, hmb⟩ := h hms hmt
    exact lt_irrefl _ <| (max'_lt_iff _ _).1 (hmb.lt_of_ne <| ne_of_mem_of_not_mem hms hbs) _ <|
      mem_symmDiff.2 <| Or.inr ⟨hbt, hbs⟩
  · 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.CrossProduct

Goal state before:
pp: case h₂
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
      u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 =
    ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 1 -
        ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 0 +
      (v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1 -
        v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0)

Tactic:
dsimp

Goal state after:
case h₂
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 2 * w 0 - v 0 * w 2) - u 1 * (v 1 * w 2 - v 2 * w 1) =
    (u 1 * v 2 - u 2 * v 1) * w 1 - (u 2 * v 0 - u 0 * v 2) * w 0 +
      (v 0 * (u 2 * w 0 - u 0 * w 2) - v 1 * (u 1 * w 2 - u 2 * w 1))
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : 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
b : α
hb : b ∈ t.erase m
⊢ b ∈ s.erase a

Tactic:
mem_erase

Goal state after:
α : 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
b : α
hb : b ≠ m ∧ b ∈ t
⊢ b ≠ a ∧ b ∈ s
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D ≠ D'
⊢ LinearIndepOn K id {D.rep, D'.rep}

Tactic:
← linearIndependent_pair_iff_ne,

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : LinearIndependent K ![D.rep, D'.rep]
⊢ LinearIndepOn K id {D.rep, D'.rep}
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ Injective fun s ↦ ∑ i ∈ s, n ^ i

Tactic:
intro _ _ h
  rwa [le_antisymm_iff, geomSum_le_geomSum_iff_toColex_le_toColex hn,
    geomSum_le_geomSum_iff_toColex_le_toColex hn, ← le_antisymm_iff] at h

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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ x, lineCount L ({ toFun := f, inj' := hf₁ } x)

Tactic:
dsimp

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((n + 1) * (x + 1).ascFactorial (n - x))

Tactic:
Int.natCast_mul,

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * (↑(n + 1) * ↑((x + 1).ascFactorial (n - x)))
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: case h
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst✝ : Nonempty V
v : V
⊢ ⊥ ≠ ⊤

Tactic:
exact ne_of_apply_ne (·.Adj v v) (by simp)

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1) =
    (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !

Tactic:
bell_mul_eq_lemma hx

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = take 1 (↑p).dropLast ++ drop 1 (↑p).dropLast ++ [(↑p).getLast h']

Tactic:
rw [getLast_eq_D, drop_one, this, head_eq_U]

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = [U] ++ (↑p).dropLast.tail ++ [D]
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: 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 : 0 < K
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

Tactic:
have hK₀ : 0 < K := by positivity

Goal state after:
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
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
hn : p.IsNested
i : ℕ
⊢ count D (List.take i (↑p).dropLast.tail) ≤ count U (List.take i (↑p).dropLast.tail)

Tactic:
by
    replace h := toList_ne_nil.mpr hn.1
    have l1 : p.toList.take 1 = [p.toList.head h] := by rcases p with - | - <;> tauto
    have l3 : p.toList.length - 1 = p.toList.length - 1 - 1 + 1 := by
      rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
      · tauto
      · rename_i bal _
        cases s <;> simp at bal
      · tauto
    rw [← drop_one, take_drop, dropLast_eq_take, take_take]
    have ub : min (1 + i) (p.toList.length - 1) < p.toList.length :=
      (min_le_right _ p.toList.length.pred).trans_lt (Nat.pred_lt ((length_pos_iff.mpr h).ne'))
    have lb : 0 < min (1 + i) (p.toList.length - 1) := by omega
    have eq := hn.2 lb ub
    set j := min (1 + i) (p.toList.length - 1)
    rw [← (p.toList.take j).take_append_drop 1, count_append, count_append, take_take,
      min_eq_left (by lia), l1, head_eq_U] at eq
    simp only [count_singleton', ite_true] at eq
    lia

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

Goal state before:
pp: case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ (p + q).firstReturn = p.firstReturn

Tactic:
rw [firstReturn, findIdx_eq]

Goal state after:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ decide
        (count U (List.take ((range (↑(p + q)).length)[p.firstReturn] + 1) ↑(p + q)) =
          count D (List.take ((range (↑(p + q)).length)[p.firstReturn] + 1) ↑(p + q))) =
      true ∧
    ∀ (j : ℕ) (hji : j < p.firstReturn),
      decide
          (count U (List.take ((range (↑(p + q)).length)[j] + 1) ↑(p + q)) =
            count D (List.take ((range (↑(p + q)).length)[j] + 1) ↑(p + q))) =
        false

case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (range (↑(p + q)).length).length