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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    f
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
hab : a ≫ b = f
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f

Tactic:
subst hab
    refine ⟨(k, l), pullback.lift (a ≫ e) u ?_, ?_, ?_⟩
    · simp only [Category.assoc] at u₁
      simp [← reassoc_of% h₁, w, ← reassoc_of% u₁, ← pullback.condition]
    · apply pullback.hom_ext
      · simp [h₁]
      · simpa using u₁
    · apply pullback.hom_ext
      · simp [h₂]
      · simpa using u₂

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e✝ : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : G.IsEquivalence
U : C
e : C ≌ D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
⊢ (Sieve.coverByImage G U).arrows f ↔ ⊤.arrows f

Tactic:
simp only [Sieve.top_apply, iff_true]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e✝ : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : G.IsEquivalence
U : C
e : C ≌ D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
⊢ (Sieve.coverByImage G U).arrows f
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : G.IsEquivalence
U : C
⊢ Sieve.coverByImage G U ∈ J U

Tactic:
by
    let e := (asEquivalence G).symm
    convert! J.top_mem U
    ext Y f
    simp only [Sieve.top_apply, iff_true]
    let g : e.inverse.obj _ ⟶ U := (e.unitInv.app Y) ≫ f
    have : (Sieve.coverByImage e.inverse U).arrows g := Presieve.in_coverByImage _ g
    replace := Sieve.downward_closed _ this (e.unit.app Y)
    simpa [g] using! this

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
⊢ K = e.inverse.inducedTopology J

Tactic:
ext
  rw [mem_inducedTopology_iff_of_isCoverDense]
  exact (e.inverse.functorPushforward_mem_iff K J).symm

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
⊢ (generate (Presieve.functorPullback (Over.forget X) R)).arrows g

Tactic:
refine ⟨.mk (q ≫ Y.hom), Over.homMk p (by simp [reassoc_of% hpq]), Over.homMk q rfl, hq, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
⊢ Over.homMk p ⋯ ≫ Over.homMk q ⋯ = g
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f ↔ ⊤.arrows f

Tactic:
simp only [Sieve.top_apply, iff_true]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1.of
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve Y
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ (Sieve.overEquiv { left := Z, right := right, hom := s }).symm (Sieve.generate S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }

Tactic:
| of Z S hS =>

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X

Tactic:
Precoverage.toGrothendieck_le_iff_le_toPrecoverage

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ (map U.inclusion').obj U = ⊤

Tactic:
ext1
  exact Subtype.coe_preimage_self _

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

Goal state before:
pp: case e'_2
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map (𝟙 (op V)))) s

Tactic:
F.1.map_id,

Goal state after:
case e'_2
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (𝟙 (F.obj.obj (op V)))) s
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
⊢ stalkPushforward C (𝟙 X) ℱ x = (stalkFunctor C x).map (Pushforward.id ℱ).hom

Tactic:
by
  ext
  simp only [stalkPushforward, germ, colim_map, ι_colimMap_assoc, whiskerRight_app]
  erw [CategoryTheory.Functor.map_id]
  simp [stalkFunctor]

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

Goal state before:
pp: case e'_3
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ t = (ConcreteCategory.hom (F.obj.map (𝟙 (op V)))) t

Tactic:
F.1.map_id,

Goal state after:
case e'_3
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ t = (ConcreteCategory.hom (𝟙 (F.obj.obj (op V)))) t
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 : Set M
⊢ closure[inst✝⁴] s ⊆ ↑(span R s).topologicalClosure

Tactic:
Submodule.topologicalClosure_coe

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 : Set M
⊢ closure[inst✝⁴] s ⊆ closure[inst✝⁴] ↑(span R s)
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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α✝ : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
s : C
α : IsFiltered.max i i ⟶ s
H : leftToMax i i ≫ α = rightToMax i i ≫ α
⊢ (ConcreteCategory.hom ((AddCommGrpCat.FilteredColimits.colimitCocone M).ι.app i)) (r • m) =
    (ConcreteCategory.hom ((RingCat.FilteredColimits.colimitCocone R).ι.app i)) r •
      (ConcreteCategory.hom ((AddCommGrpCat.FilteredColimits.colimitCocone M).ι.app i)) m

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (leftToMax _ _ ≫ α) α ?_

Goal state after:
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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α✝ : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
s : C
α : IsFiltered.max i i ⟶ s
H : leftToMax i i ≫ α = rightToMax i i ≫ α
⊢ (ConcreteCategory.hom
        ((((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).map
          (leftToMax i i ≫ α)))
      (r • m) =
    (ConcreteCategory.hom
        ((((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).map α))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨i, r⟩.fst ⟨i, m⟩.fst))) ⟨i, r⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨i, r⟩.fst ⟨i, m⟩.fst))) ⟨i, m⟩.snd)
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
⊢ Continuous fun ab ↦ (bil ab.1) ab.2

Tactic:
let φ := f.prodMap (LinearMap.id : B →ₗ[R] B)

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
⊢ Continuous fun ab ↦ (bil ab.1) ab.2
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
⊢ ∃ x, f x ≠ 0

Tactic:
by_contra! h

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
h : ∀ (x : M₁), f x = 0
⊢ False
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Ring R
R₂ : Type u_2
inst✝⁶ : Ring R₂
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ f (-x) = -f x

Tactic:
by
  exact map_neg f x

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 1 • e.symm 1 = 1

Tactic:
← map_smul,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e.symm (e 1 • 1) = 1
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:
← map_smul,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e (e.symm 1 • 1) = 1
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app i))

Tactic:
exact (s.ι.app i).hom.2

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

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
wlog hs' : s.Finite generalizing s

Goal state after:
case inr
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
this :
  ∀ (s : Set ↑S),
    Ideal.span s = ⊤ → (∀ f ∈ s, Q (of (Localization.Away f))) → s.Finite → (ObjectProperty.ofObj f).isoClosure S
hs' : ¬s.Finite
⊢ (ObjectProperty.ofObj f).isoClosure S

P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
hs' : s.Finite
⊢ (ObjectProperty.ofObj f).isoClosure S
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
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
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₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ i₂ (σ (ι₃ x)) - i₂ (f₁ y) = 0

Tactic:
← H₂,

Goal state after:
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
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
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₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ g₁ (ρ (i₂ (σ (ι₃ x)))) - i₂ (f₁ y) = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePushouts C
⊢ HasFiniteColimits (Under B)

Tactic:
rw [← hasFiniteLimits_opposite_iff]
  exact hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.opEquivOpUnder _).inverse

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
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ ∀ (j : WidePullbackShape J),
    ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app j =
      { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
            inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app j

Tactic:
rintro (j | j)

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app none =
    { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
          inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
j : J
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app (some j) =
    { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
          inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app (some j)
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
p f : ℕ
hp : Fact (Nat.Prime p)
hR : Fintype.card R = p ^ f
h0 : f = 0
⊢ Fintype.card R ≤ 1

Tactic:
by simpa [h0] using hR.le

Goal state after: