mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case «0».«0»
⊢ δ ((fun i ↦ i) ⟨0, ⋯⟩) ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

pp: case «0».«1»
⊢ δ ((fun i ↦ i) ⟨1, ⋯⟩) ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Tactic:
· exact δ_comp_σ_self

Goal state after:
case «0».«1»
⊢ δ ((fun i ↦ i) ⟨1, ⋯⟩) ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
⊢ IsUpperSet s ↔ IsRelUpperSet (Subtype.val '' s) P

Tactic:
by
  refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
  · obtain ⟨a, ma, rfl⟩ := x
    exact ⟨a.2, fun b x y ↦ by simpa [h (show a ≤ ⟨b, y⟩ by exact x) ma]⟩
  · have ma : a.1 ∈ Subtype.val '' s := by simp [a.2, y]
    simpa only [mem_image, Subtype.coe_inj, exists_eq_right] using (h ma).2 x b.2

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

Goal state before:
pp: case right
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
t : Finset β
hts : t ⊆ Finset.image f s'
⊢ t.Nonempty → ∃ x ∈ K.faces, Finset.image f x = t

Tactic:
ht

Goal state after:
case right
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
t : Finset β
hts : t ⊆ Finset.image f s'
ht : t.Nonempty
⊢ ∃ x ∈ K.faces, Finset.image f x = t
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
⊢ t.Nonempty → t ∈ {s | ∃ v, s = {v}}

Tactic:
ht

Goal state after:
case right
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
⊢ t ∈ {s | ∃ v, s = {v}}
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
⊢ t.Nonempty → t ∈ {t | ∃ v, t = {v}}

Tactic:
ht

Goal state after:
case right
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
⊢ t ∈ {t | ∃ v, t = {v}}
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
⊢ t.Nonempty → t ∈ {s | ∃ v, s = {v}}

Tactic:
ht

Goal state after:
case right
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
⊢ t ∈ {s | ∃ v, s = {v}}
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
hK : K ∈ x✝
a✝ : Finset ι
⊢ a✝ ∈ (fun K ↦ K.faces) K → a✝ ∈ (fun K ↦ K.faces) (sSup x✝)

Tactic:
ht

Goal state after:
case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
hK : K ∈ x✝
a✝ : Finset ι
ht : a✝ ∈ (fun K ↦ K.faces) K
⊢ a✝ ∈ (fun K ↦ K.faces) (sSup x✝)
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
⊢ a✝ ∈ (fun K ↦ K.faces) (sSup x✝) → a✝ ∈ (fun K ↦ K.faces) L

Tactic:
ht

Goal state after:
case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
ht : a✝ ∈ (fun K ↦ K.faces) (sSup x✝)
⊢ a✝ ∈ (fun K ↦ K.faces) L
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl.left
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ g y ≤ g (f z)

Tactic:
exact g.monotone (by simpa using hz.1)

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

Goal state before:
pp: X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h : { dim := n, simplex := s }.toN.simplex ∈ A.obj (Opposite.op ⦋{ dim := n, simplex := s }.toN.dim⦌)
⊢ s ∈ A.obj (Opposite.op ⦋n⦌)

Tactic:
simp only [← ofSimplex_le_iff] at h ⊢

Goal state after:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h : ofSimplex { dim := n, simplex := s }.toN.simplex ≤ A
⊢ ofSimplex s ≤ A
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2

Tactic:
rw [Prod.lt_iff]

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Mono (yonedaEquiv.symm x)

Tactic:
exact Nonsingular.mono' x hx

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) (h.equivII y)
⊢ f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))

Tactic:
← ancestralRel_iff

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
obtain ⟨x, rfl⟩ := h.equivII.surjective x
        obtain ⟨y, rfl⟩ := h.equivII.surjective y
        rw [← ancestralRel_iff] at hxy
        simpa using f.lt hxy

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) (h.equivII y)
⊢ (↑(h.equivII x)).dim = (↑(h.equivII y)).dim →
    f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))

Tactic:
← ancestralRel_iff

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ (↑(h.equivII x)).dim = (↑(h.equivII y)).dim →
    f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ (↑x).dim = (↑y).dim → f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
obtain ⟨x, rfl⟩ := h.equivII.surjective x
        obtain ⟨y, rfl⟩ := h.equivII.surjective y
        rw [← ancestralRel_iff] at hxy
        simpa using f.lt hxy

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.pairing.IsProper ↔ h.IsProper

Tactic:
by
  refine ⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩
  simpa [type₁_pairing] using h.pairing.isUniquelyCodimOneFace (h.equivII s)

Goal state after:
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
⊢ f.app (op ⦋0⦌) = hom H 0 1 ≫ ((alternatingFaceMapComplex C).obj Y).d 1 0 + g.app (op ⦋0⦌)

Tactic:
simp [← H.h_last_comp_δ_last 0]

Goal state after:
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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ c.horn.image c.map < (↑(P.p c.s)).subcomplex

Tactic:
rw [lt_iff_le_and_ne]
  exact ⟨by simpa using! image_le_range c.horn c.map,
    fun h ↦ c.subcomplex_not_le_image_horn (by simpa only [h] using! P.le c.s)⟩

Goal state after:
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 ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ (↑(P.p c.s)).subcomplex ≤ ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
exact le_trans (by rfl) (le_iSup _ c)

Goal state after:
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✝ : OrderBot ι
⊢ f.filtration ⊥ = A

Tactic:
by
  simp [filtration_def]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X : C
⊢ ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p

Tactic:
obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS X

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X : C
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ X
h✝ : ExtremalEpi p
⊢ ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.smallCategoryOfSet.obj
f : (𝟭 ↑h.smallCategoryOfSet.obj).obj x ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y
x' y' : ↑h.smallCategoryOfSet.obj
g : (𝟭 ↑h.smallCategoryOfSet.obj).obj x' ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y'
hfg :
  h.functor.mapArrow.obj { left := x, right := y, hom := f } =
    h.functor.mapArrow.obj { left := x', right := y', hom := g }
⊢ { left := x, right := y, hom := f } = { left := x', right := y', hom := g }

Tactic:
obtain rfl : x = x' := by simpa using! congr_arg Arrow.leftFunc.obj hfg

Goal state after:
case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.smallCategoryOfSet.obj
f : (𝟭 ↑h.smallCategoryOfSet.obj).obj x ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y
y' : ↑h.smallCategoryOfSet.obj
g : (𝟭 ↑h.smallCategoryOfSet.obj).obj x ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y'
hfg :
  h.functor.mapArrow.obj { left := x, right := y, hom := f } =
    h.functor.mapArrow.obj { left := x, right := y', hom := g }
⊢ { left := x, right := y, hom := f } = { left := x, right := y', hom := g }
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
⊢ Function.Injective fun X ↦ Arrow.mk (𝟙 X)

Tactic:
intro X Y h

Goal state after:
κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
X Y : C
h : (fun X ↦ Arrow.mk (𝟙 X)) X = (fun X ↦ Arrow.mk (𝟙 X)) Y
⊢ X = Y
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case h₀
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₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α) ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.fst =
    ((Arrow.mk f₂).hom ≫ ⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ≫
      sq₁₃.fst

pp: case h₁
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₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α) ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd =
    ((Arrow.mk f₂).hom ≫ ⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ≫
      sq₁₃.snd

Tactic:
· simp [← adj₂.homEquiv_naturality_two,
                ← adj₂.homEquiv_naturality_one,
                sq₁₂.isPushout.w_assoc]

Goal state after:
case h₁
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₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α) ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd =
    ((Arrow.mk f₂).hom ≫ ⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ≫
      sq₁₃.snd
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 : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : i ∈ finset x hd
⊢ l.succ ≤ i

Tactic:
rw [mem_finset_iff] at hi

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : (x.cast hd).simplex.1 i = k.succ
⊢ l.succ ≤ i
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 : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin (hl.δ.dim + 1)
⊢ ¬IsIndex hl.δ ⋯ t

Tactic:
ht

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin (hl.δ.dim + 1)
ht : IsIndex hl.δ ⋯ t
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) l.castSucc)) (x.cast hd).simplex
⊢ l.castSucc = l.castSucc ∨ l.castSucc = l.succ

pp: case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : l.castSucc < i
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
· exact Or.inl rfl

Goal state after:
case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : l.castSucc < i
⊢ i = l.castSucc ∨ i = l.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ IsColimit (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    (Preadditive.isColimitCokernelCoforkOfCofork
      ((isColimitMapCoconeCoforkEquiv _ _).1
        (isColimitOfPreserves (sigmaConst.obj R) X.isColimitCoforkπ₀)))

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ parallelPair ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0)) 0 ≅
    parallelPair ((X.chainComplex R).d 1 0) 0

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj
      (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯)) ≅
    CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Goal state before:
pp: X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
h : f.Homotopy g
f' : RelativeMorphism B C ψ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ A.ι ▷ Δ[1] ≫ h.h ≫ f'.map = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι

Tactic:
by simp [h.rel_assoc, ← fac]

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:
have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx

Goal state after:
α ι : 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
this : s ⊆ u
⊢ s.card ≤ u.card
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
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
let c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
  have hcᵢ : Tendsto (fun n ↦ v i (c n)) atTop (𝓝 (v i b)) := by
    have : v i a⁻¹ < 1 := map_inv₀ (v i) a ▸ inv_lt_one_of_one_lt₀ ha
    simpa [c] using (tendsto_div_one_add_pow_nhds_one this).mul_const (v i b)
  have hcⱼ (j : ι) (hj : j ≠ i) : atTop.Tendsto (fun n ↦ v j (c n)) (𝓝 0) := by
    have : 1 < v j a⁻¹ := map_inv₀ (v j) _ ▸
      (one_lt_inv₀ <| (v j).pos fun h ↦ by linarith [map_zero (v _) ▸ h ▸ ha]).2 (haj j hj)
    simpa [c] using (tendsto_div_one_add_pow_nhds_zero this).mul_const _
  have hcₙ : atTop.Tendsto (fun n ↦ w (c n)) (𝓝 (w b)) := by
    have : w a⁻¹ < 1 := map_inv₀ w _ ▸ inv_lt_one_of_one_lt₀ haw
    simpa [c] using (tendsto_div_one_add_pow_nhds_one this).mul_const (w b)
  simp_rw +instances [OrderTopology.topology_eq_generate_intervals,
    TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_atTop_sets, Set.mem_preimage] at hcⱼ
  choose r₁ hr₁ using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_const_lt hb hcᵢ
  choose rₙ hrₙ using fun j hj ↦ hcⱼ j hj (.Iio 1) (by simpa using ⟨1, .inr rfl⟩) (by simp)
  choose rN hrN using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_lt_const hbw hcₙ
  have := Fintype.ofFinite ι
  let r := max (Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h) rN
  refine ⟨c r, hr₁ r ?_, fun j hj ↦ ?_, ?_⟩
  · exact le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl
  · exact hrₙ j hj _ <| le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_neg (fun j ↦ j = i) (Finset.mem_univ j) _
  · exact hrN _ <| le_max_iff.2 (.inr le_rfl)

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

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
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
s : Set E
has : s ∈ 𝓝 a
hs : s ×ˢ s ⊆ {x | ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ ≤ ↑c * ‖x.1 - x.2‖}
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
exact ⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩

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
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) / log (v a) < ↑q.num / ↑q.den
hq₂ : ↑q.num / ↑q.den < log (w b) / log (w a)
⊢ False

Tactic:
div_lt_div_iff₀ (log_pos ha) (by simp [q.den_pos]),

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) * ↑q.den < ↑q.num * log (v a)
hq₂ : ↑q.num / ↑q.den < log (w b) / log (w a)
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

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

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

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
                        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
                      ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
                    ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹⁻¹ *
                  ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
                ‖↑n !‖⁻¹⁻¹ *
              ‖↑n !‖⁻¹ *
            ‖a + ↑n‖⁻¹ *
          ‖b + ↑n‖⁻¹ *
        ‖c + ↑n‖⁻¹⁻¹ *
      ‖1 + ↑n‖⁻¹⁻¹ =
    ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖

Tactic:
simp only [inv_inv]
      repeat rw [DivisionRing.mul_inv_cancel, one_mul]
      all_goals
        rw [norm_ne_zero_iff]
      any_goals
        apply (ascPochhammer_eval_eq_zero_iff n _).not.2
        push Not
        exact fun kn hkn ↦ by simp [habc kn hkn]
      exact cast_ne_zero.2 (factorial_ne_zero n)

Goal state after: