mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_1
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✝¹
C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
J✝ : GrothendieckTopology C✝
K : GrothendieckTopology D
F : C✝ ⥤ D
G : D ⥤ C✝
S : Sheaf J✝ RingCat
R✝ : Sheaf K RingCat
inst✝⁴ : F.IsContinuous J✝ K
inst✝³ : G.IsContinuous K J✝
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R✝
ψ : R✝ ⟶ (G.sheafPushforwardContinuous RingCat K J✝).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R✝.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
C : Type u'
inst✝² : Category.{v', u'} C
inst✝¹ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
x✝¹ : (Over Y)ᵒᵖ
x✝ : ↑(((𝟭 (Over Y)).op ⋙ (R.over Y).obj).obj x✝¹)
⊢ (RingCat.Hom.hom ((whiskerRight (NatTrans.op (Over.mapPullbackAdj f).counit) (R.over Y).obj).app x✝¹)) x✝ =
    (RingCat.Hom.hom
        (((R.toPushforwardOverPullback f).hom ≫
              (Over.pullback f).op.whiskerLeft (R.pushforwardOverMapIso f).inv.hom).app
          x✝¹))
      x✝

Tactic:
simp [Sheaf.pushforwardOverMapIso]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case pair
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.pair i j)))) s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Tactic:
· rw [← (F.mapCone (Pairwise.cocone U).op).w (op <| Pairwise.Hom.left i j)]
    exact congr_arg _ (h i)

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.obj U sf
⊢ s = t

Tactic:
obtain ⟨gl, -, gl_uniq⟩ := F.existsUnique_gluing U sf sf_compatible

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.obj U sf
gl : ToType (F.obj.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
⊢ s = t
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : (Opens ↑X)ᵒᵖ
φ ψ : ((pullback C f).obj F).obj U ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop U ≤ (Opens.map f).obj V),
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
⊢ φ = ψ

Tactic:
by
  apply ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F _).hom_ext
  rintro ⟨⟨V⟩, ⟨⟩, ⟨b⟩⟩
  simpa [pullbackPushforwardAdjunction, Functor.lanAdjunction_unit]
    using! h V (leOfHom b)

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F : Presheaf C X
x : ↑X
U : Opens ↑X
hxU : x ∈ U
s : ToType (F.obj (op U))
V : Opens ↑X
hV : V ∈ B
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ (ConcreteCategory.hom (F.germ V x hxV)) ((ConcreteCategory.hom (F.map (homOfLE hVU).op)) s) =
    (ConcreteCategory.hom (F.germ U x hxU)) s

Tactic:
rw [← ConcreteCategory.comp_apply, F.germ_res']

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
⊢ s = t

Tactic:
choose V m i₁ i₂ heq using fun x : U => F.presheaf.germ_eq x.1 x.2 x.2 s t (h x.1 x.2)
  -- Since `F` is a sheaf, we can prove the equality locally, if we can show that these
  -- neighborhoods form a cover of `U`.
  apply F.eq_of_locally_eq' V U i₁
  · intro x hxU
    simp only [Opens.mem_iSup]
    exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
  · intro x
    rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
⊢ Continuous[Pi.topologicalSpace, inst✝²] ⇑f

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
⊢ Continuous[Pi.topologicalSpace, inst✝²] ⇑f
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
f : M₁ × M₂ →L[R] M
⊢ (fun f ↦ f.1.coprod f.2) ((fun f ↦ (f ∘SL inl R M₁ M₂, f ∘SL inr R M₁ M₂)) f) = f

Tactic:
by simp [← comp_coprod f (.inl R M₁ M₂)]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r s✝ : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
U₁ : C
a₁ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₁
U₂ : C
a₂ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₂
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
s : C
α : IsFiltered.max (IsFiltered.max U₁ V) (IsFiltered.max U₂ V) ⟶ s
β : IsFiltered.max (IsFiltered.max U₁ U₂) V ⟶ s
h₁ :
  (rightToMax U₁ V ≫ leftToMax (IsFiltered.max U₁ V) (IsFiltered.max U₂ V)) ≫ α =
    rightToMax (IsFiltered.max U₁ U₂) V ≫ β
h₂ :
  (rightToMax U₂ V ≫ rightToMax (IsFiltered.max U₁ V) (IsFiltered.max U₂ V)) ≫ α =
    rightToMax (IsFiltered.max U₁ U₂) V ≫ β
h₃ :
  (leftToMax U₁ V ≫ leftToMax (IsFiltered.max U₁ V) (IsFiltered.max U₂ V)) ≫ α =
    (leftToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ β
h₄ :
  (leftToMax U₂ V ≫ rightToMax (IsFiltered.max U₁ V) (IsFiltered.max U₂ V)) ≫ α =
    (rightToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ β
⊢ (ConcreteCategory.hom (M.map β))
      ((ConcreteCategory.hom (R.map (leftToMax (IsFiltered.max U₁ U₂) V)))
          ((ConcreteCategory.hom (R.map (leftToMax U₁ U₂))) a₁ + (ConcreteCategory.hom (R.map (rightToMax U₁ U₂))) a₂) •
        (ConcreteCategory.hom (M.map (rightToMax (IsFiltered.max U₁ U₂) V))) b) =
    (ConcreteCategory.hom (M.map α))
      ((ConcreteCategory.hom (M.map (leftToMax (IsFiltered.max U₁ V) (IsFiltered.max U₂ V))))
          ((ConcreteCategory.hom (R.map (leftToMax U₁ V))) a₁ • (ConcreteCategory.hom (M.map (rightToMax U₁ V))) b) +
        (ConcreteCategory.hom (M.map (rightToMax (IsFiltered.max U₁ V) (IsFiltered.max U₂ V))))
          ((ConcreteCategory.hom (R.map (leftToMax U₂ V))) a₂ • (ConcreteCategory.hom (M.map (rightToMax U₂ V))) b))

Tactic:
simp only [add_smul, map_add, ← ConcreteCategory.comp_apply, ← Functor.map_comp, *]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
⊢ Continuous fun ab ↦ (bil ab.1) ab.2

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
⊢ Continuous fun ab ↦ (bil ab.1) ab.2
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ Continuous fun ab ↦ (bil ab.1) ab.2

Tactic:
rw [show (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) =
    ((fun ba ↦ bil.flip ba.1 ba.2 : (B × A → C)) ∘ (Prod.swap : A × B → B × A)) by ext; simp]

Goal state after:
R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ Continuous ((fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.symm
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝¹ y✝ x y : Prequotient F
x✝ : Relation F x y
h : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x

Tactic:
| symm x y _ h =>

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
⊢ ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
ext r; change algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r;
          simp only [Algebra.algebraMap_eq_smul_one, smul_tmul]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e.symm 1 * e 1 = 1

Tactic:
rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ PreservesCofilteredLimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (Over.forget X)

Tactic:
refine ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
  obtain i := Nonempty.some ((inferInstance : Nonempty J))
  let s' : Cone F := ⟨Over.mk (s.π.app i ≫ (F.obj i).hom), fun j ↦ Over.homMk (s.π.app j) (by
    obtain ⟨k, hik, hjk, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    simp only [Functor.const_obj_obj, Over.mk_left, Over.mk_hom,
      ← s.w hjk, ← s.w hik]
    simp), fun j k e ↦ by ext; simpa using (s.w e).symm⟩
  refine ⟨(hc.lift s').left, fun j ↦ congr($(hc.fac s' j).left), fun f hf ↦ ?_⟩
  dsimp at hf
  exact congr($(hc.uniq s' (Over.homMk f (by simp [s', ← hf]))
    fun j ↦ Over.OverMorphism.ext (hf j)).left)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
⊢ Cocone F

Tactic:
exact
      { pt := (c₁.pt, c₂.pt)
        ι.app i := (c₁.ι.app i, c₂.ι.app i)
        ι.naturality {i j} f := by
          ext
          · simpa using c₁.w f
          · simpa using c₂.w f }

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
⊢ ∃ l a, ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
by
  have (i : ι) : ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p := by
    obtain ⟨l, a, b, hl⟩ := h₂ (Sum.elim (fun (_ : PUnit.{w + 1}) ↦ f₁ i)
      (fun (_ : PUnit.{w + 1}) ↦ f₂ i))
        (hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out))
    exact ⟨l, a, (hl (Sum.inl .unit)).trans (hl (Sum.inr .unit)).symm⟩
  choose l p hp using this
  obtain ⟨l, a, b, h⟩ := isCardinalFiltered_iff_aux₁ h₁ h₂ p hι
  exact ⟨l, b, fun i ↦ by grind⟩

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁹ : AddCommGroup M₁
inst✝¹⁸ : Module R M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : Module R M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : Module R M₃
inst✝¹³ : AddCommGroup N₁
inst✝¹² : Module R N₁
inst✝¹¹ : AddCommGroup N₂
inst✝¹⁰ : Module R N₂
inst✝⁹ : AddCommGroup N₃
inst✝⁸ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁷ : AddCommGroup K₂
inst✝⁶ : Module R K₂
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
r : R
x : K₃
⊢ f₂ (r • σ (ι₃ x)) = ι₃ (r • x)

Tactic:
by simp only [map_smul, H₁]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R S : CommRingCat
inst✝⁴ : Algebra ↑R ↑S
A B : Type u
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra (↑R) A
inst✝ : Algebra (↑R) B
f g : A →ₐ[↑R] B
⊢ (f.equalizer g).val.toUnder ≫ f.toUnder = (f.equalizer g).val.toUnder ≫ g.toUnder

Tactic:
ext a; exact a.property

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

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ CreatesLimitsOfShape WalkingCospan (CostructuredArrow.forget P ⊤ L X)

Tactic:
apply +allowSynthFailures forgetCreatesLimitsOfShapeOfClosed
  · exact inferInstanceAs (HasLimitsOfShape WalkingCospan (CostructuredArrow L X))
  · exact CostructuredArrow.closedUnderLimitsOfShape_walkingCospan _ _

Goal state after:
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 : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (Under.mk (f ≫ c.inl)).hom ≫ hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯) = s.pt.hom

Tactic:
by
        simpa using! s.inl.w

Goal state after:
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 B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ (((Functor.const (WidePullbackShape J)).obj c.pt.left).map f ≫
      Option.casesOn Y c.pt.hom fun j ↦ Hom.left (c.π.app { as := j })) =
    (Option.casesOn X c.pt.hom fun j ↦ Hom.left (c.π.app { as := j })) ≫ (widePullbackDiagramOfDiagramOver B F).map f

Tactic:
by
        dsimp; cases X <;> cases Y <;> cases f
        · rw [Category.id_comp, Category.comp_id]
        · rw [Over.w, Category.id_comp]
        · rw [Category.id_comp, Category.comp_id]

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

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
⊢ ExpChar A 1

Tactic:
have := charZero_of_injective_ringHom h

Goal state after:
case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
this : CharZero A
⊢ ExpChar A 1
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : DivisionRing K
inst✝¹ : NonAssocSemiring L
inst✝ : Nontrivial L
f : K →+* L
p : ℕ
⊢ CharP K p ↔ CharP L p

Tactic:
simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, map_zero f]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ x, Ideal.torsionOf R M x = ⊥
n : ℕ
exact : ↑n = ↑n • 1
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
rw [exact, LinearMap.ext_iff, ← hchar.1]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ x, Ideal.torsionOf R M x = ⊥
n : ℕ
exact : ↑n = ↑n • 1
⊢ (∀ (x : M), (↑n • 1) x = 0 x) ↔ ↑n = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ IsUnit ↑↑n

Tactic:
by
  -- `n : R` is a unit iff `(n)` is not a proper ideal in `R`.
  rw [← Ideal.span_singleton_eq_top]
  -- So by contrapositive, we should show the quotient does not have characteristic zero.
  apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))
  intro h_char_zero
  -- In particular, the image of `n` in the quotient should be nonzero.
  apply h_char_zero.cast_injective.ne n.ne_zero
  -- But `n` generates the ideal, so its image is clearly zero.
  rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]
  exact Ideal.subset_span (Set.mem_singleton _)

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

Goal state before:
pp: case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) p
⊢ CharP (R ⧸ I) 0

Tactic:
| intro p hp =>

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s = cons x s.tail

Tactic:
ext1 n
  cases n <;> simp only [get?_cons_zero, get?_cons_succ, get?_tail]
  exact h

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Seq α

Tactic:
refine ⟨Stream'.corec' (Corec.f f) (some b), fun {n} h => ?_⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
h : corec' (Corec.f f) (some b) n = none
⊢ corec' (Corec.f f) (some b) (n + 1) = none
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive (Computation.pure v)

Tactic:
apply pure

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).tail.tail.get (2 * n) = s₁.get n.succ

Tactic:
interleave_eq,

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail.get (2 * n) = s₁.get n.succ
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).tail.tail.get (2 * n + 1) = s₂.get n.succ

Tactic:
interleave_eq,

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail.get (2 * n + 1) = s₂.get n.succ
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 → s = nil

pp: case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Tactic:
· intro h
    ext n
    rw [le_stable _ (Nat.zero_le _) h]
    simp

Goal state after:
case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0