mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
⊢ (sSetTopAdj.homEquiv Δ[0] X) f = SSet.const (TopCat.toSSetObj₀Equiv.symm ((ConcreteCategory.hom f) default))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphI.symm 0 = stdSimplex.vertex 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphI.symm 1 = stdSimplex.vertex 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
x y : toSSet.obj X _⦋0⦌
e : SSet.Edge x y
⊢ (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) x = (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
x : ZerothHomotopy ↑X
⊢ SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯ (ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
x : (toSSet.obj X).π₀
⊢ ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ (SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯ x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
R : C
⊢ (singularChainComplexFunctorAdjunction C n).unit.app R =
    Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom ((stdSimplexToTop.app ⦋n⦌).app (Opposite.op ⦋n⦌))) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (Unique (ZerothHomotopy ↑X))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1))) default)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ (toSSet.obj X).IsConnected

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplex.δ 1 ≫ toSSetObjI = SSet.const (TopCat.toSSetObj₀Equiv.symm 0)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0))) default)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplex.δ 0 ≫ toSSetObjI = SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X) = F.map i.down

Tactic:
· congr 1
    rw [← reassoc_of% sSetTopAdj_unit_app_app_down]
    exact congr(($(sSetTopAdj.right_triangle_components X).app (.op ⦋n⦌) i).down)

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ Sigma.ι (fun x ↦ ((evaluation TopCat C).obj (SimplexCategory.toTop.{w} ^⦋n⦌)).obj F) i ≫
      ((singularChainComplexFunctorAdjunction C n).counit.app F).app X =
    F.map i.down

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ (ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 0 (op ⦋0⦌)) = TopCat.toSSetObj₀Equiv.symm 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ToSSet

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ SSet.ι₀ ≫ TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    (SSet.RelativeMorphism.botEquiv.symm (TopCat.toSSet.map f)).map

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ToSSet

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ SSet.ι₁ ≫ TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    (SSet.RelativeMorphism.botEquiv.symm (TopCat.toSSet.map g)).map

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ (ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 1 (op ⦋0⦌)) = TopCat.toSSetObj₀Equiv.symm 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ToSSet

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ ⊥.ι ▷ SSet.stdSimplex.obj { len := 1 } ≫
      TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    SemiCartesianMonoidalCategory.fst ⊥.toSSet (SSet.stdSimplex.obj { len := 1 }) ≫
      SSet.Subcomplex.isInitialBot.to ⊥.toSSet ≫ ⊥.ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₀

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
X : TopCat
R : C
⊢ ((X.singularHomology₀Iso R).hom ≫ Sigma.desc fun x ↦ 𝟙 R) = X.singularHomology₀ε R

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₁

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : Field R
T : Type u_3
inst✝² : Field T
v : AbsoluteValue R S
inst✝¹ : Algebra R T
inst✝ : Algebra.IsSeparable R T
⊢ (algebraMap (WithAbs v) T).comp ↑(equiv v).symm = (↑(RingEquiv.refl T)).comp (algebraMap R T)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
inst✝ : Field R
v : AbsoluteValue R ℝ
a : R
ha : v a < 1
⊢ Filter.Tendsto (fun e ↦ ‖1⁻¹ + toAbs v a ^ e - 1‖) Filter.atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
inst✝ : Field R
v : AbsoluteValue R ℝ
a : R
ha : v a < 1
⊢ Filter.Tendsto (fun n ↦ (equiv v).symm (1 / (1 + a ^ n))) Filter.atTop (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : CommRing R
T : Type u_3
inst✝¹ : Field T
inst✝ : Algebra R T
w : AbsoluteValue T ℝ
r : R
⊢ UniformContinuous fun x ↦ r • x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : s.Nonempty
x : ↑s
⊢ { toFun := fun p ↦ ⟨↑p.1 • x✝ + (1 - ↑p.1) • ↑p.2, ⋯⟩, continuous_toFun := ?m.76 }.toFun (0, x) =
    (ContinuousMap.id ↑s) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : s.Nonempty
x : ↑s
⊢ { toFun := fun p ↦ ⟨↑p.1 • x✝ + (1 - ↑p.1) • ↑p.2, ⋯⟩, continuous_toFun := ?m.76 }.toFun (1, x) =
    (ContinuousMap.const ↑s ⟨x✝, ⋯⟩) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : s.Nonempty
⊢ ContractibleSpace ↑s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: n : ℕ
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ 1 ≤ 1 + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: n : ℕ
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ (Y.spine 1 f₂._proof_6 (f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x))).vertex 1 =
    (Y.spine 1 f₂._proof_6 (f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x))).vertex 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := (f i).toFinset
x : α
hx : x ∈ s
⊢ x ∈ u

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := (f i).toFinset
⊢ s.card ≤ u.card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
⊢ ↑u.card ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst✝¹ : Semiring T
inst✝ : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f✝ : R →+* T
g✝ : T →+* U
f : R ≃+* T
g : T ≃+* U
x : WithAbs v
⊢ (map w v f.symm.toRingHom) ((↑↑(map v w f.toRingHom)).toFun x) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ ((hY.spineEquiv 2 f₂._proof_5) (f₂ f₀ f₁ hδ₁ hδ₀ hY x)).arrow 0 =
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst✝¹ : Semiring T
inst✝ : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f✝ : R →+* T
g✝ : T →+* U
f : R ≃+* T
g : T ≃+* U
x : WithAbs w
⊢ (↑↑(map v w f.toRingHom)).toFun ((map w v f.symm.toRingHom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : Semiring R
v w : AbsoluteValue R S
x : WithAbs w
⊢ (equiv v) ((congr v w (RingEquiv.refl R)).symm x) = (equiv w) x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
⊢ t ⊆ ⋃ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : Semiring R
v w : AbsoluteValue R S
x : R
⊢ (congr v w (RingEquiv.refl R)) ((equiv v).symm x) = (equiv w).symm x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : Semiring R
v w : AbsoluteValue R S
x : R
⊢ (congr v w (RingEquiv.refl R)).symm ((equiv w).symm x) = (equiv v).symm x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ i, f i
⊢ (sum fun x ↦ a) = #ι * a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
R : Type u_3
T : Type u_4
inst✝² : Semiring R
v : AbsoluteValue R S
inst✝¹ : SMul T R
inst✝ : FaithfulSMul T R
m₁✝ m₂✝ : T
h : ∀ (a : WithAbs v), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ ((hY.spineEquiv 2 f₂._proof_5) (f₂ f₀ f₁ hδ₁ hδ₀ hY x)).arrow 1 =
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
R : Type u_3
T : Type u_4
inst✝⁴ : Semiring R
v : AbsoluteValue R S
P : Type u_5
inst✝³ : SMul T P
inst✝² : SMul R T
inst✝¹ : SMul R P
inst✝ : IsScalarTower R T P
⊢ ∀ (x : WithAbs v) (y : T) (z : P), (x • y) • z = x • y • z

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ i, f i
⊢ #ι * a ≤ ℵ₀ * a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
R : Type u_3
T : Type u_4
inst✝⁴ : Semiring R
v : AbsoluteValue R S
P : Type u_5
inst✝³ : SMul P R
inst✝² : SMul P T
inst✝¹ : SMul R T
inst✝ : IsScalarTower P R T
⊢ ∀ (x : P) (y : WithAbs v) (z : T), (x • y) • z = x • y • z

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun x ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
this : #↑(ULift.down ⁻¹' t) ≤ lift.{v, u} a
⊢ #↑t ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
    (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) (f₂ f₀ f₁ hδ₁ hδ₀ hY x)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case ht
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun x ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l
x : ULift.{v, u} α
hx : x ∈ ULift.down ⁻¹' t
⊢ ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i

Tactic:
simpa only [Function.comp_apply, mem_preimage, eventually_map] using! ht _ hx

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #α ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
    (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) (f₂ f₀ f₁ hδ₁ hδ₀ hY x)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α = a

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
this : ∃ f, range f ⊆ Set.univ ∧ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Injective f
⊢ 𝔠 ≤ #𝕜

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ x + c ^ n ∈ U ∩ Set.univ

Tactic:
by

Goal state after: