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

Goal state before:
pp: case refine_1.of
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S : Sieve X✝
X : C
R : Presieve X
hR : R ∈ J.coverings X
⊢ ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows

Tactic:
use R, hR
      exact Sieve.le_generate R

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

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ Function.Bijective ⇑(ConcreteCategory.hom (P.map (pullbackComparison F (f i) (f j)).op))

Tactic:
← isIso_iff_bijective

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ IsIso (P.map (pullbackComparison F (f i) (f j)).op)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K.toGrothendieck ≤ J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Sieve.generate R ∈ J X

Tactic:
exact h _ (generate_mem_toGrothendieck hR)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
| (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁)

Tactic:
rw [eq₁]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
| (ConcreteCategory.hom (ℱ.obj.map ((c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯).op))
    (x g₁ hg₁)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
⊢ ∀ ⦃I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve f, ⋯⟩⦄ (r : I₁.Relation I₂),
    (match I₁ with
        | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op) ≫
        F.obj.map r.g₁.op =
      (match I₂ with
        | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op) ≫
        F.obj.map r.g₂.op

Tactic:
rintro ⟨W₀, a, ha⟩ ⟨W₀', a', ha'⟩ ⟨T₀, p₁, p₂, fac⟩
      rw [← Functor.map_comp, ← Functor.map_comp, ← op_comp, ← op_comp]
      apply map_eq_of_eq K G
      rw [Functor.map_comp, Functor.map_comp, ha.choose_spec, ha'.choose_spec,
        ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, fac]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
⊢ imageSieve f a ∈ K X

Tactic:
apply K.transitive (H.is_cover_of_isCoverDense K X)
    intro Y g ⟨⟨Z, lift, m, fac⟩⟩
    rw [← fac, Sieve.pullback_comp]
    apply K.pullback_stable
    have hh := hH.cover_preserve <| imageSieve_mem J (whiskerLeft H.op f) (G.map m.op a)
    refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_
    refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_) hh
    intro W q ⟨x, h⟩
    simp only [Sieve.functorPullback_apply, Presieve.functorPullback_mem, Sieve.pullback_apply]
    exact ⟨x, by simpa using! h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.h₁ (e.hom.s₁ k) ≫
      eqToHom ⋯ ≫ e.hom.h₁ ((congrIndexOneOfEq ⋯ ⋯) k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)).hom =
    𝟙 (F.Y (e.hom.s₁ k))

Tactic:
rw [← eqToHom_naturality_assoc _ (by simp)]

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.h₁ (e.hom.s₁ k) ≫
      e.hom.h₁ (e.inv.s₁ (e.hom.s₁ k)) ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)).hom =
    𝟙 (F.Y (e.hom.s₁ k))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
i₀ : E.I₀
⊢ m ≫ F.obj.map (E.f i₀).op = c.ι i₀

Tactic:
exact hm i₀

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ HasBinaryCoproducts α

Tactic:
have : ∀ x y : α, HasColimit (pair x y) := by
    let := hasFiniteColimits_of_hasFiniteColimits_of_size.{u} α
    infer_instance
  apply hasBinaryCoproducts_of_hasColimit_pair

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ IsSeparable {f | ∀ (i : Fin n), (f i).2 ∈ s}

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ Continuous[Pi.topologicalSpace, inst✝⁴] fun f ↦ ∑ i, (f i).1 • (f i).2

Tactic:
· have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by
      apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)
    rwa [Set.univ_prod] at this

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ Continuous[Pi.topologicalSpace, inst✝⁴] fun f ↦ ∑ i, (f i).1 • (f i).2
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ IsClosed[inst✝⁴] ↑s ∨ Dense ↑s

Tactic:
refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ s.topologicalClosure = s → IsClosed[inst✝⁴] ↑s
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: case hl
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
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
x✝ : M₁
⊢ ((r • a.1).coprod (r • a.2) ∘SL inl R M₁ M₂) x✝ = ((r • a.1.coprod a.2) ∘SL inl R M₁ M₂) x✝

Tactic:
simp [smul_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: case hr
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
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
x✝ : M₂
⊢ ((r • a.1).coprod (r • a.2) ∘SL inr R M₁ M₂) x✝ = ((r • a.1.coprod a.2) ∘SL inr R M₁ M₂) x✝

Tactic:
simp [smul_apply]

Goal state after:
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 A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective ⇑f
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : (Fin m → R) × B →ₗ[R] A × B := f.prodMap LinearMap.id
hφ : Function.Surjective ⇑φ
⊢ Continuous fun ab ↦ (bil ab.1) ab.2

Tactic:
rw [Topology.IsQuotientMap.continuous_iff (isQuotientMap_of_surjective hφ)]

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 A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective ⇑f
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : (Fin m → R) × B →ₗ[R] A × B := f.prodMap LinearMap.id
hφ : Function.Surjective ⇑φ
⊢ Continuous ((fun ab ↦ (bil ab.1) ab.2) ∘ ⇑φ)
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 y : ↑S.X₂.toModuleCat
hy : (ConcreteCategory.hom S.g) y = 0
e : (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x
z : ↑S.X₁.toModuleCat
hz : ↑(Hom.hom S.f) z = y - x
⊢ (ConcreteCategory.hom S.g) x = 0

Tactic:
obtain rfl := eq_sub_iff_add_eq.mp hz

Goal state after:
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
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ (↑e ∘SL f).inverse = f.inverse ∘SL ↑e.symm

Tactic:
inverse_of_not_isInvertible (by simp [hf]),

Goal state after:
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ 0 = f.inverse ∘SL ↑e.symm
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ (f ∘SL ↑e).inverse = ↑e.symm ∘SL f.inverse

Tactic:
inverse_of_not_isInvertible (by simp [hf]),

Goal state after:
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ 0 = ↑e.symm ∘SL f.inverse
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i), ι := { app := fun j ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
f : ((Under.forget X).mapCocone c).pt ⟶ s.pt
hf : ∀ (j : J), Under.Hom.right (c.ι.app j) ≫ f = s.ι.app j
⊢ f = Under.Hom.right (hc.desc s')

Tactic:
exact congr($(hc.uniq s' (Under.homMk f (by simp [s', ← hf]))
    fun j ↦ Under.UnderMorphism.ext (hf j)).right)

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
⊢ ∃ j u, f₁ ≫ F.map u = f₂ ≫ F.map u

Tactic:
by
  have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
  have := isFiltered_of_isCardinalFiltered J κ
  exact exists_eq_of_preservesColimit_coyoneda_self hc f₁ f₂ hf

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
j : ι
⊢ Pi.single i (x ⊗ₜ[R] m) j = x ⊗ₜ[R] Pi.single i m j

Tactic:
← tmul_single

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
j : ι
⊢ x ⊗ₜ[R] Pi.single i m j = x ⊗ₜ[R] Pi.single i m j
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
N : Type u_4
inst✝³ : Semiring N
inst✝² : Algebra R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : ι → R
⊢ (piScalarRight R S N ι).symm ((algebraMap (ι → R) (ι → N)) x) = 1 ⊗ₜ[R] x

Tactic:
by
  simp [Algebra.algebraMap_eq_smul_one, Pi.smul_def', LinearEquiv.symm_apply_eq,
    piScalarRight_apply, piScalarRightHom_tmul]

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₃
⊢ π₁ (ρ (i₂ (σ (ι₃ (r • x))))) = π₁ (r • ρ (i₂ (σ (ι₃ x))))

Tactic:
apply eq_of_eq i₁ i₂ f₁ f₂ hf g₁ h₁ ρ hρ ι₃ π₁ hπ₁ (r • x) _ (H₁ _) _ (H₂ _)
        (r • σ (ι₃ x)) (by simp only [map_smul, H₁]) _ (by simp only [map_smul, H₂])

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ Function.Injective ⇑(lTensor A g)

Tactic:
by
/-
The proof is taking a resolution `0 → K → Q → A → 0` with `Q` flat,
and applying snake lemma on the following diagram to
```
                      0
                      ↓
    K ⊗ M → K ⊗ N → K ⊗ P → 0
      ↓       ↓       ↓
0 → Q ⊗ M → Q ⊗ N → Q ⊗ P
      ↓       ↓
    A ⊗ M → A ⊗ N
      ↓       ↓
      0       0
```
to get `0 → A ⊗ K → A ⊗ M` exact.
-/
  let Q := A →₀ R
  let π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
  have hπ : Function.Surjective π := Finsupp.linearCombination_surjective _ Function.surjective_id
  let K := LinearMap.ker π
  have := SnakeLemma.exact_δ'_left (K.subtype.rTensor M) (K.subtype.rTensor N) (K.subtype.rTensor P)
    (g.lTensor K) (f.lTensor K) (lTensor_exact K H hf) (g.lTensor Q) (f.lTensor Q)
    (lTensor_exact Q H hf) (by simp) (by simp) (K₃ := Unit) 0
    (by simpa using Module.Flat.rTensor_preserves_injective_linearMap _ K.subtype_injective)
    (π.rTensor M) (rTensor_exact _ (exact_subtype_ker_map π) hπ) (π.rTensor N)
    (rTensor_exact _ (exact_subtype_ker_map π) hπ) (lTensor_surjective K hf)
    (Module.Flat.lTensor_preserves_injective_linearMap _ hg) (g.lTensor A)
    (by simp) (rTensor_surjective _ hπ)
  rw [Subsingleton.elim (SnakeLemma.δ' ..) 0] at this
  simpa using this

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

Goal state before:
pp: ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
j : ι
⊢ (Pi.evalRingHom (fun x ↦ R) j) ↑x = 0

Tactic:
rw [map_natCast, h]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
S : Subsemiring R
x : ℕ
h : ↑x = 0
⊢ S.subtype ↑x = 0

Tactic:
rw [map_natCast, h]

Goal state after: