mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ

Tactic:
rw [disjoint_iff_inter_eq_empty, ← compl_union, ← image_union, ← compl_inter,
      disjoint_iff_inter_eq_empty.mp disj, compl_empty, compl_empty_iff,
      image_univ_of_surjective ρ_surj]

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)

Tactic:
exact ((preirreducibleSpace_iff_open_dense X).mp h hU Un).closure_eq ▸ isOpen_univ

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

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
h : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
⊢ False

Tactic:
let h : Y ⟶ mkFinite (ULift (Fin 2)) := ConcreteCategory.ofHom ⟨fun _ => ⟨1⟩, continuous_const⟩

Goal state after:
X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ False
Module: Mathlib.Topology.Category.LightProfinite.Limits

Goal state before:
pp: X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom f)
y : ↑Y.toTop
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.snd f g)) a = y

Tactic:
obtain ⟨x, hx⟩ := h (g y)

Goal state after:
X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom f)
y : ↑Y.toTop
x : ↑X.toTop
hx : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.snd f g)) a = y
Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rw [← epi_iff_surjective]

Goal state after:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Epi f
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))
⊢ False

Tactic:
let g : Y ⟶ Z := CompHausLike.ofHom _
        ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩

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 := ⋯ }
⊢ False
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✝¹
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
⊢ ∀ ⦃X Y : (CompHausLike P)ᵒᵖ⦄ (f_1 : X ⟶ Y),
    ((TopCat.toSheafCompHausLike P X✝ hs).obj.map f_1 ≫ ↾fun g ↦ (TopCat.Hom.hom f).comp g) =
      (↾fun g ↦ (TopCat.Hom.hom f).comp g) ≫ (TopCat.toSheafCompHausLike P Y✝ hs).obj.map f_1

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
Z : Type u_6
inst✝¹ : MulOneClass Y
inst✝ : MulOneClass Z
f : Y →* Z
⊢ map (⇑f) 1 = 1

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
Z : Type u_6
inst✝¹ : MulOneClass Y
inst✝ : MulOneClass Z
f : Y →* Z
⊢ ∀ (x y : LocallyConstant X Y), map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (x y : LocallyConstant X Y), map (⇑f) (x + y) = map (⇑f) x + map (⇑f) y

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (m : R) (x : LocallyConstant X Y), map (⇑f) (m • x) = (RingHom.id R) m • map (⇑f) x

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring Y
inst✝² : Algebra R Y
inst✝¹ : Semiring Z
inst✝ : Algebra R Z
f : Y →ₐ[R] Z
x✝ : R
⊢ (↑↑(mapRingHom ↑f)).toFun ((algebraMap R (LocallyConstant X Y)) x✝) = (algebraMap R (LocallyConstant X Z)) x✝

Tactic:
aesop

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

Goal state before:
pp: F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)

Tactic:
aesop

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

Goal state before:
pp: F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
            (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv)

Tactic:
aesop

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

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
⊢ ∀ (t : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}) (j : ↑X.toTop),
    (fintypeCatAsCofan X).inj j ≫
        ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (t.inj x)) PUnit.unit, continuous_toFun := ⋯ } =
      t.inj j

Tactic:
aesop

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

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : 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:
by
  rw [← isLocallySurjective_iff_epi']
  exact LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite _ f

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : ↑(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:
by
  rw [← isLocallySurjective_iff_epi']
  exact LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite _ f

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

Goal state before:
pp: X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X
⊢ (ConcreteCategory.hom ((isColimitLocallyConstantPresheafDiagram X S).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) =
    (ConcreteCategory.hom (s.ι.app n)) f

Tactic:
change ((((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n) ≫
    (isColimitLocallyConstantPresheafDiagram X S).desc s) _ = _

Goal state after:
X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X
⊢ (ConcreteCategory.hom
        (((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n ≫
          (isColimitLocallyConstantPresheafDiagram X S).desc s))
      f =
    (ConcreteCategory.hom (s.ι.app n)) f
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
            (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j ≫
        colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.hom)

Tactic:
aesop

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

Goal state before:
pp: F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
            (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.inv)

Tactic:
aesop

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

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
⊢ ∀ (t : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}) (j : ↑X.toTop),
    (fintypeCatAsCofan X).inj j ≫
        ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (t.inj x)) PUnit.unit, continuous_toFun := ⋯ } =
      t.inj j

Tactic:
aesop

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

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

Tactic:
rw [internallyProjective_iff_tensor_condition]
  refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩
  · specialize h e S ((β_ _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (β_ _ _).inv ≫ g', ?_⟩
    simp [← hh]
  · specialize h e S ((β_ _ _).inv ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (β_ _ _).hom ≫ g', ?_⟩
    simp [← hh]

Goal state after:
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'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom
        (f ≫ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont }))
      a✝ =
    (ConcreteCategory.hom g) a✝

Tactic:
simp [← h₂]

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

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

Tactic:
specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map (μIso
        lightProfiniteToLightCondSet _ _).inv ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc]

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

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

Tactic:
specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map (μIso
        lightProfiniteToLightCondSet _ _).inv ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc]

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

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

Tactic:
rcases x with - | x <;> simp! [*, functor_norm, Option.traverse]

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

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x : F α
⊢ ∀ (u : F fun i ↦ Subtype ((fun i x ↦ ofRepeat (P i x)) i)),
    (fun i ↦ Subtype.val) <$$> u = x ↔ subtypeVal P <$$> toSubtype P <$$> u = x

Tactic:
by simp [MvFunctor.map_map]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ S' π = ⋂ n, ⋂ m, {x | (π ↑(x n)).1 = (π ↑(x m)).1}

Tactic:
aesop

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
⊢ f i ∈ t i

Tactic:
by_cases hi : i ∈ s

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∈ s
⊢ f i ∈ t i

case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ f i ∈ t i
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - (2 - 1) ≤ 2 * count b l

Tactic:
exact length_sub_one_le_two_mul_count_bool hl b

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) → ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) = a :: lookmap f l

Tactic:
simp only [lookmap, lookmap.go, Array.toListAppend_eq, nil_append]
  rw [lookmap.go_append, lookmap, h]; simp

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

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

Tactic:
simpa [h] using IH (pairwise_cons.1 H).2

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ b ∈ dlookup a l

Tactic:
by
  obtain ⟨b', h'⟩ := Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h))
  cases nd.eq_of_mk_mem h (of_mem_dlookup h')
  exact h'

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ ∀ (x y : ↑(S' ⊗ ℕ∪{∞}).toTop), h.elim x = h.elim y

Tactic:
aesop

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

Goal state before:
pp: case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)

Tactic:
have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using! Perm.swap a b l

Goal state after:
case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
this : (fun a b l ↦ ↑(a :: b :: l)) <$> f y <*> f x = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y
⊢ ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)
Module: Mathlib.Data.Finmap

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ a ∈ [].toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ []

Tactic:
simp only [toFinmap_nil, notMem_empty, not_mem_nil, exists_false]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
h₁ : s = t
h₂ : ∀ x ∈ t, f x = g x
⊢ pimage f s = pimage g t

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : f (b, m).1 = (b, m).2 ∧ (b, m).2 ≠ 0
n : M
hc : f (b, n).1 = (b, n).2 ∧ (b, n).2 ≠ 0
⊢ (b, m) = (b, n)

Tactic:
dsimp at hb hc

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : f b = m ∧ ¬m = 0
n : M
hc : f b = n ∧ ¬n = 0
⊢ (b, m) = (b, n)
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝ : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₁.support

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝ : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₂.support

Tactic:
aesop

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
⊢ (f + g).embSigma = f.embSigma + g.embSigma

Tactic:
ext ⟨k', i⟩

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩