mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

pp: case inr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
· suffices ∃ j, IsEmpty (F.obj j) by
      refine this.imp fun j hj => ?_
      refine ⟨⟨hj.elim, fun A => ?_⟩, ?_⟩
      · convert! isOpen_empty
        ext x
        exact hj.elim x
      · ext x
        exact hj.elim' (C.π.app j x)
    by_contra! h
    have : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := h
    have : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : T2Space (F.obj j))
    have : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : CompactSpace (F.obj j))
    have cond := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u}
      (F ⋙ Profinite.toTopCat)
    suffices Nonempty C.pt from IsEmpty.false (S.proj this.some)
    let D := Profinite.toTopCat.mapCone C
    have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
    have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv
    exact cond.map CD

Goal state after:
case inr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
⊢ ∀ (s : Option Γ'),
    Λ'.Supports S
      ((if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main) (unrev (Λ'.ret k).succ))

Tactic:
| succ =>

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

Goal state before:
pp: case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
⊢ Λ'.Supports S (trNormal f (Cont'.cons₁ fs k))

Tactic:
apply IHf

Goal state after:
case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
apply IHf

Goal state after:
case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝ : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
⊢ ∀ {c_1 : ULiftHom (ULift.{w, u} I)}
    (s s' : (e.inverse ⋙ functor c).obj c_1 ⟶ { left := left✝, right := X, hom := f }),
    ∃ c' t, (e.inverse ⋙ functor c).map t ≫ s = (e.inverse ⋙ functor c).map t ≫ s'

Tactic:
⟨i⟩

Goal state after:
case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝ : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
⊢ ∀ (s s' : (e.inverse ⋙ functor c).obj { down := i } ⟶ { left := left✝, right := X, hom := f }),
    ∃ c' t, (e.inverse ⋙ functor c).map t ≫ s = (e.inverse ⋙ functor c).map t ≫ s'
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : CondensedSet
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))].TFAE

Tactic:
tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
  tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
  tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ CompHaus.isTerminalPUnit adjunction _
  tfae_have 1 ↔ 5 :=
    have : functor.Faithful := inferInstance
    have : functor.Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ CompHaus.isTerminalPUnit adjunction _
  tfae_have 1 ↔ 6 :=
    (Sheaf.isConstant_iff_of_equivalence (coherentTopology Profinite)
      (coherentTopology CompHaus) profiniteToCompHaus Profinite.isTerminalPUnit
      CompHaus.isTerminalPUnit _).symm
  tfae_have 7 → 4 := fun h ↦
    mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)
  tfae_have 4 → 7 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv (isoWhiskerLeft profiniteToCompHaus.op
      ((sheafToPresheaf _ _).mapIso i))
      (Condensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
  tfae_finish

Goal state after:
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ (∀ (X_1 : CompHaus) (y : ToType (Y.obj.obj (op X_1))),
      ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (hom (f.hom.app (op X'))) x = (hom (Y.obj.map (op φ))) y) ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y

Tactic:
[

Goal state after:
A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ (∀ (X_1 : CompHaus) (y : ToType (Y.obj.obj (op X_1))),
      ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (hom (f.hom.app (op X'))) x = (hom (Y.obj.map (op φ))) y) ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (toProfinite.op ⋙ F).map x✝ ≫ (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
by
    simp only [comp_obj, op_obj, finYoneda_obj, Functor.comp_map, op_map]
    ext
    simp only [isoFinYonedaComponents_hom, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
      ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, toProfinite_obj,
      ← Functor.map_comp_apply]
    rfl

Goal state after:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y) ↔
    ∀ (S : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
[

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y) ↔
    ∀ (S : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi (lim.map f)

Tactic:
this

Goal state after:
n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom)
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
have Z_closed (i) : IsClosed (Z i) :=
    (IsClosedEmbedding.isClosed_iff_image_isClosed (Continuous.isClosedEmbedding hf f_inj)).mp
    (IsClosed.preimage hg isClosed_singleton)

Goal state after:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
⊢ (ihomPoints R P B S').symm ((ihomPoints R P A S') ((ihomPoints R P A S').symm g') ≫ e) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) g

Tactic:
have := ihomPoints_symm_comp R B P S' S π ((ihomPoints R P B S) g)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
this :
  (ihomPoints R P B S').symm (P ◁ (free R).map (lightProfiniteToLightCondSet.map π) ≫ (ihomPoints R P B S) g) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map π.op)) ((ihomPoints R P B S).symm ((ihomPoints R P B S) g))
⊢ (ihomPoints R P B S').symm ((ihomPoints R P A S') ((ihomPoints R P A S').symm g') ≫ e) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) g
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x✝ : t α
⊢ traverse ((fun {α} ↦ η.app α) ∘ f) x✝ = (fun {α} ↦ η.app α) (traverse f x✝)

Tactic:
naturality

Goal state after:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x✝ : t α
⊢ traverse ((fun {α} ↦ η.app α) ∘ f) x✝ = traverse ((fun {α} ↦ η.app α) ∘ f) x✝
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 Const

Tactic:
constructor <;> intros <;> simp [bitraverse, Const.bitraverse, functor_norm] <;> rfl

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

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y
⊢ WellFounded (Upto.GT p)

Tactic:
this

Goal state after:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y
⊢ WellFounded (InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y)
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : α → β → β
x✝¹ x✝ : FreeMonoid α
⊢ ↾flip (List.foldr f) (FreeMonoid.toList (x✝¹ * x✝)) =
    ↾flip (List.foldr f) (FreeMonoid.toList x✝¹) * ↾flip (List.foldr f) (FreeMonoid.toList x✝)

Tactic:
by
    apply ConcreteCategory.ext
    ext
    apply List.foldr_append

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
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
this : (fun i ↦ Subtype.val) = fun i x ↦ ↑(f P n α i x)
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x

Tactic:
this

Goal state after:
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) }
this : (fun i ↦ Subtype.val) = fun i x ↦ ↑(f P n α i x)
⊢ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x ↔ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x
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
P : β → Prop
x : F (α ::: β)
⊢ LiftP' (α.PredLast' P) x ↔ LiftP (α.PredLast P) x

Tactic:
by
  dsimp only [LiftP, LiftP']
  apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)
  · ext i ⟨x, _⟩
    cases i <;> rfl
  · intros
    rw [MvFunctor.map_map]
    dsimp +unfoldPartialApp [(· ⊚ ·)]
    suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this]
    ext i ⟨x, _⟩
    cases i <;> rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
this : g = nilFun
⊢ β g

Tactic:
this

Goal state after:
n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
this : g = nilFun
⊢ β nilFun
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
α β : Type u
f : α → β
x : t' α
⊢ Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)

Tactic:
by
  simp only [Equiv.traverse, traverse_eq_map_id]; rfl

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
hf : f i = 0
hg : g i = 0
⊢ Icc (f i) (g i) = 0

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
hf : f i = 0
hg : g i = 0
⊢ Icc (f i) (g i) = 0
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), x i ∈ (f.rangeIcc g) i) ↔ f ≤ x ∧ x ≤ g

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), x i ∈ (f.rangeIcc g) i) ↔ f ≤ x ∧ x ≤ g
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f ≤ toMultiset g ↔ f ≤ g

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f ≤ toMultiset g ↔ f ≤ g
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f < toMultiset g ↔ f < g

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f < toMultiset g ↔ f < g
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ ∑ a ∈ Finset.cons a s ha, ⨆ i, f a i = ⨆ i, ∑ a ∈ Finset.cons a s ha, f a i

Tactic:
[

Goal state after:
case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ ∑ a ∈ Finset.cons a s ha, ⨆ i, f a i = ⨆ i, ∑ a ∈ Finset.cons a s ha, f a i
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin

Tactic:
ss

Goal state after:
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin

Tactic:
ss

Goal state after:
C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left✝² : a ∈ _root_.Set.univ
left✝¹ : b ∈ _root_.Set.univ
left✝ : c ∈ _root_.Set.univ
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left✝² : a ∈ _root_.Set.univ
left✝¹ : b ∈ _root_.Set.univ
left✝ : c ∈ _root_.Set.univ
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ (lookup k s₂).isSome = true

Tactic:
this

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ (some ((lookup k s₁).get ⋯)).isSome = true
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type ?u.51
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
H' : f a₁ = f a₂
⊢ s₂.liftOn (f a₁) ⋯ = s₂.liftOn (f a₂) ⋯

Tactic:
simp only [H']

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ || f x✝² x✝¹ || f x✝ b₂) = (x✝³ || f x✝ b₂ || f x✝² x✝¹)

Tactic:
[

Goal state after:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ || f x✝² x✝¹ || f x✝ b₂) = (x✝³ || f x✝ b₂ || f x✝² x✝¹)