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

Goal state before:
pp: case inl
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.castSucc)
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map (SimplexCategory.δ it.castSucc).op))
      ((pairingCore k n).type₁
          { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).simplex =
    ((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).simplex
⊢ hs.δ = ht.δ

Tactic:
Subcomplex.N.ext_iff,

Goal state after:
case inl
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.castSucc)
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map (SimplexCategory.δ it.castSucc).op))
      ((pairingCore k n).type₁
          { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).simplex =
    ((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).simplex
⊢ hs.δ.toN = ht.δ.toN
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ 0)) ≫
      δ Y 0 =
    g.app (op ⦋n⦌)

Tactic:
ext x

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ 0)) ≫
            δ Y 0)).toFun
      x =
    (ConcreteCategory.hom (g.app (op ⦋n⦌))).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ (Fin.last n))) ≫
      δ Y (Fin.last (n + 1)) =
    f.app (op ⦋n⦌)

Tactic:
ext x

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ (Fin.last n))) ≫
            δ Y (Fin.last (n + 1)))).toFun
      x =
    (ConcreteCategory.hom (f.app (op ⦋n⦌))).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ)) ≫
      δ Y i.castSucc =
    δ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)

Tactic:
ext x

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ)) ≫
            δ Y i.castSucc)).toFun
      x =
    (ConcreteCategory.hom
          (δ X i ≫
            ↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j))).toFun
      x
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)
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ i.succ)) ≫
      δ Y i.castSucc.succ =
    (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ i.castSucc)) ≫
      δ Y i.castSucc.succ

Tactic:
ext x

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ i.succ)) ≫
            δ Y i.castSucc.succ)).toFun
      x =
    (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ i.castSucc)) ≫
            δ Y i.castSucc.succ)).toFun
      x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)) ≫
      δ Y i.succ =
    δ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)

Tactic:
ext x

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)) ≫
            δ Y i.succ)).toFun
      x =
    (ConcreteCategory.hom
          (δ X i ≫
            ↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j))).toFun
      x
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).ι
⊢ (pairingCore k.succ n).index x ≠ Fin.last ((pairingCore k.succ n).dim x + 1)

Tactic:
dsimp [pairingCore]

Goal state after:
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)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) ≫
      σ Y i.castSucc =
    σ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ)

Tactic:
ext x

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) ≫
            σ Y i.castSucc)).toFun
      x =
    (ConcreteCategory.hom
          (σ X i ≫
            ↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ))).toFun
      x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) ≫
      σ Y i.succ =
    σ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)

Tactic:
ext x

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ (ConcreteCategory.hom
          ((↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) ≫
            σ Y i.succ)).toFun
      x =
    (ConcreteCategory.hom
          (σ X i ≫
            ↾fun x ↦
              (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
                ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc))).toFun
      x
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))), ↑X)
⊢ (fun x ↦ { toFun := fun x_1 ↦ x, continuous_toFun := ⋯ }) ((fun f ↦ f.toFun default) x✝) = x✝

Tactic:
ext x

Goal state after:
X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))), ↑X)
x : ↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1)))
⊢ ((fun x ↦ { toFun := fun x_1 ↦ x, continuous_toFun := ⋯ }) ((fun f ↦ f.toFun default) x✝)) x = x✝ x
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:
dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
    Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
    Adjunction.comp, singularChainComplexFunctor,
    SSet.chainComplexFunctorAdjunction, SSet.chainComplexFunctor]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
R : C
⊢ ((Sigma.ι (fun x ↦ R) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)) ≫
        (𝟙 (∐ fun x ↦ R) ≫
            ((Adjunction.whiskerLeft C sSetTopAdj).unit.app
                    (((Functor.postcompose₂.obj (eval C (ComplexShape.down ℕ) n)).obj
                          ((Functor.postcompose₂.obj (alternatingFaceMapComplex C)).obj
                            (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C))).obj
                      R)).app
                Δ[n] ≫
              𝟙 (∐ fun x ↦ R)) ≫
          𝟙 (∐ fun x ↦ R)) ≫
      Sigma.map' ⇑(ConcreteCategory.hom ((TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)).app (Opposite.op ⦋n⦌))) fun x ↦
        𝟙 R) =
    Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom ((stdSimplexToTop.app ⦋n⦌).app (Opposite.op ⦋n⦌))) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case inr
α ι : 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 ≤ a

Tactic:
have : t ⊆ ⋃ i, f i := by
      intro x hx
      obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
      exact mem_iUnion_of_mem i hi
    calc #t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
      _ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
      _ ≤ sum (fun _ ↦ a) := sum_le_sum _ _ h'f
      _ = #ι * a := by simp
      _ ≤ ℵ₀ * a := by grw [mk_le_aleph0]
      _ = a := aleph0_mul_eq ha

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

Goal state before:
pp: case h'f
α : 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} α) := ⋯
l' : Filter (ULift.{u, v} ι) := ⋯
⊢ ∀ (i : ULift.{u, v} ι), #↑(g i) ≤ lift.{v, u} a

Tactic:
intro i
    simpa [g] using! h'f i.down

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

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s

Tactic:
filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 0)
n : ℕ
hn : (c ^ n)⁻¹ • x ∈ s
⊢ x ∈ c ^ n • s
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x = 1 ↔ w x = 1

Tactic:
simpa only [map_one] using h.eq_iff_eq (x := x) (y := 1)

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
⊢ JoinedIn sᶜ a b

Tactic:
have x_ne_zero : x ≠ 0 := by simpa [x] using sub_ne_zero.2 hab.symm

Goal state after:
case inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
⊢ JoinedIn sᶜ a b
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt f (↑i) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)

Tactic:
have hx : x ∈ R.source := HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source _

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt f (↑i) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inr.inr.inl.inl
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
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι ≠ 2
hlt : 2 < card ι
a b : R
k : ι
hk hj : k ≠ i
ha :
  1 < (restrict (fun k_1 ↦ k_1 ≠ k) v ⟨i, ⋯⟩) a ∧
    ∀ (j : { k_1 // k_1 ≠ k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 ≠ k) v j) a < 1
hb :
  1 < (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v ⟨i, ⋯⟩) b ∧
    ∀ (j : { k_1 // k_1 = i ∨ k_1 = k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v j) b < 1
ha₁ : (v k) a ≠ 1
ha_lt : (v k) a < 1
⊢ (v k) a < 1

pp: case refine_2.inr.inr.inl.inr
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
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_lt : (v j) a < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ (v k) a < 1

Tactic:
try exact ha_lt; exact ha.2 ⟨k, h⟩ (by grind)

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

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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
⊢ ‖↑A.symm (f x') - ↑A.symm y - ↑f'.symm (f x' - y)‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - y‖

Tactic:
rcases (mem_image _ _ _).1 hy with ⟨y', y's, rfl⟩

Goal state after:
𝕜 : 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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖↑A.symm (f x') - ↑A.symm (f y') - ↑f'.symm (f x' - f y')‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - f y'‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: x : ℂ
h : x ∈ slitPlane
h0 : x ≠ 0
⊢ HasStrictDerivAt (↑expOpenPartialHomeomorph) x (↑expOpenPartialHomeomorph.symm x)

Tactic:
simpa [exp_log h0] using! hasStrictDerivAt_exp (log x)

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

Goal state before:
pp: case convert_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this : AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ iteratedDeriv i (fun i ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / ↑i_1.factorial) • iteratedDeriv i_1 f 0) 0 = 0

Tactic:
iteratedDeriv_fun_sub (AnalyticAt.contDiffAt <| by fun_prop) this.contDiffAt

Goal state after:
case convert_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this : AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ iteratedDeriv i f 0 - iteratedDeriv i (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0 =
    0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ Real.log = fun x ↦ (log ↑x).re

Tactic:
ext x

Goal state after:
x✝ : ℝ
hx : 0 < x✝
x : ℝ
⊢ Real.log x = (log ↑x).re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
this :
  HasFPowerSeriesOnBall log
    (FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n))
    (ofRealCLM 1) r
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun n ↦ -(-1) ^ n / ↑n) n) fun x ↦ 1) =
    (reCLM.compFormalMultilinearSeries
        ((FormalMultilinearSeries.restrictScalars ℝ
              (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n)).compContinuousLinearMap
          ofRealCLM)
        n)
      fun x ↦ 1

Tactic:
simp only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
    ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply,
    FormalMultilinearSeries.compContinuousLinearMap_apply]

Goal state after:
r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
this :
  HasFPowerSeriesOnBall log
    (FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n))
    (ofRealCLM 1) r
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun n ↦ -(-1) ^ n / ↑n) n) fun x ↦ 1) =
    reCLM
      ((FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) n)
        (⇑ofRealCLM ∘ fun x ↦ 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹

Tactic:
simp only [id]

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case e'_9
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹

Tactic:
simp only [id]

Goal state after:
case e'_9
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (x * I) * (1 * I) + cexp (-x * I) * (-1 * I)) * 2⁻¹