mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ ¬F.map g = 0 ↔ g ≠ 0

Tactic:
ne_eq,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ ¬F.map g = 0 ↔ ¬g = 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False

Tactic:
Simple.mono_isIso_iff_nonzero

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : f ≫ i.hom ≠ 0
⊢ False
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
e : φ = ψ
X : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (ψ.hom.app U)

Tactic:
subst e

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (φ.hom.app U)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
e : φ = ψ
X : SheafOfModules R
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((forget S).obj ((pushforward φ).obj X)).map x✝ ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map x✝))).map
        ((ModuleCat.restrictScalarsCongr ⋯).app
            (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝¹)).hom =
    ((ModuleCat.restrictScalarsCongr ⋯).app
          (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝²)).hom ≫
      ((forget S).obj ((pushforward ψ).obj X)).map x✝

Tactic:
subst e

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : SheafOfModules R
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((forget S).obj ((pushforward φ).obj X)).map x✝ ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map x✝))).map
        ((ModuleCat.restrictScalarsCongr ⋯).app
            (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝¹)).hom =
    ((ModuleCat.restrictScalarsCongr ⋯).app
          (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝²)).hom ≫
      ((forget S).obj ((pushforward φ).obj X)).map x✝
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
e : φ = ψ
X✝ Y✝ : SheafOfModules R
x✝ : X✝ ⟶ Y✝
⊢ (pushforward φ).map x✝ ≫
      ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y✝.val).obj U))
            ⋯)).hom =
    ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X✝.val).obj U))
            ⋯)).hom ≫
      (pushforward ψ).map x✝

Tactic:
subst e

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X✝ Y✝ : SheafOfModules R
x✝ : X✝ ⟶ Y✝
⊢ (pushforward φ).map x✝ ≫
      ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y✝.val).obj U))
            ⋯)).hom =
    ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X✝.val).obj U))
            ⋯)).hom ≫
      (pushforward φ).map x✝
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
Y : D
⊢ Sieve.ofObjects (fun i ↦ i.fst) Y ∈ K Y

Tactic:
refine K.superset_covering ?_ <| G.cover_lift K _ (P.coversTop (G.obj Y))

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
Y : D
⊢ Sieve.functorPullback G (Sieve.ofObjects P.X (G.obj Y)) ≤ Sieve.ofObjects (fun i ↦ i.fst) Y
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ m = F.interUnionPullbackConeLift U V s

Tactic:
← cancel_mono (F.1.map (eqToHom hι.symm).op)

Goal state after:
case property.refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ m ≫ F.obj.map (eqToHom ⋯).op = F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
x : ↑S.X₂.toModuleCat
z : ↑S.X₁.toModuleCat
hy : (ConcreteCategory.hom S.g) (↑(Hom.hom S.f) z + x) = 0
e : (ConcreteCategory.hom D₂.p) (↑(Hom.hom S.f) z + x) = (ConcreteCategory.hom D₂.p) x
hz : ↑(Hom.hom S.f) z = ↑(Hom.hom S.f) z + x - x
⊢ (ConcreteCategory.hom S.g) x = 0

Tactic:
simpa [show S.g (S.f z) = 0 from ConcreteCategory.congr_hom S.zero z] using hy

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ (f.inv * ↑f) x = x

Tactic:
rw [f.inv_val]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ 1 x = x
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
⊢ ¬eqToHom ⋯ ≫ Hom.fst b = eqToHom ⋯ ≫ Hom.snd b

Tactic:
let f : ((left a : WalkingMulticospan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False

Goal state after:
case pos
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ¬eqToHom ⋯ ≫ Hom.fst b = eqToHom ⋯ ≫ Hom.snd b
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (ContinuousLinearMap.id R M).inverse = ContinuousLinearMap.id R M

Tactic:
rw [← ringInverse_eq_inverse]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (ContinuousLinearMap.id R M)⁻¹ʳ = ContinuousLinearMap.id R M
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case pos
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b

Tactic:
choose m b hb using fun (i : ι × ι) ↦ h₂ (f i.1 ≫ a) (f i.2 ≫ a)

Goal state after:
case pos
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (i : ι × ι), (f i.1 ≫ a) ≫ F.map (b i) = (f i.2 ≫ a) ≫ F.map (b i)
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
⊢ { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
            map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents (fun c ↦ c.eta) ⋯).hom.app c) ≫
      (NatIso.ofComponents
              (fun X_1 ↦
                BinaryFan.ext
                  (Over.isoMk
                    (Iso.refl
                      (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                                  map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯,
                                  map_comp := ⋯ } ⋙
                                { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                                  map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                                  map_comp := ⋯ }).obj
                            X_1).pt.left)
                    ⋯)
                  ⋯ ⋯)
              ⋯).hom.app
        ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj
          c) =
    𝟙
      ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
            map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj
        c)

Tactic:
ext; simp [BinaryFan.ext]

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

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})

Tactic:
· apply Under.closedUnderColimitsOfShape_discrete_empty _

Goal state after:
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Tactic:
by
  have hch := CharP.cast_eq_zero R (ringChar R)
  have hp : p.Prime := Fact.out
  constructor
  · rintro h₁ ⟨q, hq⟩
    rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩
    have h₃ : ¬ringChar R ∣ q := by
      rintro ⟨r, hr⟩
      rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
      nth_rw 1 [← mul_one (ringChar R)] at hq
      exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
    simp_all only [ne_eq]
    grind [ringChar.dvd]
  · intro h
    rcases (hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
    apply_fun ((↑) : ℤ → R) at hab
    push_cast at hab
    rw [hch, mul_zero, add_zero, mul_comm] at hab
    exact .of_mul_eq_one a hab

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case hg
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q ?g

pp: case hfg
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯ ≫ ?g)

pp: case g
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ ((map Q hPf ⋙ pullback P Q f).obj A).left ⟶ ?m.150

pp: T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ T

Tactic:
· exact Q.pullback_fst _ _ hQf

Goal state after:
case hfg
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯ ≫ pullback.fst ((map Q hPf).obj A).hom f)
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
⊢ IsUnit ↑a

Tactic:
by_contra g

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ¬IsUnit ↑a
⊢ False
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
⊢ ↑(r ^ n) = 0

Tactic:
← one_mul (↑(r ^ n) : R),

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
⊢ 1 * ↑(r ^ n) = 0
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ x = y

Tactic:
← Option.some_inj,

Goal state after:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ some x = some y
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case inl
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
get_drop,

Goal state after:
case inl
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ (x ++ₛ a).get (n + k) = (List.drop n x ++ₛ a).get k
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)

Tactic:
get_drop,

Goal state after:
case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
⊢ (x ++ₛ a).get (n + (m + p)) = (List.drop n x ++ₛ a).get (m + p)
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.nums 1 = gp.b * g.h + gp.a

Tactic:
by simp [num_eq_conts_a, first_cont_eq zeroth_s_eq]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ pred_conts.a * (g.contsAux (n + 1 + 1)).b - pred_conts.b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
let ppA := ppred_conts.a

Goal state after:
case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
⊢ pred_conts.a * (g.contsAux (n + 1 + 1)).b - pred_conts.b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0