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

Goal state before:
pp: q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : [].reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }

Tactic:
simp only [List.reverseAux] at e

Goal state after:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : [].reverseAux (trPosNum a) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none, stk := elim (trPosNum a ++ Γ'.cons :: trList v) [] c d }

Tactic:
simp only [List.reverseAux] at e

Goal state after:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none, stk := elim (trPosNum a ++ Γ'.cons :: trList v) [] c d }
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (finsetClopens X)

Tactic:
apply Function.Injective.of_comp (f := Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ (↑))
  rw [comp_finsetClopens]
  intro ⟨_, _⟩ ⟨_, _⟩ h
  congr
  rw [Setoid.classes_inj]
  exact h

Goal state after:
Module: Mathlib.Condensed.AB

Goal state before:
pp: A : Type u_1
J : Type u_2
inst✝⁸ : Category.{v_1, u_1} A
inst✝⁷ : Category.{v_2, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
⊢ HasExactColimitsOfShape J (Condensed A)

Tactic:
let e : Condensed.{u} A ≌ Sheaf (extensiveTopology Stonean.{u}) A :=
    (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
  exact HasExactColimitsOfShape.domain_of_functor _ e.functor

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ inst✝³ = generateFrom {s | IsClopen s}

Tactic:
apply IsTopologicalBasis.eq_generateFrom

Goal state after:
case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ IsTopologicalBasis {s | IsClopen s}
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos (↑n).succ')).tail ++ Γ'.cons :: trList tail✝

Tactic:
cases (n : Num).succ' <;> exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case pred.refine_2.inl
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
x✝ : q' = unrev q₂
x : Λ'
h'✝ : x ∈ trStmts₁ (unrev q₂)
h' : x = Λ'.move (fun x ↦ false) rev main q₂
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
simp [h', unrev]

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

Goal state before:
pp: case pred.refine_2.inr
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
x✝ : q' = unrev q₂
x : Λ'
h'✝ : x ∈ trStmts₁ (unrev q₂)
h' : x ∈ trStmts₁ q₂
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
simp [h', unrev]

Goal state after:
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
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))

Tactic:
refine ⟨fun a b h ↦ ?_, fun ⟨a, ha⟩ ↦ ?_⟩

Goal state after:
case refine_1
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
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a =
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) b
⊢ a = b

case refine_2
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
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
x✝ :
  (fun X ↦ X)
    ↑{x |
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
a : (yonedaPresheaf G X).obj (op Z)
ha :
  a ∈
    {x |
      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
⊢ ∃ a_1,
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a_1 = ⟨a, ha⟩
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩
h :
  (sigmaIsoHom f) ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ =
    (sigmaIsoHom f) ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩
⊢ ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ = ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩

Tactic:
refine Sigma.subtype_ext ?_ h

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx : val✝¹ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩
w✝ : ↑(Set.range f)
val✝ : S
hy : val✝ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩
h :
  (sigmaIsoHom f) ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩ =
    (sigmaIsoHom f) ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩
⊢ ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx⟩⟩.fst = ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy⟩⟩.fst
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
y : ↑(Set.range ⇑l)
hy : (fun x ↦ ⇑l ⁻¹' {↑x}) y = ↑x
⊢ CompactSpace ↑↑x

Tactic:
rw [← isCompact_iff_compactSpace, ← hy]

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
y : ↑(Set.range ⇑l)
hy : (fun x ↦ ⇑l ⁻¹' {↑x}) y = ↑x
⊢ IsCompact ((fun x ↦ ⇑l ⁻¹' {↑x}) y)
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
⊢ CompactSpace ↑↑x

Tactic:
by
  obtain ⟨y, hy⟩ := x.prop
  rw [← isCompact_iff_compactSpace, ← hy]
  exact (l.2.isClosed_fiber _).isCompact

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

Goal state before:
pp: case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
⊢ Λ'.Supports S (trNormal f k) ∧ Λ'.Supports S (trNormal g k)

Tactic:
exact ⟨IHf Hk.2.1, IHg Hk.2.2⟩

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

Goal state before:
pp: case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (counitAppApp (Profinite.of (Opposite.unop Y).obj) X)) f)

Tactic:
dsimp [toProfinite_obj]

Goal state after:
case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (counitAppApp (Profinite.of (Opposite.unop Y).obj) X)) f)
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
⊢ ⇑(ConcreteCategory.hom g') ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom f') ∘ ⇑(ConcreteCategory.hom g)

Tactic:
simp [← CompHausLike.coe_comp, h_comm]

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

Goal state before:
pp: α : Type u_1
x : Option α
⊢ Option.traverse pure x = pure x

Tactic:
by
  cases x <;> rfl

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

Goal state before:
pp: σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by
  cases x <;> simp! [Sum.traverse, functor_norm]

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ i.rev.rev = i

Tactic:
induction i <;> simp_all [rev]

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

Goal state before:
pp: case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u

Tactic:
refine ⟨g <$$> u, ?_⟩
    rw [h₁]
    simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
⊢ y ∈ approx (⇑f) j a → y = b

Tactic:
intro h₁

Goal state after:
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
⊢ y = b
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) f) = f

Tactic:
cases f <;> simp [Except.map]

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) f) = f

Tactic:
cases f <;> simp [Except.map]

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)
c : Chain ((a : α) → (b : β a) → γ a b)
⊢ (monotoneUncurry α β γ) (ωSup c) = ωSup (c.map (monotoneUncurry α β γ))

Tactic:
by
  ext ⟨x, y⟩
  dsimp [uncurry, ωSup]
  rw [map_comp, map_comp]
  rfl

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
x : BitVec w
n : ℕ
⊢ (x ^ n).toFin = x.toFin ^ n

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp [ih, BitVec.pow_succ]

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
x✝ : Set α
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∪ G.F.f t,
            pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets

Tactic:
cases G

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
x✝ : Set α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : F✝¹.toFilter = f
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = g
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.f s ∪ { σ := σ✝, F := F✝, eq := eq✝ }.F.f t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') =>
                  ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.inf a b, { σ := σ✝, F := F✝, eq := eq✝ }.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∩ G.F.f t,
        pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g

Tactic:
cases G

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : F✝¹.toFilter = f
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = g
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.f s ∩ { σ := σ✝, F := F✝, eq := eq✝ }.F.f t,
        pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.inf a b, { σ := σ✝, F := F✝, eq := eq✝ }.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ f = ⊥

Tactic:
← F.eq,

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ F.F.toFilter = ⊥
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case swap.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₂ : f b with - | d

Goal state after:
case swap.none.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.none.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case swap.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₂ : f b with - | d

Goal state after:
case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.some.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
⊢ (s :: l).NodupKeys ↔ ¬s.fst ∈ l.keys ∧ l.NodupKeys

Tactic:
by simp [keys, NodupKeys]

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

Goal state before:
pp: α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih : tl.NodupKeys → (map (Sigma.map f fun x ↦ id) tl).NodupKeys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
h : (Sigma.map f (fun x ↦ id) hd).fst ∈ (map (Sigma.map f fun x ↦ id) tl).keys
⊢ hd.fst ∈ tl.keys

Tactic:
by
      simp only [keys, map_map] at h ⊢
      obtain ⟨x, hm, he⟩ := mem_map.mp h
      exact mem_map.mpr ⟨x, hm, hf he⟩

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
· subst h₂
      simp [h]

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case swap
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
s₁ s₂ : Sigma β
l✝ : List (Sigma β)
l : List (Sigma β)
⊢ (s₂ :: s₁ :: l✝).kunion l ~ (s₁ :: s₂ :: l✝).kunion l

Tactic:
| swap s₁ s₂ l =>

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

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑i) * fib (-↑(i + 1) + -1) + -fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs

Tactic:
← neg_add,

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑i) * fib (-(↑(i + 1) + 1)) + -fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l.reverse <+: l.reverse

Tactic:
exact takeWhile_prefix _

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

Goal state before:
pp: m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]

Tactic:
by
  simp [Ico, Nat.sub_sub_self (succ_le_of_lt h)]

Goal state after: