mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))

Tactic:
rintro (_ | _)

Goal state after:
case pbb.false
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))

case pbb.true
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0

Tactic:
rintro (_ | _)

Goal state after:
case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case h.right.head
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: t ≠ [] ∧ P.rmatch (a :: t) = true

Tactic:
simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]

Goal state after:
case h.right.head
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ (P.deriv a).rmatch t = true
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0

Tactic:
rintro (_ | _)

Goal state after:
case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0

Tactic:
rintro (_ | _)

Goal state after:
case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0

Tactic:
rintro (_ | _)

Goal state after:
case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0

Tactic:
rintro (_ | _)

Goal state after:
case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0

Tactic:
rintro (_ | _)

Goal state after:
case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.one
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)

Tactic:
rintro (_ | _)

Goal state after:
case fnn.one.one
⊢ pos one ||| pos one = pos (one.lor one)

case fnn.one.bit1
a✝ : PosNum
⊢ pos one ||| pos a✝.bit1 = pos (one.lor a✝.bit1)

case fnn.one.bit0
a✝ : PosNum
⊢ pos one ||| pos a✝.bit0 = pos (one.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit1
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit1 ||| pos n = pos (a✝.bit1.lor n)

Tactic:
rintro (_ | _)

Goal state after:
case fnn.bit1.one
a✝ : PosNum
⊢ pos a✝.bit1 ||| pos one = pos (a✝.bit1.lor one)

case fnn.bit1.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit1 = pos (a✝¹.bit1.lor a✝.bit1)

case fnn.bit1.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit0 = pos (a✝¹.bit1.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit0
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit0 ||| pos n = pos (a✝.bit0.lor n)

Tactic:
rintro (_ | _)

Goal state after:
case fnn.bit0.one
a✝ : PosNum
⊢ pos a✝.bit0 ||| pos one = pos (a✝.bit0.lor one)

case fnn.bit0.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit1 = pos (a✝¹.bit0.lor a✝.bit1)

case fnn.bit0.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit0 = pos (a✝¹.bit0.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.false
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)

Tactic:
rintro (_ | _)

Goal state after:
case p1b.false.one
⊢ pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)

case p1b.false.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit1)) = bit (true || false) (bif false || true then pos a✝.bit1 else 0)

case p1b.false.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit0)) = bit (true || false) (bif false || true then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.true
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)

Tactic:
rintro (_ | _)

Goal state after:
case p1b.true.one
⊢ pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)

case p1b.true.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit1)) = bit (true || true) (bif false || true then pos a✝.bit1 else 0)

case p1b.true.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit0)) = bit (true || true) (bif false || true then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.false
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)

Tactic:
rintro (_ | _)

Goal state after:
case pb1.false.one
⊢ pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)

case pb1.false.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit1).lor 1) = bit (false || true) (bif true || false then pos a✝.bit1 else 0)

case pb1.false.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit0).lor 1) = bit (false || true) (bif true || false then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.true
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)

Tactic:
rintro (_ | _)

Goal state after:
case pb1.true.one
⊢ pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)

case pb1.true.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit1).lor 1) = bit (true || true) (bif true || false then pos a✝.bit1 else 0)

case pb1.true.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit0).lor 1) = bit (true || true) (bif true || false then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.false
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))

Tactic:
rintro (_ | _)

Goal state after:
case pbb.false.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))

case pbb.false.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (pos (m.lor n))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n (addBottom L) = addBottom (ListBlank.modifyNth f n L)

Tactic:
cases n <;>
    simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]
  congr; symm; apply ListBlank.map_modifyNth; intro; rfl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.true
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))

Tactic:
rintro (_ | _)

Goal state after:
case pbb.true.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))

case pbb.true.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (pos (m.lor n))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₁ l₂ : List Bool
f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
    stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
induction l₂ generalizing l₁ with

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k (some (f v))) (S k).length L))))) =
    TM1.stepAux q v ((Tape.move Dir.right)^[(S k).length + 1] (Tape.mk' ∅ (addBottom ?m.135)))

Tactic:
Nat.add_one,

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k (some (f v))) (S k).length L))))) =
    TM1.stepAux q v ((Tape.move Dir.right)^[(S k).length.succ] (Tape.mk' ∅ (addBottom ?m.135)))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
v : List.Vector ℕ m
⊢ nil.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v

Tactic:
simp [Vector.mOfFn]

Goal state after:
m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
v : List.Vector ℕ m
⊢ Part.some [] = Subtype.val <$> Part.some Vector.nil
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ range (Subtype.val ∘ Subtype.val) = interior s

Tactic:
Set.range_comp,

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ Subtype.val '' range Subtype.val = interior s
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
⊢ X '' ⋂ c, ↑c = univ

Tactic:
by_cases hC : Nonempty C

Goal state after:
case pos
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
⊢ X '' ⋂ c, ↑c = univ

case neg
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : ¬Nonempty ↑C
⊢ X '' ⋂ c, ↑c = univ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit0.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d }
        { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }

Tactic:
refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩

Goal state after:
case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ { l := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d } ∈
    TM2.step tr { l := some q.succ, var := s, stk := elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d }
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (((image fun t ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X)

Tactic:
rw [comp_finsetClopens]

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective fun x ↦
    match x with
    | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
⊢ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V} =
    {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}

Tactic:
ext U0

Goal state after:
case e'_3
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V} ↔
    U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
⊢ ∃ b₂,
    TrCfg (stepRet k v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

pp: case neg
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
⊢ ∃ b₂,
    TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

Tactic:
· obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?
      refine ⟨c, h₁, TransGen.head rfl ?_⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]
      exact h₂

Goal state after:
case neg
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
⊢ ∃ b₂,
    TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: f g : Code
k : Cont'
⊢ codeSupp (f.comp g) k = trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k)

Tactic:
simp only [codeSupp, codeSupp', trNormal, Finset.union_assoc, contSupp]
  rw [← Finset.union_assoc _ _ (contSupp k),
    Finset.union_eq_right.2 (codeSupp'_self _ _)]

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_1.none.some
m : ℕ
h : 0 = ↑m + 1
⊢ none = Option.some m

Tactic:
assumption_mod_cast

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_1.some.none
n : ℕ
h : ↑n + 1 = 0
⊢ Option.some n = none

Tactic:
assumption_mod_cast

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ lanPresheaf F ≅ F

Tactic:
by
  refine NatIso.ofComponents
    (fun ⟨S⟩ ↦ (lanPresheafIso (hF S))) fun _ ↦ ?_
  simp only [lanPresheaf, pointwiseLeftKanExtension_map,
    lanPresheafIso_hom, Opposite.op_unop]
  exact colimit.hom_ext fun _ ↦ (by simp)

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
S : CompHausᵒᵖ
x : X.obj.obj S
⊢ Continuous fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x

Tactic:
suffices ∀ (i : (T : CompHaus.{u}) × X.obj.obj ⟨T⟩),
          Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
        rw [← continuous_sigma_iff]
        apply continuous_coinduced_rng

Goal state after:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P.toCondensed ⊗ S'.toCondensed) ⟶ A
hh :
  (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet P S').inv ≫
      (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫
        (free R).map (μIso lightProfiniteToLightCondSet P S).hom ≫ g

Tactic:
simp [-map_comp, ← map_comp_assoc]

Goal state after:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S ⊗ P).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P.toCondensed) ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet S' P).inv ≫
      (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
        (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g

Tactic:
simp [-map_comp, ← map_comp_assoc]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ P (g <$$> u)

Tactic:
h₁

Goal state after:
case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ q (f <$$> g <$$> u)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ LiftR' (α.RelLast' rr) x y ↔ LiftR (α.RelLast rr) x y

Tactic:
dsimp only [LiftR, LiftR']

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ (∃ u, (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y) ↔
    ∃ u, (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
C : TypeVec.{?u.15} (n + 1) → Sort u
H : (α : TypeVec.{?u.15} n) → (β : Type ?u.15) → C (α ::: β)
γ : TypeVec.{?u.15} (n + 1)
⊢ C γ

Tactic:
rw [← @append1_drop_last _ γ]

Goal state after:
n : ℕ
C : TypeVec.{?u.15} (n + 1) → Sort u
H : (α : TypeVec.{?u.15} n) → (β : Type ?u.15) → C (α ::: β)
γ : TypeVec.{?u.15} (n + 1)
⊢ C (γ.drop ::: γ.last)