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

Goal state before:
pp: case pos.pos.bit0.bit0
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bit (g false false) (Nat.bitwise g ↑m ↑n)

Tactic:
Nat.bitwise_zero,

Goal state after:
case pos.pos.bit0.bit0
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bit (g false false) (Nat.bitwise g ↑m ↑n)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case zero
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
f : List.Vector Bool 0 → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool 0), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux 0 f)

Tactic:
exact hf _

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case epsilon
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ epsilon.rmatch x = true ↔ x ∈ epsilon.matches'

Tactic:
one_def,

Goal state after:
case epsilon
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
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:
rw [Nat.add_one, iterate_succ']

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 ∘ (Tape.move Dir.right)^[(S k).length]) (Tape.mk' ∅ (addBottom ?m.135)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (write (enc (f (ListBlank.cons a R).head v)).toList (move n Dir.left (trNormal dec q))) v
      (trTape' enc0 L (ListBlank.cons a R)))
    (trCfg enc enc0 (stepAux q v (Tape.write (f (ListBlank.cons a R).head v) (Tape.mk' L (ListBlank.cons a R)))))

Tactic:
stepAux_write,

Goal state after:
case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (move n Dir.left (trNormal dec q)) v (trTape' enc0 (ListBlank.cons (f (ListBlank.cons a R).head v) L) R))
    (trCfg enc enc0 (stepAux q v (Tape.write (f (ListBlank.cons a R).head v) (Tape.mk' L (ListBlank.cons a R)))))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m : Num
n : ℕ
⊢ ↑(m >>> n) = ↑m >>> n

Tactic:
obtain - | m := m

Goal state after:
case zero
n : ℕ
⊢ ↑(zero >>> n) = ↑zero >>> n

case pos
n : ℕ
m : PosNum
⊢ ↑(pos m >>> n) = ↑(pos m) >>> n
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((comp a✝¹ a✝).then k').eval v = (comp a✝¹ a✝).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]

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

Goal state before:
pp: c : Code
h : c.Ok
v : List ℕ
⊢ (do
      let v ← c.eval v
      StateTransition.eval step (Cfg.ret Cont.halt v)) =
    Cfg.halt <$> c.eval v

Tactic:
← bind_pure_comp

Goal state after:
c : Code
h : c.Ok
v : List ℕ
⊢ (do
      let v ← c.eval v
      StateTransition.eval step (Cfg.ret Cont.halt v)) =
    do
    let a ← c.eval v
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mp
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
y : Cfg
h : x ∈ eval step y
IH :
  ∀ (a' : Cfg),
    step y = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ ∀ (v : List ℕ) (c' : Cfg),
    y = c'.then (Cont.fix f k) →
      Reaches step (stepNormal f Cont.halt v) c' →
        ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
rintro v (⟨v'⟩ | ⟨k', v'⟩) rfl hr

Goal state after:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step ((Cfg.halt v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.halt v').then (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

case mp.ret
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step ((Cfg.ret k' v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.ret k' v').then (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.ret k' v')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
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
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
⊢ (List.map ((proj k').f ∘ fun a ↦ update default k (some a)) L.reverse)[i]?.getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i

Tactic:
rw [this, List.getElem?_map, proj, PointedMap.mk_val]

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
⊢ (Option.map (fun a ↦ update default k (some a) k') L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i
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
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp M S
this :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt S q →
      (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
      have :=
        this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
      rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]

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

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal g (Cont.comp f k) v) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [Code.eval, IHg]

Goal state after:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let v ← (fun v ↦ g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

Tactic:
by
  -- suffices to prove for nonempty $G$
  by_cases G_empty : G = ∅
  · simpa only [G_empty, image_empty] using empty_subset _
  · -- let $a \in \rho(G)$
    intro a ha
    rw [mem_closure_iff]
    -- let $N$ be a neighbourhood of $a$
    intro N N_open hN
    -- get $x \in A$ from nonempty open $G \cap \rho^{-1}(N)$
    rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩
    have nonempty : (G ∩ ρ ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr hN⟩
    have is_open : IsOpen <| G ∩ ρ ⁻¹' N := hG.inter <| N_open.preimage ρ_cont
    have ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ :=
      zorn_subset _ (compl_ne_univ.mpr nonempty) is_open.isClosed_compl
    rcases nonempty_compl.mpr ne_univ with ⟨x, hx⟩
    -- prove $x \in N \cap (A \setminus \rho(E \setminus G))$
    have hx' : x ∈ (ρ '' Gᶜ)ᶜ := fun h => hx <| image_mono (by simp) h
    rcases ρ_surj x with ⟨y, rfl⟩
    have hy : y ∈ G ∩ ρ ⁻¹' N := by simpa using mt (mem_image_of_mem ρ) <| mem_compl hx
    exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ (ρ '' univ)ᶜ = ∅

Tactic:
compl_empty_iff,

Goal state after:
A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ ρ '' univ = univ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f

Tactic:
refine ⟨h, h.hom.hom.2, ?_⟩

Goal state after:
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
⊢ g ∘ ⇑(ConcreteCategory.hom h) = f
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mp.refine_1
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
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i ↦ if h : i = j then ⋯.mpr V else Set.univ
⊢ ∀ i ∈ {j}, U i ∈ T i

Tactic:
simp only [Finset.mem_singleton]
      rintro i rfl
      simpa [U]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ
⊢ x ∈ ⋃₀ S

Tactic:
refine ⟨s.1, s.2, ?_⟩

Goal state after:
case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ
⊢ x ∈ ↑s
Module: Mathlib.Topology.Category.CompHausLike.SigmaComparison

Goal state before:
pp: P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
⊢ (ConcreteCategory.hom (sigmaComparison X σ)) x a =
    (ConcreteCategory.hom (Pi.π (fun a ↦ X.obj (Opposite.op (of P (σ a)))) a))
      ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a))))
        ((ConcreteCategory.hom
            (X.map
              (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
                  (productIsProduct fun x ↦ Opposite.op (of P (σ x)))).hom))
          x))

Tactic:
have := ConcreteCategory.congr_hom (piComparison_comp_π X (fun a ↦ ⟨of P (σ a)⟩) a)

Goal state after:
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom
          ((piComparison X fun a ↦ Opposite.op (of P (σ a))) ≫ Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        x =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ (ConcreteCategory.hom (sigmaComparison X σ)) x a =
    (ConcreteCategory.hom (Pi.π (fun a ↦ X.obj (Opposite.op (of P (σ a)))) a))
      ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a))))
        ((ConcreteCategory.hom
            (X.map
              (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
                  (productIsProduct fun x ↦ Opposite.op (of P (σ x)))).hom))
          x))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
⊢ Supports (contSupp k) S

Tactic:
by
  induction k with
  | halt => simp [contSupp_halt, Supports]
  | cons₁ f k IH =>
    have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁
    refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_
    refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩
    simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
    exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
  | cons₂ k IH =>
    have H' := H; rw [contSupp_cons₂] at H'
    exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
  | comp f k IH =>
    have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H'
    exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩
  | fix f k IH =>
    rw [contSupp] at H
    exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

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

Goal state before:
pp: F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝² : PreservesFiniteProducts F
X Y : Profinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (ConcreteCategory.hom (isoFinYonedaComponents F X).inv) (f ∘ ⇑(ConcreteCategory.hom g)) =
    (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)

Tactic:
apply injective_of_mono (isoFinYonedaComponents F X).hom
  simp only [Iso.inv_hom_id_apply]
  ext x
  rw [isoFinYonedaComponents_hom_apply]
  simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

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

Goal state before:
pp: F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (ConcreteCategory.hom (isoFinYonedaComponents F X).inv) (f ∘ ⇑(ConcreteCategory.hom g)) =
    (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)

Tactic:
apply injective_of_mono (isoFinYonedaComponents F X).hom
  simp only [Iso.inv_hom_id_apply]
  ext x
  rw [isoFinYonedaComponents_hom_apply]
  simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

Goal state after: