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

Goal state before:
pp: case read
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
b : Λ'
⊢ Decidable (read f✝ = b)

Tactic:
cases b

Goal state after:
case read.move
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (read f✝ = move p✝ k₁✝ k₂✝ q✝)

case read.clear
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (read f✝ = clear p✝ k✝ q✝)

case read.copy
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ Decidable (read f✝ = q✝.copy)

case read.push
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (read f✝ = push k✝ s✝ q✝)

case read.read
f✝¹ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝¹ a = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (read f✝¹ = read f✝)

case read.succ
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ Decidable (read f✝ = q✝.succ)

case read.pred
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (read f✝ = q₁✝.pred q₂✝)

case read.ret
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : Cont'
⊢ Decidable (read f✝ = ret k✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
b : Λ'
⊢ Decidable (q✝.succ = b)

Tactic:
cases b

Goal state after:
case succ.move
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = move p✝ k₁✝ k₂✝ q✝)

case succ.clear
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = clear p✝ k✝ q✝)

case succ.copy
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (q✝¹.succ = q✝.copy)

case succ.push
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = push k✝ s✝ q✝)

case succ.read
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q✝.succ = read f✝)

case succ.succ
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (q✝¹.succ = q✝.succ)

case succ.pred
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (q✝.succ = q₁✝.pred q₂✝)

case succ.ret
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (q✝.succ = ret k✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
b : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = b)

Tactic:
cases b

Goal state after:
case pred.move
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = move p✝ k₁✝ k₂✝ q✝)

case pred.clear
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = clear p✝ k✝ q✝)

case pred.copy
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = q✝.copy)

case pred.push
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = push k✝ s✝ q✝)

case pred.read
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q₁✝.pred q₂✝ = read f✝)

case pred.succ
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = q✝.succ)

case pred.pred
q₁✝¹ q₂✝¹ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝¹ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝¹ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (q₁✝¹.pred q₂✝¹ = q₁✝.pred q₂✝)

case pred.ret
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
k✝ : Cont'
⊢ Decidable (q₁✝.pred q₂✝ = ret k✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case ret
k✝ : Cont'
b : Λ'
⊢ Decidable (ret k✝ = b)

Tactic:
cases b

Goal state after:
case ret.move
k✝ : Cont'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (ret k✝ = move p✝ k₁✝ k₂✝ q✝)

case ret.clear
k✝¹ : Cont'
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (ret k✝¹ = clear p✝ k✝ q✝)

case ret.copy
k✝ : Cont'
q✝ : Λ'
⊢ Decidable (ret k✝ = q✝.copy)

case ret.push
k✝¹ : Cont'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (ret k✝¹ = push k✝ s✝ q✝)

case ret.read
k✝ : Cont'
f✝ : Option Γ' → Λ'
⊢ Decidable (ret k✝ = read f✝)

case ret.succ
k✝ : Cont'
q✝ : Λ'
⊢ Decidable (ret k✝ = q✝.succ)

case ret.pred
k✝ : Cont'
q₁✝ q₂✝ : Λ'
⊢ Decidable (ret k✝ = q₁✝.pred q₂✝)

case ret.ret
k✝¹ k✝ : Cont'
⊢ Decidable (ret k✝¹ = ret k✝)
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
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
by
  refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => hu.2) fun x U memU hU => ?_
  obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU
  let u : Set s := ((↑) : s → H) ⁻¹' interior s
  have u_open_in_s : IsOpen u := isOpen_interior.preimage continuous_subtype_val
  lift x to s using interior_subset xs
  have : CompactSpace s := isCompact_iff_compactSpace.1 comp
  obtain ⟨V : Set s, VisClopen, Vx, V_sub⟩ := compact_exists_isClopen_in_isOpen u_open_in_s xs
  have VisClopen' : IsClopen (((↑) : s → H) '' V) := by
    refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1,
      ?_⟩
    let v : Set u := ((↑) : u → s) ⁻¹' V
    have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl
    have f0 : IsEmbedding ((↑) : u → H) := IsEmbedding.subtypeVal.comp IsEmbedding.subtypeVal
    have f1 : IsOpenEmbedding ((↑) : u → H) := by
      refine ⟨f0, ?_⟩
      · have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset
        rw [this]
        apply isOpen_interior
    have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val
    have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
      rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]
    rw [f3]
    apply f1.isOpenMap v f2
  use (↑) '' V, VisClopen', by simp [Vx], Subset.trans (by simp) sU

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

Goal state before:
pp: case cons₁
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    Cfg.halt <$>
      (fun v ↦ do
          let ns ← fs.eval as
          k.eval (v.headI :: ns))
        v

Tactic:
simp only [← bind_pure_comp, bind_assoc]

Goal state after:
case cons₁
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval as
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₂
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> (Cont.cons₂ ns k).eval v

Tactic:
rw [Cont.eval, stepRet]

Goal state after:
case cons₂
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun v ↦ k.eval (ns.headI :: v)) v
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun v ↦ f.eval v >>= k.eval) v

Tactic:
simp only [← bind_pure_comp, bind_assoc]

Goal state after:
case comp
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    do
    let x ← f.eval v
    let a ← k.eval x
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.fix f k) v) = Cfg.halt <$> (Cont.fix f k).eval v

Tactic:
rw [Cont.eval, stepRet]

Goal state after:
case fix
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) =
    Cfg.halt <$> (fun v ↦ if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval) v
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
⊢ ∀ {f : A → C} {g : B → C}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
φ

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
⊢ ∀ {g : B → C}, Continuous φ → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = φ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

Tactic:
← ij,

Goal state after:
case pos
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk i ⁻¹' Sigma.mk i '' U)
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : CompHaus
⊢ ∀ (f : toCompHaus.obj X ⟶ C) (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = f

Tactic:
φ

Goal state after:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
⊢ ∀ (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : Profinite
⊢ ∀ (f : toProfinite.obj X ⟶ C) (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = f

Tactic:
φ

Goal state after:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
⊢ ∀ (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X B C : Stonean
⊢ ∀ (f : X ⟶ C) (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = f

Tactic:
φ

Goal state after:
X B C : Stonean
φ : X ⟶ C
⊢ ∀ (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = φ
Module: Mathlib.Topology.Category.Profinite.AsLimit

Goal state before:
pp: case refine_2
X : Profinite
a : (fun X ↦ ↑X.toTop) (limitCone X.diagram).pt
⊢ ∃ a_1, (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) a_1 = a

Tactic:
· obtain ⟨b, hb⟩ :=
          DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h)
        use b
        -- ext S : 3 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` does not work, replaced with following
        -- three lines.
        apply Subtype.ext
        apply funext
        rintro S
        -- Porting note: end replacement block
        apply hb

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

Goal state before:
pp: case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
· rw [← CategoryTheory.ofHom_epi_iff_surjective]
    apply (forget LightProfinite).epi_of_epi_map

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

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

Tactic:
rw [contSupp_fix] at H₁

Goal state after:
case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret k))

Tactic:
by
  have W := fun {q} => trStmts₁_self q
  cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)

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

Goal state before:
pp: case read
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ'), x ∈ trStmts₁ (q x_1) → x ∈ S
⊢ Supports (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) S

Tactic:
exact supports_biUnion.2 fun _ => q_ih _ (H₁ _) fun _ h => h₂ _ h

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

Goal state before:
pp: case read
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ'), x ∈ trStmts₁ (q x_1) → x ∈ S
⊢ Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))) S

Tactic:
refine supports_insert.2 ⟨fun _ => h₂ _ W, ?_⟩ -- read
    exact supports_biUnion.2 fun _ => q_ih _ (H₁ _) fun _ h => h₂ _ h

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

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom
        ((Y.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (counitAppApp S Y)) f) =
    counitAppAppImage f a

Tactic:
Functor.mapIso_hom,

Goal state after:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (Y.map (sigmaIso f).op.hom ≫ (sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (counitAppApp S Y)) f) =
    counitAppAppImage f a
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full
⊢ (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).essImage
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
change (discrete _).essImage _

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full
⊢ (discrete (Type (u + 1))).essImage
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((functorIsoDiscreteAux₂ R X✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝)) ≫
      (functor R).map f =
    (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
assoc,

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functorIsoDiscreteAux₂ R X✝).hom ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
⊢ ∀ (X : Type (max u w)),
    (functor P hs).map ((unit P hs).app X) ≫ (counit P hs).app ((functor P hs).obj X) = 𝟙 ((functor P hs).obj X)

Tactic:
intro X
    ext : 1
    exact adjunction_left_triangle P hs X

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

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ (constantSheaf (coherentTopology LightProfinite) (Type u)).essImage
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
change (discrete _).essImage _

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ (discrete (Type u)).essImage
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))
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
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
have : Epi ((LightCondensed.forget _).map f) := inferInstance

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 : Epi ((LightCondensed.forget R).map f)
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ 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
⊢ (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g = ((μIso (free R) P S'.toCondensed).inv ≫ g') ≫ e

Tactic:
assoc,

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_2
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 ⊗ (free R).obj S.toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S'.toCondensed) ⟶ A
hh : (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g = g' ≫ e
⊢ (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = ((μIso (free R) P S'.toCondensed).hom ≫ g') ≫ e

Tactic:
assoc,

Goal state after:
case refine_2
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 ⊗ (free R).obj S.toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S'.toCondensed) ⟶ A
hh : (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g = g' ≫ e
⊢ (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = (μIso (free R) P S'.toCondensed).hom ≫ 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
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g = ((μIso (free R) S'.toCondensed P).inv ≫ g') ≫ e

Tactic:
assoc,

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