mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : α
x : Bool
hx : x ∈ Part.map (fun b ↦ true) (Part.assert (p a) fun x ↦ Part.some ())
y : Bool
hy : y ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) a) fun x ↦ Part.some ())
⊢ x = y

Tactic:
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
            and_true, exists_const] at hx hy

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
a : α
x y : Bool
hx : p a ∧ true = x
hy : ¬p a ∧ false = y
⊢ x = y
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.one
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)
⊢ ↑(p (PosNum.bit true m) 1) = ↑(bit (g true true) (bif g true false then pos m else 0))

Tactic:
pb1

Goal state after:
case pos.pos.bit1.one
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)
⊢ ↑(bit (g true true) (bif g true false then pos m else 0)) = ↑(bit (g true true) (bif g true false then pos m else 0))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.one
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)
⊢ ↑(p (PosNum.bit false m) 1) = ↑(bit (g false true) (bif g true false then pos m else 0))

Tactic:
pb1

Goal state after:
case pos.pos.bit0.one
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)
⊢ ↑(bit (g false true) (bif g true false then pos m else 0)) =
    ↑(bit (g false true) (bif g true false then pos m else 0))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case neg
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : ¬v₁.headI = 0
hv₂ : v₂ ∈ f.fix.eval v₁.tail
⊢ Sum.inl v₂ ∈ Part.some (Sum.inr v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inr v₁.tail) ∧
        v₂ ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'

Tactic:
exact Or.inr ⟨_, Part.mem_some _, hv₂⟩

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE

Tactic:
by
  tfae_have 2 → 1
  | _ => by
    simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]
  tfae_have 1 → 2
  | _ => inferInstance
  tfae_have 3 → 2
  | e => by
    rw [epi_iff_surjective]
    intro b
    obtain ⟨t, x, h⟩ := e b
    refine ⟨Sigma.ι X t x, ?_⟩
    change (Sigma.ι X t ≫ Sigma.desc π) x = _
    simpa using h
  tfae_have 2 → 3
  | e => by
    rw [epi_iff_surjective] at e
    let i : ∐ X ≅ finiteCoproduct X :=
      (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _)
    intro b
    obtain ⟨t, rfl⟩ := e b
    let q := i.hom t
    refine ⟨q.1,q.2,?_⟩
    have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id]; rfl
    rw [this]
    change _ = (i.inv ≫ Sigma.desc π) (i.hom t)
    suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by
      rw [this]; rfl
    rw [Iso.inv_comp_eq]
    apply colimit.hom_ext
    rintro ⟨a⟩
    simp only [i, Discrete.functor_obj, colimit.ι_desc, Cofan.mk_ι_app,
      colimit.comp_coconePointUniqueUpToIso_hom_assoc]
    ext; rfl
  tfae_finish

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

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg.halt <$> k.eval (v.headI :: v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

Tactic:
bind_pure_comp

Goal state after:
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg.halt <$> k.eval (v.headI :: v') = Cfg.halt <$> k.eval (v.headI :: v')
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
bind_pure_comp

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg.halt <$> k.eval v' = Cfg.halt <$> k.eval v'
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
rw [IH, bind_pure_comp]

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

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → ∀ (b : ↑Y.toTop), ∃ a, (ConcreteCategory.hom f) a = b

Tactic:
contrapose!

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
⊢ (∃ b, ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ b) → ¬Epi f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) rev []) k₂
      ((update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) rev).reverseAux
        (update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₂))

Tactic:
simp only [Function.update_comm h₁.1, Function.update_idem]

Goal state after:
case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))
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)
⊢ ⋃₀ S ⊆ ⋃ i, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i

Tactic:
rintro x ⟨T, hT, hx⟩

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 ∈ ⋃ i, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
⊢ Epi f → ∀ (b : ↑Y.toTop), ∃ a, (ConcreteCategory.hom f) a = b

Tactic:
contrapose!

Goal state after:
case mp
X Y : LightProfinite
f : X ⟶ Y
⊢ (∃ b, ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ b) → ¬Epi f
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)
⊢ IsIso (sigmaComparison X σ)

Tactic:
sigmaComparison_eq_comp_isos

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)
⊢ IsIso
    ((X.mapIso
          (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
            (productIsProduct fun x ↦ Opposite.op (of P (σ x))))).hom ≫
      (PreservesProduct.iso X fun a ↦ Opposite.op (of P (σ a))).hom ≫
        (Types.productIso fun a ↦ X.obj (Opposite.op (of P (σ a)))).hom)
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg

Tactic:
have :
    LocallyConstant.comap (C.π.app j0).hom.hom ggg =
      LocallyConstant.unflip (LocallyConstant.comap (C.π.app j0).hom.hom ggg).flip := by
    simp

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
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
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
⊢ f x = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg)) x

Tactic:
simp only [LocallyConstant.coe_comap, LocallyConstant.map_apply,
    Function.comp_apply]

Goal state after:
J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
⊢ f x = σ (gg ((TopCat.Hom.hom (C.π.app j).hom) x))
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 Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
⊢ ((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1})) ⋙
            functor P hs).map
        g ≫
      ObjectProperty.homMk (counitApp Y.obj) =
    ObjectProperty.homMk (counitApp X.obj) ≫ (𝟭 (Sheaf (coherentTopology (CompHausLike P)) (Type (max u w)))).map g

Tactic:
have := CompHausLike.preregular hs
    apply InducedCategory.hom_ext
    simp only [functor, Functor.comp_obj, Functor.flip_obj_obj, ObjectProperty.ι_obj,
      ObjectProperty.lift_obj_obj, Functor.id_obj, Functor.comp_map, Functor.flip_obj_map,
      ObjectProperty.ι_map, ObjectProperty.lift_map, ObjectProperty.FullSubcategory.comp_hom,
      ObjectProperty.homMk_hom, Functor.id_map]
    ext S (f : LocallyConstant _ _)
    simp only [NatTrans.comp_app, counitApp_app, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply]
    apply presheaf_ext (f.map (g.hom.app (op (CompHausLike.of P PUnit.{u + 1}))))
    intro a
    simp only [functorToPresheaves_obj_obj, functorToPresheaves_map_app, TypeCat.hom_ofHom,
      TypeCat.Fun.coe_mk, dsimp% incl_of_counitAppApp]
    apply presheaf_ext (f.comap (sigmaIncl _ _).hom.hom)
    intro b
    simp only [counitAppAppImage, ← Functor.map_comp_apply, ← op_comp,
      map_apply, IsTerminal.comp_from, ← map_preimage_eq_image_map]
    change (_ ≫ Y.obj.map _) _ = (_ ≫ Y.obj.map _) _
    simp only [← g.hom.naturality]
    rw [show sigmaIncl (f.comap (sigmaIncl (f.map _) a).hom.hom) b ≫ sigmaIncl (f.map _) a =
        CompHausLike.ofHom P (X := fiber _ b) (sigmaInclIncl f _ a b) ≫ sigmaIncl f (Fiber.mk f _)
      by ext; rfl]
    simp only [op_comp, Functor.map_comp, types_comp_apply, dsimp% incl_of_counitAppApp]
    simp only [counitAppAppImage, ← Functor.map_comp_apply, ← op_comp]
    rw [mk_image]
    change (X.obj.map _ ≫ _) _ = (X.obj.map _ ≫ _) _
    simp only [g.hom.naturality]
    simp only [types_comp_apply]
    have := map_preimage_eq_image (f := g.hom.app _ ∘ f) (a := a)
    simp only [Function.comp_apply] at this
    rw [this]
    apply congrArg
    symm
    convert! (b.preimage).prop
    exact (mem_iff_eq_image (g.hom.app _ ∘ f) _ _).symm

Goal state after:
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
y : ↑S.toTop
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g.down)) a = y

Tactic:
obtain ⟨x, hx⟩ := hf (g.down.hom y)

Goal state after:
X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
y : ↑S.toTop
x : ↑X✝.toTop
hx : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g.down.hom) y
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g.down)) a = y
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (isoLocallyConstantOfIsColimit X hX).inv = counitApp X

Tactic:
by
  dsimp [isoLocallyConstantOfIsColimit]
  simp only [Category.assoc]
  rw [Iso.inv_comp_eq]
  ext S : 2
  apply colimit.hom_ext
  intro ⟨Y, _, g⟩
  suffices _ ≫ (isoFinYonedaComponents _ _).inv ≫ X.map g =
    (locallyConstantPresheaf _).map g ≫ counitAppApp (Opposite.unop S) X by
      simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]
  erw [(counitApp.{u, u + 1} X).naturality]
  simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]
  congr
  ext f
  simp only [toProfinite_obj, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
    ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, counitApp_app]
  apply presheaf_ext.{u, u + 1} (X := X) (Y := X) (f := f)
  intro x
  dsimp [toProfinite_obj]
  rw [incl_of_counitAppApp.{u, u + 1}]
  simp only [counitAppAppImage]
  have : Finite (fiber.{u, u + 1} f x) :=
    Finite.of_injective (sigmaIncl.{u, u + 1} f x).1 Subtype.val_injective
  apply injective_of_mono (isoFinYonedaComponents X (fiber.{u, u + 1} f x)).hom
  ext y
  simp only [toProfinite_obj, isoFinYonedaComponents_hom, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk, ← Functor.map_comp_apply, ← op_comp]
  rw [show (Profinite.of PUnit.{u + 1}).const y ≫
    IsTerminal.from _ (fiber.{u, u + 1} f x) = 𝟙 _ from rfl]
  simp only [op_comp, Functor.map_comp_apply, op_id, Functor.map_id_apply]
  simpa [← dsimp% isoFinYonedaComponents_inv_comp X _ (sigmaIncl.{u, u + 1} f x),
    ← isoFinYonedaComponents_hom_apply, -isoFinYonedaComponents_hom] using! x.map_eq_image f y

Goal state after:
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: case inl
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h'✝ : j < (↑x).succ
h' : j < ↑x
⊢ ¬p j

Tactic:
exact x.2 _ h'

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompl t F G)

Tactic:
by
  constructor <;> intros <;>
    simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]
  · simp [traverse_eq_map_id', bitraverse_eq_bimap_id]
  · dsimp only [bicompl]
    simp [binaturality, naturality_pf]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
⊢ (α.drop ::: α.last) i = α i

Tactic:
by cases i <;> rfl

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a s.toAList = dlookup a s

Tactic:
List.toAList,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a { entries := s.dedupKeys, nodupKeys := ⋯ } = dlookup a s