mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
U₀ : C₀
b : U₀ ⟶ W₀
hb : (↑⟨(data X).sieve₁₀ q₁ q₂, ⋯⟩).arrows b
⊢ presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ F.map a ≫ F.map p₁ ≫ h₁.q) =
    presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ F.map a ≫ F.map p₂ ≫ h₂.q)

Tactic:
apply presheafObj_mapPreimage_condition

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
U₀ : C₀
b : U₀ ⟶ W₀
hb : (↑⟨(data X).sieve₁₀ q₁ q₂, ⋯⟩).arrows b
⊢ (F.map b ≫ F.map a ≫ F.map p₁ ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map b ≫ F.map a ≫ F.map p₂ ≫ h₂.q) ≫ (data X).f h₂.i₀
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ restriction.res data G₀ (Nonempty.some ⋯) = presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
apply presheafObj_mapPreimage_condition

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ (Nonempty.some ⋯).q ≫ (data X).f (Nonempty.some ⋯).i₀ = p ≫ (data X).f i
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_3.inr.refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
⊢ ∀ ⦃i j : T.affineOneHypercover.I₀⦄ (k : T.affineOneHypercover.I₁ i j),
    Presieve.IsSeparatedFor F
      (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
· intro i j k
        rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate]
        apply Presieve.IsSheafFor.isSeparatedFor
        rw [← Presieve.ofArrows_pullback]
        exact this (𝒰.pullback₂ _) ⟨_, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a ≫ H.desc (aux e ⋯) = e a

Tactic:
have := H.fac (aux e h) ⟨Over.mk (π a), a, 𝟙 _, by simp⟩
      dsimp [aux] at this; rw [this]; clear this
      conv_rhs => rw [← Category.id_comp (e a)]
      apply h
      generalize_proofs h1 h2
      rw [h2.choose_spec, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: ⊢ etalePrecoverage ≤ proetalePrecoverage

Tactic:
proetalePrecoverage,

Goal state after:
⊢ etalePrecoverage ≤ propQCPrecoverage @WeaklyEtale
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ J.yonedaEquiv (J.yoneda.map f ≫ J.yonedaEquiv.symm x) =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x))

Tactic:
rw [yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app (op X'))) f =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x))
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
u : J.yoneda.obj (unop X) ⟶ F
⊢ J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f)) (J.yonedaEquiv u)) =
    J.yoneda.map f.unop ≫ J.yonedaEquiv.symm (J.yonedaEquiv u)

Tactic:
rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Arrow.mk f = Φ.toSuccArrow X → Φ.prop f

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.prop f
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
⊢ P ≤ Q → transfiniteCompositions.{w, v, u} P ≤ Q

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
h : P ≤ Q
⊢ transfiniteCompositions.{w, v, u} P ≤ Q
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ ¬IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))

Tactic:
intro h

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
h : IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q

Tactic:
by rw [← padicNorm.mul, div_mul_cancel₀ _ hr]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
rw [min_eq_left h]; exact le_padicValRat_add_of_le hqr h

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 → (↑p)⁻¹ < padicNorm p ↑m

Tactic:
intro h

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ (↑p)⁻¹ < padicNorm p ↑m
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ p < 0 → ↑0 = 1

Tactic:
intro h

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
h : p < 0
⊢ ↑0 = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1

Tactic:
intro h

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ^ (-padicValRat p ↑m) = 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Prime p)
⊢ log p n < log p (n + 1) → log p (n + 1) ≤ padicValNat p (n + 1)

Tactic:
intro h

Goal state after:
p n : ℕ
hp : Fact (Prime p)
h : log p n < log p (n + 1)
⊢ log p (n + 1) ≤ padicValNat p (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs

Tactic:
rw [Int.natAbs_mul, padicValNat.mul]

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.natAbs ≠ 0

case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.natAbs ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f.norm = 0 → f ≈ 0

Tactic:
intro h

Goal state after:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f.norm = 0
⊢ f ≈ 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f ≈ 0 → f.norm = 0

Tactic:
intro h

Goal state after:
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f ≈ 0
⊢ f.norm = 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

Tactic:
use (⟨x, hx⟩, 1)
      rw [Submonoid.coe_one, map_one, mul_one, PadicInt.algebraMap_apply, Subtype.coe_mk]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd → IsIso c.fst

Tactic:
intro h

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
⊢ IsIso c.fst
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → IsIso c.inl

Tactic:
intro h

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
⊢ IsIso c.inl
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
s : ↥S
a : S.residueField s ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨s, a⟩) default
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨s, a⟩ ∧ l default = x

Tactic:
obtain rfl : f x = s := by simp [hx, SpecToEquivOfField]

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case hf.hj₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ (Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)).pred ⋯ ≠ 0

Tactic:
intro h

Goal state after:
case hf.hj₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
h : (Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)).pred ⋯ = 0
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 → ↑p ∣ k

Tactic:
intro h

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ‖↑k‖ < 1
⊢ ↑p ∣ k
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → A.fst = Δ

Tactic:
intro h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ A.fst = Δ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → A.EqId

Tactic:
intro h

Goal state after:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ A.EqId
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → (unop A.fst).len = (unop Δ).len

Tactic:
intro h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ (unop A.fst).len = (unop Δ).len
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len → A.fst = Δ

Tactic:
intro h

Goal state after:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ A.fst = Δ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len → (unop Δ).len ≤ (unop A.fst).len

Tactic:
intro h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop Δ).len ≤ (unop A.fst).len
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → Mono A.e

Tactic:
intro h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ Mono A.e
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
⊢ f = g

Tactic:
ext ⟨Δ⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
⊢ f.app (op Δ) = g.app (op Δ)
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      ChainComplex.of.d (fun n ↦ underlying.obj (NormalizedMooreComplex.objX X n)) (NormalizedMooreComplex.objD X)
          (n + 1) n ≫
        (inclusionOfMooreComplexMap X).f n =
    K[X].d (n + 1) n ≫ PInfty.f n

Tactic:
ChainComplex.of_d,

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      NormalizedMooreComplex.objD X n ≫ (inclusionOfMooreComplexMap X).f n =
    K[X].d (n + 1) n ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ⦋n + 1⦌ ≠ ⦋n⦌

Tactic:
intro h

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : ⦋n + 1⦌ = ⦋n⦌
⊢ False
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
⊢ f ≫ PInfty.f n = 0 → f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0

Tactic:
intro h

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ PInfty.f n = 0
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ⦋n + 1⦌ ≠ ⦋n⦌

Tactic:
intro h

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
h : ⦋n + 1⦌ = ⦋n⦌
⊢ False
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0 → f ≫ PInfty.f n = 0

Tactic:
intro h

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ f ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Preadditive.DoldKan.equivalence.counitIso.hom.app ((toKaroubiEquivalence (ChainComplex C ℕ)).functor.obj K) =
    Preadditive.DoldKan.equivalence.functor.map (isoΓ₀.hom.app K) ≫ isoN₁.hom.app (Γ.obj K) ≫ N₁Γ₀.hom.app K

Tactic:
exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp)

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom f)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
by
    apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
    intros
    rw [Path.prod_coe, ulift_apply H]
    simp

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom g)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
by
    apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
    intros
    rw [Path.prod_coe, ulift_apply H]
    simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
this✝ : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
this : IsIso (L.map p)
⊢ Function.Bijective (leftHomotopyClassToHom L)

Tactic:
← Function.Bijective.of_comp_iff _
      (LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence _ p)

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
this✝ : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
this : IsIso (L.map p)
⊢ Function.Bijective (leftHomotopyClassToHom L ∘ fun f ↦ f.postcomp p)
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A → A ≤ Subfunctor.equalizer f g

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : Subfunctor.equalizer f g = A
⊢ A ≤ Subfunctor.equalizer f g
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ A ≤ Subfunctor.equalizer f g → Subfunctor.equalizer f g = A

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : A ≤ Subfunctor.equalizer f g
⊢ Subfunctor.equalizer f g = A