mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x ⊗ y✝ ⟶ z✝
y z : SimplexCategory
f g : WithInitial.star ⊗ WithInitial.of y ⟶ WithInitial.of z
h₁ : inl WithInitial.star (WithInitial.of y) ≫ f = inl WithInitial.star (WithInitial.of y) ≫ g
h₂ : inr WithInitial.star (WithInitial.of y) ≫ f = inr WithInitial.star (WithInitial.of y) ≫ g
⊢ f = g

Tactic:
simp only [inr, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self,
        id_star_whiskerRight] at h₂
      simpa [Category.id_comp f, Category.id_comp g] using h₂

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
⊢ { dim := x.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }

Tactic:
by
  obtain ⟨d, x, rfl⟩ := x.mk_surjective
  obtain ⟨d', y, rfl⟩ := y.mk_surjective
  obtain rfl : d' = d + 1 := hxy.dim_eq
  rw [iff] at hxy ⊢
  simpa [← SSet.δ_naturality_apply, dsimp% (e.app (Opposite.op ⦋d⦌)).toEquiv.apply_eq_iff_eq]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
⊢ Monotone (map' f)

Tactic:
intro x

Goal state after:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ ∀ ⦃b : Fin (m + 2)⦄, x ≤ b → map' f x ≤ map' f b
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ (↑(P.p s)).toS = (↑(P.p t)).toS

Tactic:
← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ ((↑(P.p s)).cast ⋯).toS = (↑(P.p t)).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ ↑(P.p s) = ↑t

Tactic:
← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ (↑(P.p s)).cast ⋯ = ↑t
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ α x = -β (x.2.succ, x.1.castSucc)

Tactic:
dsimp [α, β]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1 = -((-1) ^ (↑x.2 + 1 + ↑x.1) • H.h x.1.castSucc ≫ Y.δ x.2.succ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
d : ℕ
⊢ Function.Injective ⇑(ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌)))

Tactic:
intro x

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
d : ℕ
x : Δ[c.dim + 1] _⦋d⦌
⊢ ∀ ⦃a₂ : (fun X ↦ X) (Δ[c.dim + 1] _⦋d⦌)⦄,
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) x =
        (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) a₂ →
      x = a₂
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0

Tactic:
have eq₅ : ∑ x, β (γ₄ x) = - ∑ x, β (γ₃ x) := by
    rw [← Finset.sum_neg_distrib]
    exact Finset.sum_congr rfl (fun x hx ↦ by simp [h_succ_comp_δ_castSucc_succ, β, γ₃, γ₄])

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
this : IsSplitEpi i
⊢ IsIso i

Tactic:
obtain ⟨r, fac⟩ := this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
r : Y ⟶ X
fac : r ≫ i = 𝟙 Y
⊢ IsIso i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : ↑c.s = ↑(P.p c'.s)
⊢ Cell.type₂ f c = Cell.type₁ f c'

pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : c.s = c'.s
⊢ Cell.type₂ f c = Cell.type₂ f c'

Tactic:
· exact (P.ne _ _ h.symm).elim

Goal state after:
case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : c.s = c'.s
⊢ Cell.type₂ f c = Cell.type₂ f c'
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
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ IsZero (X.homology R n)

Tactic:
rw [← exactAt_iff_isZero_homology]
  exact X.exactAt_chainComplex_of_hasDimensionLT R n d

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 : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this✝ : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
i : Fin ((s.x.cast ⋯).dim + 1)
hi : (s.x.cast ⋯).simplex.1 i = 0
this : (fun j ↦ (s.x.cast ⋯).simplex.1 j) 0 ≤ (fun j ↦ (s.x.cast ⋯).simplex.1 j) i
⊢ False

Tactic:
have h₁ := hs.simplex_fst_castSucc

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this✝ : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
i : Fin ((s.x.cast ⋯).dim + 1)
hi : (s.x.cast ⋯).simplex.1 i = 0
this : (fun j ↦ (s.x.cast ⋯).simplex.1 j) 0 ≤ (fun j ↦ (s.x.cast ⋯).simplex.1 j) i
h₁ : (s.x.cast ⋯).simplex.1 (Fin.castSucc 0) = k.succ.castSucc
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: case e_6
⊢ (ConcreteCategory.hom
        (toTop.map (stdSimplex.δ 1) ≫
          (TopCat.isoOfHomeo
              (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
      default =
    0

Tactic:
have : stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo
      (((toTop.{u}.map (stdSimplex.δ 1)).hom) default)) = 0 := by
    rw [← stdSimplexHomeomorphUnitInterval_zero]
    congr 1
    refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
    rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
    rfl

Goal state after:
case e_6
this : stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1))) default)) = 0
⊢ (ConcreteCategory.hom
        (toTop.map (stdSimplex.δ 1) ≫
          (TopCat.isoOfHomeo
              (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
      default =
    0
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:
intro x

Goal state after:
α ι : 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
x : α
⊢ x ∈ t → x ∈ ⋃ i, f i
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} α) := ⋯
l' : Filter (ULift.{u, v} ι) := ⋯
⊢ ∀ x ∈ ULift.down ⁻¹' t, ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i

Tactic:
intro x

Goal state after:
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} α
⊢ x ∈ ULift.down ⁻¹' t → ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i
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), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s

Tactic:
intro x

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
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: 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 := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c - x -[ℝ] c + t • y] ∩ [c - x -[ℝ] c + t' • y] ⊆ {c - x}

Tactic:
sub_eq_add_neg _ x

Goal state after:
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
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c + -x -[ℝ] c + t • y] ∩ [c + -x -[ℝ] c + t' • y] ⊆ {c + -x}
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
⊢ ∃ y, dist z ((algebraMap F ((i : ι) → WithAbs (v i))) y) < r

Tactic:
choose a hx using exists_one_lt_lt_one_pi_of_not_isEquiv h hv

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
⊢ ∃ y, dist z ((algebraMap F ((i : ι) → WithAbs (v i))) y) < r
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ nerve.homEquiv ((Edge.id x).map φ) =
    𝟙 (nerveEquiv ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) x))

Tactic:
by simpa using! nerve.homEquiv_id (φ.app _ x)

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

Goal state before:
pp: case top
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0

Tactic:
obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp h

Goal state after:
case top
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = f x
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inr
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
hc : c < f'symm.nnnorm⁻¹
hs : ∀ x ∈ s, ∃ i, 0 < i ∧ closedBall x i ⊆ s
⊢ ∀ ⦃x : E⦄, x ∈ s → ∃ i, 0 < i ∧ closedBall (f x) i ⊆ f '' s

Tactic:
intro x

Goal state after:
case inr
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
hc : c < f'symm.nnnorm⁻¹
hs : ∀ x ∈ s, ∃ i, 0 < i ∧ closedBall x i ⊆ s
x : E
⊢ x ∈ s → ∃ i, 0 < i ∧ closedBall (f x) i ⊆ f '' s
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ deriv (fun x_1 ↦ (x_1 - x) ^ r • F x_1) x = 0

Tactic:
deriv_fun_smul (by fun_prop) (by fun_prop),

Goal state after:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ (x - x) ^ r • deriv F x + deriv (fun x_1 ↦ (x_1 - x) ^ r) x • F x = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
div_eq_inv_mul

Goal state after:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t ↦ log (f t)) ((f x)⁻¹ * f') x
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
simpa only [div_eq_inv_mul] using! (hasStrictFDerivAt_log_real h₂).comp_hasStrictDerivAt x h₁

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
div_eq_inv_mul

Goal state after:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t ↦ log (f t)) ((f x)⁻¹ * f') x
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t ↦ log (f t)) (f' / f x) s x

Tactic:
div_eq_inv_mul

Goal state after:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t ↦ log (f t)) ((f x)⁻¹ * f') s x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: z : ℂ
m : z ∈ slitPlane
⊢ AnalyticAt ℂ log z

Tactic:
by
  rw [analyticAt_iff_eventually_differentiableAt]
  filter_upwards [isOpen_slitPlane.eventually_mem m]
  intro z m
  exact differentiableAt_id.clog m

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
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ F,
    AnalyticAt 𝕜 F 0 ∧ ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z

Tactic:
by
  classical
  obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n
  obtain ⟨U, hU0, hU'⟩ := by rwa [eventually_iff_exists_mem] at hF
  refine ⟨fun z ↦ if z ∈ U then F z else (z ^ n)⁻¹ • (f z
      - (∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0)), ?_, fun z ↦ ?_⟩
  · exact hFa.congr (by filter_upwards [hU0] using by simp +contextual)
  · by_cases hz : z ∈ U
    · simpa [hz] using hU' z hz
    · simp only [if_neg hz]
      rw [smul_inv_smul₀]
      · module
      · contrapose hz
        exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0

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
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n✝ m : ℕ
n : ℕ∞
⊢ n = ↑m ↔ ↑m ≤ n ∧ ¬↑m + 1 ≤ n

Tactic:
cases n with | top => simp | coe _ => norm_cast; lia

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ MeromorphicAt (f + g) x

Tactic:
refine ⟨max m n, ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ max m n • (f + g) z) x