mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Unit
p : ℕ
⊢ G
      (x✝,
          List.map
            (fun n ↦
              let a := ofNat (ℕ × Code) n;
              List.map (evaln a.1 a.2) (List.range a.1))
            (List.range p)).2 =
    some
      (let a := ofNat (ℕ × Code) p;
      List.map (evaln a.1 a.2) (List.range a.1))

Tactic:
simp only [G, prod_ofNat_val, ofNat_nat, List.length_map, List.length_range,
        Nat.pair_unpair, Option.some_inj]
      refine List.map_congr_left fun n => ?_
      have : List.range p = List.range (Nat.pair p.unpair.1 (encode (ofNat Code p.unpair.2))) := by
        simp
      rw [this]
      generalize p.unpair.1 = k
      generalize ofNat Code p.unpair.2 = c
      intro nk
      rcases k with - | k'
      · simp [evaln]
      let k := k' + 1
      simp only
      simp only [List.mem_range, Nat.lt_succ_iff] at nk
      have hg :
        ∀ {k' c' n},
          Nat.pair k' (encode c') < Nat.pair k (encode c) →
            lup ((List.range (Nat.pair k (encode c))).map fun n =>
              (List.range n.unpair.1).map (evaln n.unpair.1 (ofNat Code n.unpair.2))) (k', c') n =
            evaln k' c' n := by
        intro k₁ c₁ n₁ hl
        simp [lup, List.getElem?_range hl, evaln_map, Bind.bind, Option.bind_map]
      obtain - | - | - | - | ⟨cf, cg⟩ | ⟨cf, cg⟩ | ⟨cf, cg⟩ | cf := c <;>
        simp [evaln, nk, Bind.bind, Functor.map, Seq.seq, pure]
      · obtain ⟨lf, lg⟩ := encode_lt_pair cf cg
        rw [hg (Nat.pair_lt_pair_right _ lf), hg (Nat.pair_lt_pair_right _ lg)]
        cases evaln k cf n
        · rfl
        cases evaln k cg n <;> rfl
      · obtain ⟨lf, lg⟩ := encode_lt_comp cf cg
        rw [hg (Nat.pair_lt_pair_right _ lg)]
        cases evaln k cg n
        · rfl
        simp [k, hg (Nat.pair_lt_pair_right _ lf)]
      · obtain ⟨lf, lg⟩ := encode_lt_prec cf cg
        rw [hg (Nat.pair_lt_pair_right _ lf)]
        cases n.unpair.2
        · rfl
        simp only
        rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]
        cases evaln k' _ _
        · rfl
        simp [k, hg (Nat.pair_lt_pair_right _ lg)]
      · have lf := encode_lt_rfind' cf
        rw [hg (Nat.pair_lt_pair_right _ lf)]
        rcases evaln k cf n with - | x
        · rfl
        simp only [Option.bind_some]
        cases x <;> simp
        rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: n : ℕ
⊢ decodeNat (encodeNat n) = n

Tactic:
conv_rhs => rw [← Num.to_of_nat n]

Goal state after:
n : ℕ
⊢ decodeNat (encodeNat n) = ↑↑n
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    nth_rw 3 [← show Fin.ofNat 4 1 = (1 : ℕ) from Fin.val_ofNat ..]
    rw [List.range_succ, List.foldl_append, ih, ← Fin.ofNat_add, List.foldl_cons, List.foldl_nil]
    match h : Fin.ofNat 4 n with
    | 0 =>
      rw [Fin.zero_add, ← xor_one_of_even <| even_iff.mpr ?_, xor_xor_cancel_left]
      rw [← @mod_mod_of_dvd _ 4 _ <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 1 =>
      rw [Nat.xor_comm]
      refine xor_one_of_even <| even_iff.mpr ?_
      rw [add_mod, ← @mod_mod_of_dvd _ 4 n <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 2 =>
      apply Nat.xor_self
    | 3 =>
      apply zero_xor

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ M.IsPath s t [] ↔ s = t

Tactic:
rw [isPath_iff]

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ (t = s ∧ [] = [] ∨ ∃ t_1 a x, t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔ s = t
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b c : Num
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
by transfer_rw; apply le_trans

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

Goal state before:
pp: Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
⊢ { l // BlankExtends l₁ l ∧ BlankExtends l₂ l }

Tactic:
by
  refine
    if hl : l₁.length ≤ l₂.length then ⟨l₂, Or.elim h id fun h' ↦ ?_, BlankExtends.refl _⟩
    else ⟨l₁, BlankExtends.refl _, Or.elim h (fun h' ↦ ?_) id⟩
  · exact (BlankExtends.refl _).above_of_le h' hl
  · exact (BlankExtends.refl _).above_of_le h' (le_of_not_ge hl)

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b ↦ true) (Part.assert (p a) fun x ↦ Part.some ()) ∨
        x ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) a) fun x ↦ Part.some ())
n : α
⊢ (fun a ↦ decide (p a)) n ∈ Part.map (fun b ↦ true) (Part.assert (p n) fun x ↦ Part.some ()) ∨
    (fun a ↦ decide (p a)) n ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) n) fun x ↦ Part.some ())

Tactic:
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
        true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]

Goal state after:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b ↦ true) (Part.assert (p a) fun x ↦ Part.some ()) ∨
        x ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) a) fun x ↦ Part.some ())
n : α
⊢ p n ∨ ¬p n
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : ((some val✝, v'), s) ∈ tr M (some q, v) a
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
simp only [tr, Option.mem_def] at h₁

Goal state after:
case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₁ l₂ : List Bool
e : (enc a).toList = l₁.reverseAux l₂
⊢ (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
induction l₁ generalizing l₂ with

Goal state after:
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 → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
this :
  ∀ (q : Stmt Γ Λ σ) (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)))
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.normal l₁)) v (trTape enc0 (Tape.mk' L R)))
    (trCfg enc enc0 (stepAux (M l₁) v (Tape.mk' L R)))

Tactic:
trTape_mk'

Goal state after:
Γ : 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 Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
this :
  ∀ (q : Stmt Γ Λ σ) (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)))
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a) (stepAux (tr enc dec M (Λ'.normal l₁)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (M l₁) v (Tape.mk' L R)))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : List.Vector ℕ m), cg.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> f v
v : List.Vector ℕ m
⊢ (cf.comp cg).eval ↑v = pure <$> ((Vector.mOfFn fun i ↦ g i v) >>= f)

Tactic:
by
        simp [hg, hf, map_bind]
        rfl

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
e : (a : α) → X a ⟶ B
⊢ Continuous fun x ↦
    match x with
    | ⟨a, x⟩ => (ConcreteCategory.hom (e a)) x

Tactic:
by
      apply continuous_sigma
      intro a; exact (e a).hom.hom.continuous

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ Z✝ : CompHausLike P
f : Z✝ ⟶ X✝ ⨿ Y✝
⊢ HasExplicitPullback coprod.inl f

Tactic:
apply hP'

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ Z✝ : CompHausLike P
f : Z✝ ⟶ X✝ ⨿ Y✝
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom coprod.inl)
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)
⊢ TM1.init (trInit k L) =
    { l := Option.map normal (some default), var := default,
      Tape := Tape.mk' ∅ (addBottom (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse))) }

Tactic:
trInit,

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)
⊢ TM1.init
      ((true, (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).headI.2) ::
        (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).tail) =
    { l := Option.map normal (some default), var := default,
      Tape := Tape.mk' ∅ (addBottom (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse))) }
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_5
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
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
intro _ _ -- halt
      simp only [trStmts₁, Finset.notMem_empty]
      exact ⟨trivial, fun _ ↦ False.elim⟩

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : ↑D → B := Prod.snd ∘ Subtype.val
X₂_cont : Continuous X₂
this : f ∘ E.domRestrict X₂ = φ ∘ ⇑ρ'
⊢ φ ∘ ⇑ρ' ∘ ⇑ρ'.symm = φ

Tactic:
Homeomorph.self_comp_symm,

Goal state after:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : ↑D → B := Prod.snd ∘ Subtype.val
X₂_cont : Continuous X₂
this : f ∘ E.domRestrict X₂ = φ ∘ ⇑ρ'
⊢ φ ∘ id = φ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
by_cases! Un : U = ∅
    · simp_all
    · exact ((preirreducibleSpace_iff_open_dense X).mp h hU Un).closure_eq ▸ isOpen_univ

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case empty
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
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ ∅, P e ∈ S) → ⋂ e ∈ ∅, P e ∈ S

Tactic:
intro P he _hh

Goal state after:
case empty
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
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
P : J → Set ↑(F.obj j)
he : Set.univ ∈ S
_hh : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
⊢ (∀ e ∈ ∅, P e ∈ S) → ⋂ e ∈ ∅, P e ∈ S
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: 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)
x : ↑C.pt.toTop
T : Set ↑(toTopCat.mapCone C).pt
hT : T ∈ S
hx : x ∈ T
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app (j ⟨T, hT⟩))) ⁻¹' V ⟨T, hT⟩

Tactic:
← (hV ⟨T, hT⟩).2

Goal state after:
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)
x : ↑C.pt.toTop
T : Set ↑(toTopCat.mapCone C).pt
hT : T ∈ S
hx : x ∈ T
⊢ x ∈ ↑⟨T, hT⟩
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₂
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝ : Cont'
H₁ : contSupp a✝.cons₂ ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret a✝.cons₂))

Tactic:
rw [contSupp_cons₂, Finset.union_subset_iff] at H₁

Goal state after:
case cons₂
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝ : Cont'
H₁ : trStmts₁ (head stack (Λ'.ret a✝)) ⊆ S ∧ contSupp a✝ ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret a✝.cons₂))
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_1
⊢ Function.Injective ⇑natUnionInftyEmbedding

pp: case refine_2
⊢ IsClosedMap ⇑natUnionInftyEmbedding

Tactic:
· rintro (_ | n) (_ | m) h
    · rfl
    · simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, zero_eq_inv] at h
      assumption_mod_cast
    · simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_eq_zero] at h
      assumption_mod_cast
    · simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj,
        Nat.cast_inj] at h
      rw [h]

Goal state after:
case refine_2
⊢ IsClosedMap ⇑natUnionInftyEmbedding
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
X✝ Y✝ : Profiniteᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (lanPresheaf F).map x✝ ≫
      (match Y✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom =
    (match X✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom ≫
      F.map x✝

Tactic:
by simpa using colimit.hom_ext fun _ ↦ (by simp)

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p =
    ((LightCondensed.freeForgetAdjunction R).homEquiv T.toCondensed X).symm
        ((coherentTopology LightProfinite).yonedaEquiv.symm x) ≫
      f

Tactic:
Functor.comp_map,

Goal state after:
R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (LightCondensed.free R).map (lightProfiniteToLightCondSet.map π) ≫ p =
    ((LightCondensed.freeForgetAdjunction R).homEquiv T.toCondensed X).symm
        ((coherentTopology LightProfinite).yonedaEquiv.symm x) ≫
      f
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
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 ⊗ (free R).obj S'.toCondensed ⟶ A
hh : (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (μIso (free R) P S.toCondensed).hom ≫ g = g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e

Tactic:
refine ⟨S', π, hπ, (μIso (free R) _ _).inv ≫ g', ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
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 ⊗ (free R).obj S'.toCondensed ⟶ A
hh : (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (μIso (free R) P S.toCondensed).hom ≫ g = g' ≫ e
⊢ (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g = ((μIso (free R) P S'.toCondensed).inv ≫ g') ≫ e
Module: Mathlib.Condensed.Light.InternallyProjective

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

Tactic:
refine ⟨S', π, hπ, (μIso (free R) _ _).inv ≫ g', ?_⟩

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