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

Goal state before:
pp: case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
refine TransGen.head' rfl ?_

Goal state after:
case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ ReflTransGen (fun a b ↦ b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.clear p k q)) s S)
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
s : Option Γ'
v : List ℕ
c d : List Γ'
⊢ ∃ s',
    Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList v) [] c d }
      (Nat.rec { l := some q₁, var := s', stk := elim (trList v.tail) [] c d }
        (fun n x ↦ { l := some q₂, var := s', stk := elim (trList (n :: v.tail)) [] c d }) v.headI)

Tactic:
rcases v with (_ | ⟨_ | n, v⟩)
  · refine ⟨none, TransGen.single ?_⟩
    simp
  · refine ⟨some Γ'.cons, TransGen.single ?_⟩
    simp
  refine ⟨none, ?_⟩
  simp only [trList, trNat.eq_1, trNum, Nat.cast_succ, Num.add_one, Num.succ,
    List.tail_cons, List.headI_cons]
  rcases (n : Num) with - | a
  · simp only [trPosNum, Num.succ', List.singleton_append, List.nil_append]
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', TM2.stepAux]
    convert! unrev_ok using 2
    simp
  simp only [Num.succ']
  suffices ∀ l₁, ∃ l₁' l₂' s',
    List.reverseAux l₁ (trPosNum a) = List.reverseAux l₁' l₂' ∧
      Reaches₁ (TM2.step tr)
        ⟨some (q₁.pred q₂), s, K'.elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d⟩
        ⟨some (unrev q₂), s', K'.elim (l₂' ++ Γ'.cons :: trList v) l₁' c d⟩ by
    obtain ⟨l₁', l₂', s', e, h⟩ := this []
    simp only [List.reverseAux] at e
    refine h.trans ?_
    convert! unrev_ok using 2
    simp [e, List.reverseAux_eq]
  induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit1::l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum, show PosNum.one.succ = PosNum.one.bit0 from rfl]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp
    rfl
  | bit0 m IH =>
    obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
      cases m <;> refine ⟨_, _, rfl, rfl⟩
    refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
    simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide,
      Option.getD, -natEnd]
    rfl

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

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ False

Tactic:
have H : h = g := by
        rw [← cancel_epi f]
        ext x
        dsimp [g, LocallyConstant.ofIsClopen]
        rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, hom_ofHom, ContinuousMap.coe_mk,
          Function.comp_apply, if_neg]
        refine mt (fun α => hVU α) ?_
        simp [U, C]

Goal state after:
case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : h = g
⊢ False
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ (↑a).Nonempty

Tactic:
refine ⟨preimage f a, ?_⟩
  rw [mem_iff_eq_image, ← map_preimage_eq_image]

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₂ : (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))) S

Tactic:
try simp [Finset.subset_iff] at h₂

Goal state after:
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
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S

Tactic:
try simp [Finset.subset_iff] at h₂

Goal state after:
case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

Tactic:
try simp [Finset.subset_iff] at h₂

Goal state after:
case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case inj
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
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
a b : α
hh : ι a = ι b
hhh : 0 = if b = a then 0 else 1
⊢ a = b

Tactic:
split_ifs at hhh with hh1

Goal state after:
case pos
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
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
a b : α
hh : ι a = ι b
hh1 : b = a
hhh : 0 = 0
⊢ a = b

case neg
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
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
a b : α
hh : ι a = ι b
hh1 : ¬b = a
hhh : 0 = 1
⊢ a = b
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
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 LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
rw [Category.assoc, ← Iso.eq_inv_comp,
      ← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality]

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝) =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_1
⊢ Function.Injective ⇑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:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toProfinite).map ki)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toProfinite).map kj)) x)

Tactic:
dsimp [- CompHausLike.coe_comp]

Goal state after:
case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ toProfinite.map (F.map ki))) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ toProfinite.map (F.map kj))) x)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map ki)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map kj)) x)

Tactic:
dsimp [- CompHausLike.coe_comp]

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ toLightProfinite.map (F.map ki))) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ toLightProfinite.map (F.map kj))) x)
Module: Mathlib.Condensed.Light.InternallyProjective

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

Tactic:
specialize h e S ((μIso (free R) _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (μIso (free R) _ _).inv ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp only [← assoc]
    -- Generated by `simp?`. Leaving it unsqueezed is too slow
    simp only [μIso_hom, μIso_inv, Functor.comp_map, δ_natural_right, assoc, δ_μ, comp_id]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }) i.fs
⊢ ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2)) = ((↑x).1 = (↑x).2)

Tactic:
erw [repeatEq_iff_eq]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ ((↑x).1 = (↑x).2) = ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2))

Tactic:
erw [repeatEq_iff_eq]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
hh : ∃ i, y ∈ approx (⇑f) i a
⊢ y ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
exact h₁

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ subtypeVal r ⊚ toSubtype' r = fun i x ↦ prod.mk i (↑x).1 (↑x).2

Tactic:
by
  ext i x
  induction i <;> simp only [toSubtype', comp, subtypeVal, prod.mk] at *
  simp [*]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ mk (out ⟨s, h⟩) = ⟨s, h⟩

Tactic:
simp only [mk]

Goal state after:
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ ⟨fun b ↦ out ⟨s, h⟩ = b, ⋯⟩ = ⟨s, h⟩
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Perm α) = (Nat.card α)!

Tactic:
classical
  have := Fintype.ofFinite α
  rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

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

Goal state before:
pp: α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
nd : l.NodupKeys
⊢ (map (Sigma.map id f) l).NodupKeys

Tactic:
simp_all [NodupKeys, map₂_keys]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (lookupAll a l).length ≤ 1

Tactic:
rwa [← nodup_replicate, ← map_const]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Tactic:
by_cases h' : a ∈ s₁

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih : hd.fst ∈ tl.keys → ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ (hd :: tl).keys
⊢ ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst (hd :: tl) = l₁ ++ l₂

Tactic:
exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (a ∈ u.sup fun f ↦ image f (t.sup fun f ↦ image f s)) ↔
    a ∈ ((image comp u).sup fun f ↦ image f t).sup fun f ↦ image f s

Tactic:
simp only [mem_sup, mem_image]

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ i ∈ u, ∃ a_1, (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = a) ↔
    ∃ i, (∃ i_1, (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = a
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2

Tactic:
by
  rw [sq, sq]
  exact natAbs_lt_iff_mul_self_lt

Goal state after:
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ (↑a - ↑b).natAbs < n

Tactic:
rw [← Nat.cast_lt (α := ℤ), natCast_natAbs]

Goal state after:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |↑a - ↑b| < ↑n
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ count (fun x ↦ x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

Tactic:
← ofNat_inj,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(count (fun x ↦ x ≡ v [MOD r]) b) = ↑(b / r + if v % r < b % r then 1 else 0)
Module: Mathlib.Data.List.ChainOfFn

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Tactic:
simp_rw [isChain_iff_getElem, List.getElem_ofFn, length_ofFn]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []

Tactic:
by
  rw [rtakeWhile_concat, if_neg h]

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

Goal state before:
pp: case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ [g.reverse ++ [a]].reverse ∨ m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
reverse_singleton,

Goal state after:
case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ [g.reverse ++ [a]] ∨ m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ p.Coprime (n + 1)

Tactic:
rw [Nat.Prime.coprime_iff_not_dvd Fact.out]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ ¬p ∣ n + 1
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.ceilRoot (a ^ n) = a

Tactic:
simp [ceilRoot_def, pos_iff_ne_zero.2, hn]

Goal state after:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a