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

Goal state before:
pp: case pos.pos
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)
m n : PosNum
⊢ ↑(f (pos m) (pos n)) = Nat.bitwise g ↑(pos m) ↑(pos n)

Tactic:
fnn

Goal state after:
case pos.pos
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)
m n : PosNum
⊢ ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k' a).Dom

Tactic:
bind_dom

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ∃ (h : (k (encode a)).Dom), (↑(decode ((k (encode a)).get h))).Dom
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l l₁ → BlankExtends l l₂ → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Tactic:
by
  rintro ⟨i, rfl⟩ ⟨j, rfl⟩ h; use j - i
  simp only [List.length_append, Nat.add_le_add_iff_left, List.length_replicate] at h
  simp only [← List.replicate_add, Nat.add_sub_cancel' h, List.append_assoc]

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

Goal state before:
pp: Γ : Type ?u.6
inst✝ : Inhabited Γ
α : Sort ?u.10
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
⊢ ∀ (a b : List Γ), (BlankRel.setoid Γ) a b → f a = f b

Tactic:
rintro a b (h | h)

Goal state after:
case inl
Γ : Type ?u.6
inst✝ : Inhabited Γ
α : Sort ?u.10
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
a b : List Γ
h : BlankExtends a b
⊢ f a = f b

case inr
Γ : Type ?u.6
inst✝ : Inhabited Γ
α : Sort ?u.10
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
a b : List Γ
h : BlankExtends b a
⊢ f a = f b
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a b ∧ f b = none

pp: case refine_1.some
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none

Tactic:
· rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]
      exact ⟨ReflTransGen.refl, e⟩

Goal state after:
case refine_1.some
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
⊢ l.getI n = (l ++ List.replicate i default).getI n

Tactic:
rw [List.getI_eq_default _ h]

Goal state after:
case inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
⊢ default = (l ++ List.replicate i default).getI n
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif p v then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

Tactic:
cases p v

Goal state after:
case branch.false
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif false then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

case branch.true
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif true then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S
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' ∅ (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) (S k).length (addBottom L))))) =
    TM1.stepAux q v ((Tape.move Dir.right)^[(S k).length + 1] (Tape.mk' ∅ (addBottom ?m.135)))

Tactic:
addBottom_modifyNth fun a ↦ update a k (some (f v))

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 + 1] (Tape.mk' ∅ (addBottom ?m.135)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q → q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
refine ⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' hq ↦ ?_⟩

Goal state after:
case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q → q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
q' : Λ' Γ Λ σ
hq : (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X Y Z : CompHausLike P
f : X ⟶ Y
⊢ ∀ (g : Z ⟶ Y) [EffectiveEpi g], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
π

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
⊢ ∀ [EffectiveEpi π], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ π = h ≫ f
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
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : Γ' K Γ
v✝ : σ
⊢ go k✝ s q✝ ∈ trSupp M S

Tactic:
exact hgo

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

Goal state before:
pp: case refine_1.inr
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
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)

Tactic:
exact IH₂ _ h

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
                prop := ⋯ }).map
          f ≫
        InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app Y).hom =
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app X).hom ≫ F.map f

Tactic:
intro j k f

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj
            { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
              prop := ⋯ }).map
        f ≫
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app k).hom =
    InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some ((if o = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main) (unrev q)), var := o,
      stk := elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }

Tactic:
if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp [o])

Goal state after:
case refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main (unrev q)), var := o,
      stk := elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case intro.intro
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : CompactSpace Y
inst✝² : CompactSpace X
inst✝¹ : Finite (Clopens X)
inst✝ : Finite (Clopens Y)
val✝¹ : Fintype (Clopens X)
val✝ : Fintype (Clopens Y)
⊢ Finite (Clopens (X × Y))

Tactic:
exact .of_surjective _ surjective_finset_sup_prod

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                is_hausdorff := ⋯, prop := ⋯ }).map
          f ≫
        ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app Y).hom) =
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app X).hom) ≫
        F.map f

Tactic:
intro j k f

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj
            { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
              prop := ⋯ }).map
        f ≫
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app k).hom) =
    ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j).hom) ≫ F.map f
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
⊢ ∀ (π : Z ⟶ B) [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))

Tactic:
π

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
⊢ ∀ [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X✝ : Type w'
inst✝² : TopologicalSpace X✝
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
Z B : CompHausLike P
⊢ ∀ (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom ((CompHausLike.compHausLikeToTop P).map π))

Tactic:
π

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X✝ : Type w'
inst✝² : TopologicalSpace X✝
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
Z B : CompHausLike P
π : Z ⟶ B
⊢ ∀ [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom ((CompHausLike.compHausLikeToTop P).map π))
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ (functor c).Initial

Tactic:
by
  let e : I ≌ ULiftHom.{w} (ULift.{w} I) := ULiftHomULiftCategory.equiv _
  suffices (e.inverse ⋙ functor c).Initial from initial_of_equivalence_comp e.inverse (functor c)
  rw [initial_iff_of_isCofiltered (F := e.inverse ⋙ functor c)]
  constructor
  · intro ⟨_, X, (f : c.pt ⟶ _)⟩
    obtain ⟨i, g, h⟩ := exists_hom c hc f
    exact ⟨⟨i⟩, ⟨StructuredArrow.homMk g h.symm⟩⟩
  · intro ⟨_, X, (f : c.pt ⟶ _)⟩ ⟨i⟩ ⟨_, (s : F.obj i ⟶ X), (w : f = c.π.app i ≫ _)⟩
      ⟨_, (s' : F.obj i ⟶ X), (w' : f = c.π.app i ≫ _)⟩
    simp only [StructuredArrow.hom_eq_iff,
      StructuredArrow.comp_right]
    refine ⟨⟨i⟩, 𝟙 _, ?_⟩
    simp only [CategoryTheory.Functor.map_id]
    rw [w] at w'
    exact toProfinite.map_injective <| Epi.left_cancellation _ _ w'

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

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
h : ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))
S : Profinite
this : PreservesFilteredColimitsOfSize.{u, u, u + 1, u + 1, u + 2, u + 2} (forget (ModuleCat R)) :=
  preservesFilteredColimitsOfSize_shrink (forget (ModuleCat R))
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).obj).mapCocone S.asLimitCone.op))

Tactic:
exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
h : ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
this : PreservesFilteredColimitsOfSize.{0, 0, u, u, u + 1, u + 1} (forget (ModuleCat R)) :=
  preservesFilteredColimitsOfSize_shrink (forget (ModuleCat R))
⊢ Nonempty (IsColimit (((LightCondensed.forget R).obj M).obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ((ConcreteCategory.hom (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)))) []).reverse = toList xs

Tactic:
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
            simp only [toList, foldl, Foldl.get, foldl.ofFreeMonoid_comp_of,
              Function.comp_apply]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ (ConcreteCategory.hom (foldMap (Foldr.mk ∘ f) xs)) x =
    (TypeCat.Hom.hom (foldMap (⇑(Foldr.ofFreeMonoid f) ∘ FreeMonoid.of) xs)) x

Tactic:
foldr.ofFreeMonoid_comp_of

Goal state after:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ (ConcreteCategory.hom (foldMap (Foldr.mk ∘ f) xs)) x = (TypeCat.Hom.hom (foldMap (Foldr.mk ∘ f) xs)) x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
⊢ (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → (fs : v ⟹ v') → β v v' fs

Tactic:
intro v v'

Goal state after:
n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec.{?u.30} (n + 1)
v' : TypeVec.{?u.32} (n + 1)
⊢ (fs : v ⟹ v') → β v v' fs