mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ i = f.s₀ i

Tactic:
by simp [hs₀]

Goal state after:
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
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ j = f.s₀ j

Tactic:
by simp [hs₀]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y.left
Z : Over X
f : Z ⟶ Y
⊢ ((overEquiv Y).symm S).arrows f ↔ S.arrows (Over.Hom.left f)

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)

Tactic:
have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
          (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩
      simp only [op_id, F.map_id, types_id_apply] at h
      exact h.trans (hx.familyOfElements_apply _ _ _)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
⊢ S ∈ (J.over X) Y ↔ (Sieve.overEquiv Y) S ∈ J Y.left

Tactic:
by
  rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
⊢ Over.Hom.left f₂ ≫ Y₂.hom = W'.hom

Tactic:
simpa using! (Over.forget _).congr_map h.symm =≫ Z.hom

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
⊢ ∀ (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
p₂

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
⊢ p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
⊢ ∀ (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
p₂

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
⊢ p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
    (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: 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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
⊢ IsIso (pullbackObjUnitToUnit φ)

Tactic:
isIso_iff_coyoneda_map_bijective

Goal state after:
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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
⊢ ∀ (T : SheafOfModules R), Function.Bijective fun x ↦ pullbackObjUnitToUnit φ ≫ x
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
⊢ map (𝟙 X) = 𝟭 (Opens ↑X)

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ ⋯.functor.obj ⊤ = U

Tactic:
ext1
  exact Set.image_univ.trans Subtype.range_coe

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ (map U.inclusion' ⋙ ⋯.functor).obj (⋯.functor.obj V) = (𝟭 (Opens ↑X)).obj (⋯.functor.obj V)

Tactic:
dsimp; rw [map_functor_eq V]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
⊢ PreservesLimitsOfShape (Discrete ι) hf.functor

Tactic:
by
  apply +allowSynthFailures preservesLimitsOfShape_of_discrete
  intro g
  refine preservesLimit_of_preserves_limit_cone (Preorder.isLimitIInf g) ?_
  refine (Limits.Fan.isLimitMapConeEquiv _ _ _).symm (Preorder.isLimitOfIsGLB _ _ ?_)
  simp only [Discrete.range_functor, homOfLE_leOfHom, Fan.mk_pt, hf.functor_obj_iInf]
  apply isGLB_iInf

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
R : Sieve X
hR : ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ x ∈ Y, ∃ U f, S.arrows f ∧ x ∈ U}
x : T
hx : x ∈ X
⊢ ∃ U f, R.arrows f ∧ x ∈ U

Tactic:
rcases hS x hx with ⟨U, f, hf, hU⟩
    rcases hR hf _ hU with ⟨V, g, hg, hV⟩
    exact ⟨_, g ≫ f, hg, hV⟩

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝² : Category.{v, u} C
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
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : ToType (F.obj (op V))
⊢ (ConcreteCategory.hom (e.app (op V) ≫ G.map (homOfLE h).op)) x =
    (ConcreteCategory.hom (G.map (homOfLE h).op)) ((ConcreteCategory.hom (e.app (op V))) x)

Tactic:
ConcreteCategory.comp_apply

Goal state after:
X : TopCat
C : Type u
inst✝² : Category.{v, u} C
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
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : ToType (F.obj (op V))
⊢ (ConcreteCategory.hom (G.map (homOfLE h).op)) ((ConcreteCategory.hom (e.app (op V))) x) =
    (ConcreteCategory.hom (G.map (homOfLE h).op)) ((ConcreteCategory.hom (e.app (op V))) x)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections

Tactic:
isSheafOpensLeCover_iff_isSheafPairwiseIntersections

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafPairwiseIntersections ↔ F.IsSheafPairwiseIntersections
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 (F.germ U x hx ≫ (stalkFunctor C x).map f)) s

Tactic:
ConcreteCategory.comp_apply

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 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)
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)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map iWU₁.op)) s) =
    (ConcreteCategory.hom (F.map iWU₂.op ≫ f.app (op W))) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t

Tactic:
ConcreteCategory.comp_apply

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)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map iWU₁.op)) s) =
    (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map iWU₂.op)) t)
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
inst✝³ : ContinuousAdd M
inst✝² : Module R M
inst✝¹ : ContinuousSMul R M
inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
this : Tendsto (fun c ↦ y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + ↑u • x ∈ s
⊢ x ∈ s

Tactic:
have hy' : y ∈ ↑s := mem_of_mem_nhds hy

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
inst✝³ : ContinuousAdd M
inst✝² : Module R M
inst✝¹ : ContinuousSMul R M
inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
this : Tendsto (fun c ↦ y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + ↑u • x ∈ s
hy' : y ∈ s
⊢ x ∈ s
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 ↦
                Opposite.casesOn X_1 fun unop ↦
                  Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 ↦
                    ULift.casesOn a fun down ↦
                      WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
              naturality := ⋯ } } ≫
      F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    s.fst

Tactic:
exact
    (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
      op <| Pairwise.single <| ULift.up WalkingPair.left

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
⊢ instTopologicalSpaceProd = moduleTopology R (M × N)

Tactic:
have : ContinuousAdd M := toContinuousAdd R M

Goal state after:
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this : ContinuousAdd M
⊢ instTopologicalSpaceProd = moduleTopology R (M × N)
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:
by
  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:
by
  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 σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
⊢ ↑(f.ofSubmodule' U) = (↑f ∘SL (Submodule.comap (↑↑f) U).subtypeL).codRestrict U ⋯

Tactic:
by
  rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
X : C
inst✝ : IsFinitelyPresentable X
⊢ PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (coyoneda.obj (op X))

Tactic:
rw [← isFinitelyPresentable_iff_preservesFilteredColimitsOfSize]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
X : C
inst✝ : IsFinitelyPresentable X
⊢ IsFinitelyPresentable X
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

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

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
  obtain ⟨l, a, b, h⟩ := IsCardinalFiltered.wideSpan
    (fun i ↦ IsFiltered.coeqHom (f₁ i) (f₂ i)) hι
  exact ⟨l, b, fun i ↦ by rw [← h i, IsFiltered.coeq_condition_assoc]⟩

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 ⊗[R] ((i : ι) → M i)
⊢ (piRight R S N M) x = (piRightHom R S N M) x

Tactic:
by
  rfl

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N ⊗[R] (ι → R)
⊢ (piScalarRight R S N ι) x = (piScalarRightHom R S N ι) x

Tactic:
by
  rfl

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

Goal state before:
pp: case refine_3
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑P
⊢ (ConcreteCategory.hom (π ≫ g)) x =
    (ConcreteCategory.hom
        (g' ≫ F.map (c'.ι.app none) ≫ c.ι.app (((Functor.const (WidePushoutShape ↥s)).obj c'.pt).obj none)))
      x

Tactic:
c.w,

Goal state after:
case refine_3
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑P
⊢ (ConcreteCategory.hom (π ≫ g)) x = (ConcreteCategory.hom (g' ≫ c.ι.app i)) x
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S)

Tactic:
CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
this : (a :: const a).tail = const a
⊢ (const a).tail = const a

Tactic:
rwa [← const_eq] at this

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

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
s : Seq α
M : a ∈ s
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
⊢ C s

Tactic:
obtain ⟨k, e⟩ := M; unfold Stream'.get at e
  induction k generalizing s with
  | zero =>
    have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
    rw [TH]
    apply h1 _ _ (Or.inl rfl)
  | succ k IH =>
    cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
s : Seq α
⊢ take (n + 1) (cons x s) = x :: take n s

Tactic:
by
  rfl

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

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (pure a).bind f = f a

Tactic:
apply
    eq_of_bisim fun c₁ c₂ => c₁ = bind (pure a) f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
  · intro c₁ c₂ h
    match c₁, c₂, h with
    | _, _, Or.inl ⟨rfl, rfl⟩ =>
      simp only [BisimO, bind, Bind.f, corec_eq, rmap, destruct_pure]
      rcases destruct (f a) with b | cb <;> simp [Bind.g]
    | _, c, Or.inr rfl =>
      simp only [BisimO, Bind.f, corec_eq, rmap]
      rcases destruct c with b | cb <;> simp [Bind.g]
  · simp

Goal state after: