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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
a✝¹ : Γ → σ → σ
a✝ : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.load a✝¹ a✝), v), Tape := T } =
    TM0.step (tr M) { q := (some a✝, a✝¹ T.head v), Tape := T }

Tactic:
by rfl

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := l₁, var := v, Tape := T })
    (TM1.step M { l := l₁, var := v, Tape := T })

Tactic:
by
    rcases l₁ with - | l₁; · exact rfl
    simp only [trCfg, TM1.step, FRespects, Option.map]
    induction M l₁ generalizing v T with
    | move _ _ IH => exact TransGen.head rfl (IH _ _)
    | write _ _ IH => exact TransGen.head rfl (IH _ _)
    | load _ _ IH => exact (reaches₁_eq (by rfl)).2 (IH _ _)
    | branch p _ _ IH₁ IH₂ =>
      unfold TM1.stepAux; cases e : p T.1 v
      · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₂ _ _)
      · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₁ _ _)
    | _ =>
      exact TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T)))

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
L : ListBlank ((k : K) → Option (Γ k))
⊢ default.2 = default

Tactic:
by rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R S : RegularExpression α
⊢ map id (R + S) = R + S

Tactic:
by simp_rw [map, map_id]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R S : RegularExpression α
⊢ map id (R * S) = R * S

Tactic:
by simp_rw [map, map_id]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R : RegularExpression α
⊢ map id R.star = R.star

Tactic:
by simp_rw [map, map_id]

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

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

Tactic:
intro q hs hw

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
q : Stmt Γ Λ σ
hs : SupportsStmt S q
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
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 : σ → Option (Γ k) → σ
e : S k = []
⊢ (bif (addBottom L).head.1 then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
    else
      TM1.stepAux q (f v (∅.head.2 k))
        (Tape.write (∅.head.1, update ∅.head.2 k none) (Tape.mk' ∅.tail (ListBlank.cons ∅.head (addBottom L))))) =
    TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))

Tactic:
rw [addBottom_head_fst, cond]

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

Goal state before:
pp: case rfind.mpr
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
n : ℕ
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
w : List ℕ
this :
  w ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
⊢ w ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)

Tactic:
induction n with
      | zero => exact this
      | succ n IH =>
        refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
        simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false,
          Part.mem_some_iff, List.tail_cons]

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

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (Sigma.ι X a))

Tactic:
by
  refine IsOpenEmbedding.of_comp _ (homeoOfIso ((colimit.isColimit _).coconePointUniqueUpToIso
    (finiteCoproduct.isColimit X))).isOpenEmbedding ?_
  convert! finiteCoproduct.isOpenEmbedding_ι X a
  ext x
  change (Sigma.ι X a ≫ _) x = _
  simp

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

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
⊢ cospan f.hom g.hom ≅
    cospan ((cospan f g ⋙ compHausLikeToTop P).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ compHausLikeToTop P).map WalkingCospan.Hom.inr)

Tactic:
by rfl

Goal state after:
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
π : Z ⟶ Y
hπ : EffectiveEpi π
y : ↑X.toTop
⊢ ∃ a, (ConcreteCategory.hom (pullback.fst f π)) a = y

Tactic:
obtain ⟨z, hz⟩ := hs π hπ (f y)

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
hπ : EffectiveEpi π
y : ↑X.toTop
z : ↑Z.toTop
hz : (ConcreteCategory.hom π) z = (ConcreteCategory.hom f) y
⊢ ∃ a, (ConcreteCategory.hom (pullback.fst f π)) a = y
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ U ∈ 𝓝 x ↔ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
constructor
    · have hx : connectedComponent x = {x} :=
        totallyDisconnectedSpace_iff_connectedComponent_singleton.mp ‹_› x
      rw [connectedComponent_eq_iInter_isClopen] at hx
      intro hU
      let N := { s // IsClopen s ∧ x ∈ s }
      rsuffices ⟨⟨s, hs, hs'⟩, hs''⟩ : ∃ s : N, s.val ⊆ U
      · exact ⟨s, ⟨hs', hs⟩, hs''⟩
      have : Nonempty N := ⟨⟨univ, isClopen_univ, mem_univ x⟩⟩
      have hNcl : ∀ s : N, IsClosed s.val := fun s => s.property.1.1
      have hdir : Directed GE.ge fun s : N => s.val := by
        rintro ⟨s, hs, hxs⟩ ⟨t, ht, hxt⟩
        exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left, inter_subset_right⟩
      have h_nhds : ∀ y ∈ ⋂ s : N, s.val, U ∈ 𝓝 y := fun y y_in => by
        rw [hx, mem_singleton_iff] at y_in
        rwa [y_in]
      exact exists_subset_nhds_of_compactSpace hdir hNcl h_nhds
    · rintro ⟨V, ⟨hxV, -, V_op⟩, hUV : V ⊆ U⟩
      rw [mem_nhds_iff]
      exact ⟨V, hUV, V_op, hxV⟩

Goal state after:
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 ℕ
⊢ eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> (Cont.comp f k).eval v

Tactic:
rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]

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

Goal state before:
pp: X Y : Profinite
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 : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ ↑((ConcreteCategory.hom h) ((ConcreteCategory.hom f) x)).down =
    ↑({ toFun := ULift.up ∘ fun x ↦ if x ∈ V then 0 else 1, continuous_toFun := ⋯ } ((ConcreteCategory.hom f) x)).down

Tactic:
rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, ConcreteCategory.hom_ofHom,
          ContinuousMap.coe_mk, Function.comp_apply, if_neg]

Goal state after:
case hnc
X Y : Profinite
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 : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ (ConcreteCategory.hom f).toFun x ∉ V
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

pp: case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
· rintro ⟨⟩

Goal state after:
case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
⊢ ∀ {A B : LightProfinite} (f : A ⟶ B) [IsIso ((forget LightProfinite).map f)], IsIso f

Tactic:
intro A B f hf

Goal state after:
X Y : LightProfinite
f✝ : X ⟶ Y
A B : LightProfinite
f : A ⟶ B
hf : IsIso ((forget LightProfinite).map f)
⊢ IsIso f
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: S : LightDiagram
n : ℕ
⊢ Finite (↑((S.diagram ⋙ toProfinite).obj (op n)).toTop → Fin 2)

Tactic:
refine @Pi.finite _ _ ?_ _

Goal state after:
S : LightDiagram
n : ℕ
⊢ Finite ↑((S.diagram ⋙ toProfinite).obj (op n)).toTop
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case neg
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
⊢ ∃ b₂,
    TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

Tactic:
· obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)
      refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this.1]
      convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
      · simp
        convert! rfl
      · exact fun x h => trNat_natEnd _ _ (List.tail_subset _ h)
      · exact ⟨rfl, this.2⟩

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

Goal state before:
pp: case succ.right
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))

Tactic:
intro h x h'
      simp only [Finset.mem_insert]
      exact Or.inr (Or.inr <| q_ih h h')

Goal state after:
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
⊢ image (f ∘ g) a = image f (mk f (g (preimage (f ∘ g) a)))

Tactic:
← map_preimage_eq_image_map _ _ a,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
⊢ f (g (preimage (f ∘ g) a)) = image f (mk f (g (preimage (f ∘ g) a)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₁
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x ↦ false) aux stack (trNormal a✝¹ a✝.cons₂)))) ∪
      codeSupp a✝¹ a✝.cons₂ ⊆
    S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.cons₁ a✝¹ a✝)))

Tactic:
Finset.union_subset_iff

Goal state after:
case cons₁
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x ↦ false) aux stack (trNormal a✝¹ a✝.cons₂)))) ⊆
      S ∧
    codeSupp a✝¹ a✝.cons₂ ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.cons₁ a✝¹ a✝)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
Finset.union_subset_iff

Goal state after:
case cons₂
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝ : Cont'
H₁ : trStmts₁ (head stack (Λ'.ret a✝)) ⊆ S ∧ contSupp a✝ ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret a✝.cons₂))
Module: Mathlib.Topology.Category.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
⊢ a = b

Tactic:
have hhh := congr_fun hh a

Goal state after:
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 : ι a a = ι b a
⊢ a = b
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Prod

Tactic:
constructor <;> intros <;> casesm _ × _ <;>
    simp [bitraverse, Prod.bitraverse, functor_norm]

Goal state after:
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ Functor.Comp.mk ((fun a ↦ (fun x2 ↦ Prod.mk <$> f✝ a <*> x2) ∘ f'✝) <$> g✝ fst✝ <*> g'✝ snd✝) =
    Functor.Comp.mk ((fun a ↦ Prod.bitraverse f✝ f'✝ ∘ Prod.mk a) <$> g✝ fst✝ <*> g'✝ snd✝)

case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ pure (f✝ fst✝, f'✝ snd✝) = pure (bimap f✝ f'✝ (fst✝, snd✝))
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.4
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
⊢ (fun s ↦ Finset.map (k.trans h).toEmbedding s) =
    (fun s ↦ Finset.map h.toEmbedding s) ∘ fun s ↦ Finset.map k.toEmbedding s

Tactic:
by ext; simp [-trans_toEmbedding]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : γ → α → α
a : α
l : t β
⊢ foldr f a (g <$> l) = foldr (f ∘ g) a l

Tactic:
by
  simp only [foldr, foldMap_map, Function.comp_def]

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

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i ↦ Subtype.val) <$$> f P n α <$$> u✝ = x

Tactic:
MvFunctor.map_map

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ ((fun i ↦ Subtype.val) ⊚ f P n α) <$$> u✝ = x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) n✝ ≤ approx (⇑f) (n✝ + 1)

Tactic:
apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 ↦ x)

Tactic:
by
  ext i : 1; cases i <;> rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
exists i

Goal state after:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u_1} n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec.{u_1} (n✝ + 1)
a : α a✝.fs
b : β a✝.fs
⊢ prod.fst a✝.fs (prod.mk a✝.fs a b) = a

Tactic:
apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u_1} n✝} (a : α a✝) (b : β a✝), prod.snd a✝ (prod.mk a✝ a b) = b
α β : TypeVec.{u_1} (n✝ + 1)
a : α a✝.fs
b : β a✝.fs
⊢ prod.snd a✝.fs (prod.mk a✝.fs a b) = b

Tactic:
apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec.{u_1} n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.fst ⊚ (f ⊗' g)) a✝ = (f ⊚ prod.fst) a✝
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) a✝.fs = (f ⊚ prod.fst) a✝.fs

Tactic:
apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec.{u_1} n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) a✝.fs = (g ⊚ prod.snd) a✝.fs

Tactic:
apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝}, (prod.fst ⊚ prod.diag) a✝ = id a✝
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.fst ⊚ prod.diag) a✝.fs = id a✝.fs

Tactic:
apply i_ih

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)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i x ≤ approx (⇑f) i.succ x

Tactic:
apply approx_mono' f

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝}, (prod.snd ⊚ prod.diag) a✝ = id a✝
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.snd ⊚ prod.diag) a✝.fs = id a✝.fs

Tactic:
apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n✝¹ n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u} n✝} (a : (α ⊗ β) a✝), (id ⊗' id) a✝ a = id a✝ a
α✝ β✝ : TypeVec.{u} (n✝ + 1)
a : (α✝ ⊗ β✝) a✝.fs
⊢ (id ⊗' id) a✝.fs a = id a✝.fs a

Tactic:
apply i_ih

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ j,
    (approxChain { toFun := g, monotone' := ⋯ }) i ≤
      ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) j

Tactic:
exists i

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ (approxChain { toFun := g, monotone' := ⋯ }) i ≤
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁))

Tactic:
by
  ext i a
  cases i
  · cases a
    rfl
  · rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
⊢ fix _f = _f (fix _f)

Tactic:
by
    dsimp [fix]
    conv_lhs => erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]
    rfl

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : t' α✝
⊢ traverse (pure ∘ x✝¹) x✝ = pure (x✝¹ <$> x✝)

Tactic:
rw [h₂, Equiv.traverse_eq_map_id, h₀]

Goal state after: