mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    true

Tactic:
Legacy.Iterator.hasNext_cons_addChar,

Goal state after:
case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case4
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    false

Tactic:
Legacy.Iterator.hasNext_cons_addChar,

Goal state after:
case case4
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    false
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case think
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s✝ : WSeq α
h : c1 = (nil.append s✝.think).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux s✝.think)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append s✝.think).destruct.destruct (nil.destruct.bind (destruct_append.aux s✝.think)).destruct

Tactic:
case think t => exact ⟨nil, t, by simp⟩

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.nil.nil
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f nil.join))) (Seq.destruct (nil.append (map (map f) nil).join))

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
S : WSeq (Computation α)
⊢ List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) []) =
    match
      match
        List.foldr
          (fun c o ↦
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) [] with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.nil
α : Type u
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    nil.join.destruct.destruct nil.join.destruct.destruct

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) nil = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g nil)

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ traverse (pure ∘ f) nil = pure (map f nil)

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (nil.append (nil.append T).join).destruct.destruct (nil.append (nil.join.append T.join)).destruct.destruct

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (nil.append (S.append T).join).destruct.destruct (nil.append (S.join.append T.join)).destruct.destruct

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case nil
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
⊢ (fun {α} ↦ η.app α) (traverse f nil) = traverse (η.app β ∘ f) nil

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.nil
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    nil.join.join.destruct.destruct (map join nil).join.destruct.destruct

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (nil.append (nil.append SS.join).join).destruct.destruct
    (nil.append (nil.join.append (map join SS).join)).destruct.destruct

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (nil.append (S.append SS.join).join).destruct.destruct
    (nil.append (S.join.append (map join SS).join)).destruct.destruct

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ (∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
simp only [inr.injEq, exists_and_left, exists_eq_left']

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr.inr.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₂
hc : c ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

Tactic:
exact inr_mem_disjSum.2 hc

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = s
⊢ mapAccumr₂ f xs ys s = (s, map₂ (fun x y ↦ (f x y s).2) xs ys)

Tactic:
induction xs, ys using revInductionOn₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr f' nil s

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr f' nil s

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: case nil
α : Type u
s : WSeq α
s1 s2 : Computation ℕ
l : List α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, nil) ∧
    s2 =
      Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, nil))
⊢ Computation.BisimO
    (fun c1 c2 ↦
      ∃ l s,
        c1 =
            Computation.corec
              (fun x ↦
                match x with
                | (n, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map List.length
              (Computation.corec
                (fun x ↦
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, nil)).destruct
    (Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, nil))).destruct

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ ↑n * ⌊f 0⌋ ≤ ⌊(⇑f)^[n] 0⌋

Tactic:
rw [le_floor, Int.cast_mul, Int.cast_natCast, ← zero_add ((n : ℝ) * _)]
  apply le_iterate_of_add_int_le_map
  simp [floor_le]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n

Tactic:
rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this

Goal state after:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : τ f * ↑n = ↑m
⊢ ↑n ≠ 0
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
U : Finset G
x y : G → A
⊢ y ∈ cylinder U x ↔ y ∈ (↑U).pi fun i ↦ {x i}

Tactic:
simp [cylinder, Set.pi]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
hU : dom = U
⊢ (fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩)
      ((fun p i ↦ (↑p).config ↑i) ⟨{ config := cfg, support := dom, condition := cond }, hU⟩) =
    ⟨{ config := cfg, support := dom, condition := cond }, hU⟩

Tactic:
subst hU

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
⊢ (fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ dom then f ⟨g, h⟩ else default, support := dom, condition := ⋯ }, ⋯⟩)
      ((fun p i ↦ (↑p).config ↑i) ⟨{ config := cfg, support := dom, condition := cond }, ⋯⟩) =
    ⟨{ config := cfg, support := dom, condition := cond }, ⋯⟩
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen[inst✝¹] n
hn₂ : ω f ϕ s ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n

Tactic:
rcases eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset f ϕ s hc₁
      hc₂ hn₁ hn₂ with
    ⟨u, hu_mem, hu⟩

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen[inst✝¹] n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure[inst✝¹] (image2 ϕ u s) ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)).Nonempty

pp: case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

pp: case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
· intro u
    have hn : (image2 ϕ (u ∩ v) s).Nonempty :=
      Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
    exact hn.mono subset_closure

Goal state after:
case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : F = ∅
⊢ netMaxcard T F U n = 0

Tactic:
by rw [h, netMaxcard_empty]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬↑(netMaxcard T F U 0) = 0 0

Tactic:
netMaxcard_zero T h U,

Goal state after:
case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬↑1 = 0 0
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
· obtain ⟨V, V_uni, V_symm, V_comp_U⟩ := comp_symm_mem_uniformity_sets U_uni
    apply (coverEntropyEntourage_antitone T F V_comp_U).trans (le_iSup₂_of_le V V_uni _)
    have := isRefl_of_mem_uniformity V_uni
    exact coverEntropyEntourage_le_netEntropyEntourage T F

Goal state after:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F
Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a b : G
⊢ ((fun x1 x2 ↦ x1 * x2) a b)⁻¹ * (fun x1 x2 ↦ x1 * x2) b a ∈ (commutator G).topologicalClosure

Tactic:
by
          have h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆ := by group
          rw [h]
          exact Subgroup.le_topologicalClosure _ (Subgroup.commutator_mem_commutator
            (Subgroup.mem_top b⁻¹) (Subgroup.mem_top a⁻¹))

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
K' : Type u
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
hv : IsTranscendenceBasis R v'
⊢ #K' ≤ max (max #R #ι') ℵ₀

Tactic:
by
  simpa using cardinal_le_max_transcendence_basis v' hv

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ (refl L M) x = x

Tactic:
by simp [refl]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ []).Realize v xs ↔ ∀ φ ∈ [], φ.Realize v xs

Tactic:
| nil =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ []).Realize v xs ↔ ∃ φ ∈ [], φ.Realize v xs

Tactic:
| nil =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case nil
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode []) = []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case nil
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (flatMap (fun i ↦ (ts i).listEncode) [] ++ l) = List.map ts [] ++ listDecode l

Tactic:
| nil =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_1
L : Language
α : Type u'
i j : ℕ
ij : (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) i = (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) j
⊢ i = j

Tactic:
cases ij

Goal state after:
case refine_2.refine_1.refl
L : Language
α : Type u'
i : ℕ
⊢ i = i
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case nil
L : Language
α : Type u'
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'
⊢ listDecode (flatMap (fun φ ↦ φ.snd.listEncode) []) = []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ ((relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs

Tactic:
simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ (mapTermRel (fun n ↦ ⇑(Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n))))) (fun n ↦ id) (fun x ↦ id)
          φ).Realize
      v xs ↔
    φ.Realize (v ∘ ⇑g) xs
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ ∃ y, f y = n

Tactic:
exact ⟨f.symm n, apply_symm_apply _ _⟩

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (⋂ i ∈ s, f i)

Tactic:
rw [← Finset.inf_set_eq_iInter]
  exact definable_finset_inf hf s

Goal state after: