mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst✝ : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (G.map f₁.op).app X₃ ≫ (G.obj (op X₁)).map f₃ = (G.obj (op Y₁)).map f₃ ≫ (G.map f₁.op).app Y₃

Tactic:
simp

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

Goal state before:
pp: p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ 0) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ 0) ⋯ = OrderHom.id
this : (orderHomOfSimplex (s₁, objMk₁ 0) ⋯) 0 = OrderHom.id 0
⊢ 0 ≤ Fin.castSucc 0

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
h : is.castSucc ∈ Ss
⊢ is.castSucc < is.succ

Tactic:
simp

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

Goal state before:
pp: p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ (Fin.last (p + 1)).succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯ = OrderHom.id
this : (orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯) (Fin.last (p + 1)) = OrderHom.id (Fin.last (p + 1))
⊢ (Fin.last (p + 1)).castSucc < Fin.last (p + 2)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : St = Finset.image it.succ.succAbove Sδ ∪ {it.succ}
⊢ Disjoint (Finset.image it.succ.succAbove Sδ) {it.succ}

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
X' : SimplicialObject C := ⋯
i : Fin (n + 1)
y : X _⦋n⦌
⊢ X.ιChainComplex y ≫ X'.σ i ≫ PInfty.f (n + 1) = 0

Tactic:
simp

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc.succ.castSucc < i.castSucc.succ.succ

Tactic:
simp

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc.castSucc.succ ≤ i.castSucc.succ.castSucc

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
x : (pairingCore k.succ n).ι
⊢ ¬x.index.castSucc = Fin.last (x.d + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
x✝ : X.op.PtSimplex n (opObjEquiv.symm x)
⊢ (fun g ↦ { map := yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)), comm := ⋯ })
      ((fun f ↦ { map := yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)), comm := ⋯ }) x✝) =
    x✝

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
x✝ : X.PtSimplex n x
⊢ (fun f ↦ { map := yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)), comm := ⋯ })
      ((fun g ↦ { map := yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)), comm := ⋯ }) x✝) =
    x✝

Tactic:
simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x✝ : X.N
⊢ SemiSimplexCategory.toSimplexCategory.map (SemiSimplexCategory.homOfMono (monoOfLE ⋯)) =
    SemiSimplexCategory.toSimplexCategory.map (𝟙 ⦋x✝.dim⦌ₛ)

Tactic:
simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
X✝ Y✝ Z✝ : X.N
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ SemiSimplexCategory.toSimplexCategory.map (SemiSimplexCategory.homOfMono (monoOfLE ⋯)) =
    SemiSimplexCategory.toSimplexCategory.map
      (SemiSimplexCategory.homOfMono (monoOfLE ⋯) ≫ SemiSimplexCategory.homOfMono (monoOfLE ⋯))

Tactic:
simp

Goal state after:
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
⊢ ∀ (a b : ↥(Finset.image (⇑f) s.finset)), a ≤ b ∨ b ≤ a

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : Y
ha : a ∈ Finset.image (⇑f) s.finset
b : Y
hb : b ∈ Finset.image (⇑f) s.finset
⊢ ⟨a, ha⟩ ≤ ⟨b, hb⟩ ∨ ⟨b, hb⟩ ≤ ⟨a, ha⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ f.map = f'.map

Tactic:
hf

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ f'.map = f'.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.castSucc
j : Fin (n + 2)
hj : i.succ.succ < j
⊢ i.castSucc.succ < i.succ.succ

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
j : Fin (n + 2)
hj : j < i.castSucc.castSucc
⊢ i.castSucc.castSucc < i.succ.castSucc

Tactic:
simp

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

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))), ↑X)
⊢ (fun f ↦ (Hom.hom f).comp ↑stdSimplexHomeomorphI) ((fun f ↦ ofHom (f.comp ↑stdSimplexHomeomorphI.symm)) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: X : TopCat
x✝ : I ⟶ X
⊢ (fun f ↦ ofHom (f.comp ↑stdSimplexHomeomorphI.symm)) ((fun f ↦ (Hom.hom f).comp ↑stdSimplexHomeomorphI) x✝) = x✝

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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 ↦ F.obj (TopCat.uliftFunctor.obj (TopCat.of ↑(_root_.stdSimplex ℝ (Fin (n + 1)))))) i ≫
      (Limits.Sigma.map fun x ↦ F.map (toTopSimplex.inv.app ⦋n⦌)) ≫
        𝟙 (∐ fun x ↦ F.obj (toTop.obj Δ[n])) ≫
          (𝟙 (∐ fun x ↦ F.obj (toTop.obj Δ[n])) ≫
              (Sigma.desc fun α ↦ F.map (toTop.map (SSet.yonedaEquiv.symm α))) ≫
                𝟙 (F.obj (toTop.obj (TopCat.toSSet.obj X)))) ≫
            ((Adjunction.whiskerLeft C sSetTopAdj).counit.app F).app X =
    F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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 ext; simp [algebraMap_left_apply]

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁵ : Field R
inst✝⁴ : Semifield S
inst✝³ : LinearOrder S
v w : AbsoluteValue R S
inst✝² : IsStrictOrderedRing S
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
⊢ v 0 < 1 ↔ w 0 < 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
j : ι
hj : j ≠ i
⊢ 0 ∈ Set.Iio 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Determinant

Goal state before:
pp: ⊢ 1 * -1 - 0 * 0 = -1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ 1 = ‖reCLM 1‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖1‖ ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ 1 = ‖imCLM I‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖I‖ ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcₙ : Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (b : ℕ), r₁ ≤ b → 1 < (v i) (c b)
j : ι
hj : j ≠ i
⊢ 0 ∈ Set.Iio 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ≥0∞
⊢ x ∈ closedEBall x r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
a : E
inst✝ : CompleteSpace E
hf : HasStrictFDerivAt f (↑f') a
⊢ HasStrictFDerivAt (↑(toOpenPartialHomeomorph f hf)) (↑f') (↑(toOpenPartialHomeomorph f hf).symm (f a))

Tactic:
simpa [← localInverse_def] using hf

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

Goal state before:
pp: case refine_1.zero.«1»
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
hn : 0 < 2
x✝ : X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom
          (X.map (δ 2 ((fun i ↦ i) ⟨1, ⋯⟩) ⋯ ⋯).op ≫ app f₀ f₁ hδ₁ hδ₀ hY (op { obj := ⦋0⦌, property := ⋯ }))).toFun
      x✝ =
    (ConcreteCategory.hom
          (app f₀ f₁ hδ₁ hδ₀ hY (op { obj := ⦋0 + 1⦌, property := ⋯ }) ≫ Y.map (δ 2 ((fun i ↦ i) ⟨1, ⋯⟩) ⋯ ⋯).op)).toFun
      x✝

Tactic:
apply hδ₁

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ 𝓝 0
⊢ (fun x ↦ (WithAbs.congr v w (RingEquiv.refl F)).symm ((WithAbs.congr v w (RingEquiv.refl F)) x)) ⁻¹' U ⊆ U

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
h : Filter.Tendsto (fun n ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto (fun n ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)

Tactic:
by simpa [Function.comp_def] using (hi.continuous.tendsto 0).comp h

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hz : ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • f z

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ (fun x ↦ 1) 0 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, id z = (z - 0) ^ 1 • (fun x ↦ 1) z

Tactic:
simp

Goal state after: