mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
⊢ Arrow.mk ((iter l₁ ⋯).mapObj (iter l₂ ⋯) ⋯ ⋯ ⋯ ⋯) = Arrow.mk ((functor hj iter).map (homOfLE ⋯))

Tactic:
generalize_proofs

Goal state after:
case inr.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ Arrow.mk ((iter l₁ pf✝⁹).mapObj (iter l₂ pf✝⁷) pf✝⁵ pf✝⁴ pf✝³ pf✝⁵) = Arrow.mk ((functor hj iter).map (homOfLE pf✝))
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val)

Tactic:
← op_comp,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯ ≫ homOfLE hij).op)) e.val =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯ ≫ homOfLE hij).op)) e.val =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val)

Tactic:
← op_comp,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯ ≫ homOfLE hij).op)) e.val =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯ ≫ homOfLE hij).op)) e.val)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE hki).op))) e.val =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩

Tactic:
← op_comp,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hki ≫ homOfLE hij).op)) e.val =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (homOfLE hij').op))) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩

Tactic:
← op_comp,

Goal state after:
case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE hij' ≫ homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (q.num * r.num)

Tactic:
· simp [finite_int_prime_iff, hq, hr]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Tactic:
obtain ⟨o, j, hj⟩ := exists_ordinal hG (Subobject.mk f)
  have : Nonempty o.ToType := ⟨j⟩
  have : OrderBot o.ToType := WellFoundedLT.toOrderBot _
  exact ⟨_, _, _, _, _, ⟨transfiniteCompositionOfShapeOfEqTop hG hj⟩⟩

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
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q < padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q

Tactic:
rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]

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
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q < padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q

Tactic:
by
  rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
⊢ ↑(PadicSeq.norm ⟨fun n ↦ ↑(seq n), h⟩) ≤ 1

Tactic:
PadicSeq.norm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
⊢ ↑(if hf : ⟨fun n ↦ ↑(seq n), h⟩ ≈ 0 then 0 else padicNorm p (↑⟨fun n ↦ ↑(seq n), h⟩ (PadicSeq.stationaryPoint hf))) ≤
    1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ = 1 ↔ IsCoprime z ↑p

Tactic:
rw [norm_def, coe_intCast, Padic.norm_intCast_eq_one_iff]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ False

Tactic:
← hnam,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < padicNorm p (-↑f m + ↑f n)
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ IsUnit ((algebraMap ℤ_[p] ℚ_[p]) ↑⟨x, hx⟩)

Tactic:
algebraMap_apply,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ IsUnit ↑↑⟨x, hx⟩
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ {x y : ℤ_[p]}, (algebraMap ℤ_[p] ℚ_[p]) x = (algebraMap ℤ_[p] ℚ_[p]) y → ∃ c, ↑c * x = ↑c * y

Tactic:
algebraMap_apply,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ {x y : ℤ_[p]}, ↑x = ↑y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : LocallySmall.{w, v, u} C
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
inst✝ : HasSheafify J (Type w)
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
hf : ∀ (Φ : P.FullSubcategory), Epi (↾⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f)))
⊢ Presheaf.IsLocallySurjective J f

Tactic:
rw [Presheaf.isLocallySurjective_iff_whisker_forget,
    ← Presheaf.isLocallySurjective_presheafToSheaf_map_iff,
    Sheaf.isLocallySurjective_iff_epi,
    (hP.jointlyReflectEpimorphisms (Type w)).epi_iff]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : LocallySmall.{w, v, u} C
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
inst✝ : HasSheafify J (Type w)
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
hf : ∀ (Φ : P.FullSubcategory), Epi (↾⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f)))
⊢ ∀ (i : P.FullSubcategory),
    Epi (i.obj.sheafFiber.map ((presheafToSheaf J (Type w)).map (Functor.whiskerRight f (forget A))))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
by
  unfold norm; split_ifs
  -- Porting note: originally `padic_index_simp [hfg, hf, hg]`
  rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
  apply padicNorm.nonarchimedean

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ max 0 g.norm = g.norm

Tactic:
exact max_eq_right (norm_nonneg _)

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

Goal state before:
pp: case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : Spec (CommRingCat.of Ω) ⟶ X
𝒰 : Cover (precoverage @Etale) (Etale.mk f).left
h : Cover.Over S 𝒰
w✝ : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp w✝ ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = φ default
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1),
      ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk (φ ≫ f)))).map f_1)) y = Over.homMk φ ⋯

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := exists_fac_of_etale_of_isSepClosed (𝒰.f i) φ _ hy

Goal state after:
case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : Spec (CommRingCat.of Ω) ⟶ X
𝒰 : Cover (precoverage @Etale) (Etale.mk f).left
h : Cover.Over S 𝒰
w✝ : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp w✝ ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = φ default
l : Spec (CommRingCat.of Ω) ⟶ 𝒰.X i
hl₁ : l ≫ 𝒰.f i = φ
hl₂ : l default = y
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1),
      ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk (φ ≫ f)))).map f_1)) y = Over.homMk φ ⋯
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ yonedaEquiv
      (yoneda.map (toGlued hf i) ≫
        { hom := yonedaEquiv.symm ((glueData hf).sheafValGluedMk (fun i ↦ yonedaEquiv (f i)) ⋯) }.hom) =
    yonedaEquiv (f i)

Tactic:
yonedaEquiv_apply,

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ (ConcreteCategory.hom
        ((yoneda.map (toGlued hf i) ≫
              { hom := yonedaEquiv.symm ((glueData hf).sheafValGluedMk (fun i ↦ yonedaEquiv (f i)) ⋯) }.hom).app
          (op (X i))))
      (𝟙 (X i)) =
    yonedaEquiv (f i)
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ (ConcreteCategory.hom
        ((yoneda.map (toGlued hf i) ≫
              { hom := yonedaEquiv.symm ((glueData hf).sheafValGluedMk (fun i ↦ yonedaEquiv (f i)) ⋯) }.hom).app
          (op (X i))))
      (𝟙 (X i)) =
    yonedaEquiv (f i)

Tactic:
yonedaEquiv_apply,

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ (ConcreteCategory.hom
        ((yoneda.map (toGlued hf i) ≫
              { hom := yonedaEquiv.symm ((glueData hf).sheafValGluedMk (fun i ↦ yonedaEquiv (f i)) ⋯) }.hom).app
          (op (X i))))
      (𝟙 (X i)) =
    (ConcreteCategory.hom ((f i).app (op (X i)))) (𝟙 (X i))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ (↑i + 1) * ε

Tactic:
rw [right_distrib]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε + 1 * ε
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso = equivalenceCounitIso η

Tactic:
ext1; apply NatTrans.ext; ext Y
  dsimp [equivalence]
  simp only [comp_id, id_comp, Functor.map_comp, equivalence₂CounitIso_eq,
    equivalence₂CounitIso_hom_app, assoc, equivalenceCounitIso_hom_app]
  simp only [equivalence₂_inverse, comp_obj, ← τ₀_hom_app, hη, τ₁_hom_app, ←
    eB.inverse.map_comp_assoc]
  rw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]
  congr 2
  simp only [← e'.functor.map_comp_assoc]
  simp only [Functor.comp_map, Equivalence.fun_inv_map, comp_obj, id_obj, map_comp, assoc]
  simp only [← e'.functor.map_comp_assoc]
  simp only [Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_obj, comp_id,
    Equivalence.functor_unit_comp, map_id, id_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + Q q = 𝟙 K[X]

Tactic:
Q

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
⊢ ∃ b snd fst, IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g

Tactic:
obtain ⟨_, ⟨_, ⟨_, pbRepr⟩⟩⟩ := h (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
w✝² : C
w✝¹ : w✝² ⟶ a
w✝ : F.obj w✝² ⟶ F.obj a
pbRepr :
  IsPullback w✝ (F.map w✝¹) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
    (g ≫ pullback.snd (terminal.from X) (terminal.from X))
⊢ ∃ b snd fst, IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨i, ⋯⟩ + ((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ =
    0

Tactic:
generalize_proofs

Goal state after:
case a
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
pf✝⁴ : IsRightCancelAdd ℕ
pf✝³ : a + 1 < n + 1 + 1
pf✝² : i < n + 1 + 2
pf✝¹ : i < n + 2
pf✝ : a < n + 1
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, pf✝³⟩ ≫ X.δ ⟨i, pf✝²⟩ +
      ((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩ =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Tactic:
rw [hi]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ PInfty.f (n✝ + 1) = 0

Tactic:
obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : ⦋n✝⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map θ.op ≫ PInfty.f (n✝ + 1) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e

Tactic:
unop_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e ≫ 𝟙 (unop A.fst) = 𝟙 (unop Δ) ≫ A.e
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i ↦ ⇑(f i)) x✝

Tactic:
simp [inf'_apply]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ IsIso (Γ₂N₁.natTrans.app X)

Tactic:
compatibility_Γ₂N₁_Γ₂N₂_natTrans

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ IsIso ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X))
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case neg.e_6.e_fst
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ ⟨2 * (1 - ↑t), ⋯⟩ = σ ⟨2 * ↑t - 1, ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
case neg.e_6.e_fst
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ ↑⟨2 * (1 - ↑t), ⋯⟩ = ↑(σ ⟨2 * ↑t - 1, ⋯⟩)