mathlib-initiative/mathlib-tactics huggingface dataset:
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
M : SheafOfModules R
q : M.QuasicoherentData
X Y : C
hY : Y ⟶ X
H : (Sieve.ofObjects q.X X).arrows hY
i : q.I
hi : Y ⟶ q.X i
⊢ q.X i = (fun i ↦ q.X (Exists.choose ⋯)) ⟨q.X i, ⋯⟩

Tactic:
grind

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
i j : ι
⊢ (ConcreteCategory.hom (F.obj.map ((leSupr U i).op ≫ ((U i).infLELeft (U j)).op))) s =
    (ConcreteCategory.hom (F.obj.map ((leSupr U j).op ≫ ((U i).infLERight (U j)).op))) s

Tactic:
rfl

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
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
i : ι
⊢ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = sf i

Tactic:
rfl

Goal state after:
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
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x : C
⊢ unit (R.over x) ≅ (pushforward (𝟙 (R.over x))).obj (unit R)

Tactic:
rfl

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 u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
V : (Opens ↑Y)ᵒᵖ
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ unop V
⊢ (Opens.map f).obj (unop V) ≤ (Opens.map f).obj (unop V)

Tactic:
rfl

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
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
x✝ : ι
⊢ (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t =
    (ConcreteCategory.hom (G.obj.map ((homOfLE ⋯).op ≫ (leSupr U x✝).op))) t

Tactic:
rfl

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

Goal state before:
pp: case hcover
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
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
⊢ U ≤ iSup V

Tactic:
intro x hxU

Goal state after:
case hcover
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
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↑X
hxU : x ∈ U
⊢ x ∈ iSup V
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
⊢ U ≤ iSup V

Tactic:
intro x hxU

Goal state after:
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
x : ↑X
hxU : x ∈ U
⊢ x ∈ iSup V
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
S : Submodule R M
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalAddGroup M
inst✝ : ContinuousSMul R M
⊢ Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S] fun p ↦ p.1 • p.2

Tactic:
rw [← (IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ).continuous_comp_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
S : Submodule R M
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalAddGroup M
inst✝ : ContinuousSMul R M
⊢ Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S]
    ((fun p ↦ p.1 • p.2) ∘ Prod.map id ⇑S.mkQ)
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
z : ↑X
hz : z ∈ V x ⊓ V y
⊢ (ConcreteCategory.hom (G.obj.map ((iVU x).op ≫ ((V x).infLELeft (V y)).op) ≫ germ G.obj (V x ⊓ V y) z hz)) t =
    (ConcreteCategory.hom (G.obj.map ((iVU y).op ≫ ((V x).infLERight (V y)).op) ≫ germ G.obj (V x ⊓ V y) z hz)) t

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f g : M × M₂ →L[R] M₃
⊢ ↑f ∘ₗ LinearMap.inl R M M₂ = ↑g ∘ₗ LinearMap.inl R M M₂ ∧ ↑f ∘ₗ LinearMap.inr R M M₂ = ↑g ∘ₗ LinearMap.inr R M M₂ ↔
    ↑(f ∘SL inl R M M₂) = ↑(g ∘SL inl R M M₂) ∧ ↑(f ∘SL inr R M M₂) = ↑(g ∘SL inr R M M₂)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
r : R
m : A
⊢ φ ((algebraMap R A) r) * φ m = r • φ m

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
s : KernelFork φ
m : s.pt ⟶ (KernelFork.ofι (kerι φ) ⋯).pt
h : m ≫ kerι φ = Fork.ι s
⊢ Fork.ι s = ofHom ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ)).ker ⋯) ≫ kerι φ

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
s : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : cokerπ φ ≫ m = Cofork.π s
⊢ Cofork.π s = cokerπ φ ≫ ofHom { toLinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯, cont := ⋯ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: 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₂
⊢ S.HasHomology

Tactic:
suffices IsIso F from ⟨⟨.ofIsIsoLeftRightHomologyComparison' D₁ D₂⟩⟩

Goal state after:
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₂
⊢ IsIso F
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case one
α : Type u
inst✝ : Mul α
⊢ (mapMulHom (MulHom.id α)) 1 = (MonoidHom.id (WithOne α)) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case coe
α : Type u
inst✝ : Mul α
a✝ : α
⊢ (mapMulHom (MulHom.id α)) ↑a✝ = (MonoidHom.id (WithOne α)) ↑a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case one
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
⊢ (mapMulHom g) ((mapMulHom f) 1) = (mapMulHom (g.comp f)) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case coe
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
a✝ : α
⊢ (mapMulHom g) ((mapMulHom f) ↑a✝) = (mapMulHom (g.comp f)) ↑a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (F.map f ≫ coconeMorphism F j')) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : MonCat
x✝² : X'✝ ⟶ X✝
x✝¹ : X✝ ⟶ (forget MonCat).obj Y✝
x✝ : X'✝
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.homEquiv.trans (FreeMonoid.lift.symm.trans TypeCat.homEquiv.symm)).symm (x✝² ≫ x✝¹)))
      (FreeMonoid.of x✝) =
    (ConcreteCategory.hom
        (free.map x✝² ≫ (ConcreteCategory.homEquiv.trans (FreeMonoid.lift.symm.trans TypeCat.homEquiv.symm)).symm x✝¹))
      (FreeMonoid.of x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.of
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
x✝ : ↑(F.obj j)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (Prequotient.of j x✝)) =
    (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ m)) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.one
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ 1 = (Hom.hom (descMorphism F s)) 1

Tactic:
rfl

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝¹ : Continuous[inst✝⁵, inst✝³] (↑e).toFun
continuous_invFun✝¹ : Continuous[inst✝³, inst✝⁵] e.invFun
continuous_toFun✝ :
  Continuous[inst✝⁵, inst✝³]
    (↑↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).toFun
continuous_invFun✝ :
  Continuous[inst✝³, inst✝⁵]
    (↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).invFun
⊢ { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    {
      toLinearEquiv :=
        ↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ },
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }

Tactic:
rfl

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁶ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁵ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹² : RingHomInvPair σ₁₃ σ₃₁
inst✝¹¹ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
x✝ : M₁
⊢ ↑(e₁.trans e₂) x✝ = ((↑e₁).trans ↑e₂) x✝

Tactic:
rfl

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
x y : (M →L[R] M)ˣ
x✝ : M
⊢ (ofUnit (x * y)) x✝ = (ofUnit x * ofUnit y) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
this : f = ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg)
⊢ ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg).symm = g

Tactic:
rfl

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

Goal state before:
pp: case pos
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₃
A : M ≃L[R] M₂
⊢ (A.trans e).symm = e.symm.trans A.symm

Tactic:
rfl

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

Goal state before:
pp: case pos
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
A : M ≃L[R] M₂
⊢ (e.trans A).symm = A.symm.trans e.symm

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case refine_1
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
x✝ : T ⊗[R] R
⊢ (TensorProduct.rid R R T) x✝ ⊗ₜ[R] 1 = (TensorProduct.AlgebraTensorModule.rid R R T) x✝ ⊗ₜ[R] 1

Tactic:
rfl

Goal state after:
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
e : M ≃L[R] M
⊢ ↑((ContinuousLinearEquiv.unitsEquiv R M).symm e)⁻¹ = ↑e.symm

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M₂
inst✝ : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
p : Submodule R M
x : ↥p
⊢ ↑((e.submoduleMap p) x) = e ↑x

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M₂
inst✝ : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
p : Submodule R M
x : ↥(Submodule.map (↑↑e) p)
⊢ ↑((e.submoduleMap p).symm x) = e.symm ↑x

Tactic:
rfl

Goal state after: