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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) ≤ E.sieve₁ (f ≫ p₁) (f ≫ p₂)

Tactic:
intro Z g ⟨k, u, hu₁, hu₂⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
g : Z ⟶ T
k : E.I₁ i₁ i₂
u : Z ⟶ E.Y k
hu₁ : (g ≫ f) ≫ p₁ = u ≫ E.p₁ k
hu₂ : (g ≫ f) ≫ p₂ = u ≫ E.p₂ k
⊢ (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) ≤ E.sieve₁ (f ≫ p₁) (f ≫ p₂)

Tactic:
intro Z g ⟨k, u, hu₁, hu₂⟩
    cat_disch

Goal state after:
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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ E.sieve₁ (f ≫ p₁) (f ≫ p₂) ≤ Sieve.pullback f (E.sieve₁ p₁ p₂)

Tactic:
intro Z g ⟨k, u, hu₁, hu₂⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
g : Z ⟶ T
k : E.I₁ i₁ i₂
u : Z ⟶ E.Y k
hu₁ : g ≫ f ≫ p₁ = u ≫ E.p₁ k
hu₂ : g ≫ f ≫ p₂ = u ≫ E.p₂ k
⊢ (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g
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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ E.sieve₁ (f ≫ p₁) (f ≫ p₂) ≤ Sieve.pullback f (E.sieve₁ p₁ p₂)

Tactic:
intro Z g ⟨k, u, hu₁, hu₂⟩
    cat_disch

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
U V : C
f : G.obj U ⟶ G.obj V
Y₁ Y₂ : C
i₁ : Y₁ ⟶ U
l : Y₁ ⟶ V
hl : G.map l = G.map i₁ ≫ f
i₂ : Y₂ ⟶ Y₁
⊢ ∃ l, G.map l = G.map (i₂ ≫ i₁) ≫ f

Tactic:
exact ⟨i₂ ≫ l, by simp [hl]⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
⊢ f = g ↔
    ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯) (hs₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)),
      ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = g.h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv ≫ eqToHom ⋯

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hs₀, hh₀, hs₁, hh₁⟩ ↦ Hom.ext' hs₀ hh₀ hs₁ hh₁⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
h : f = g
⊢ ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯) (hs₁ :
    ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)),
    ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = g.h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈
    K (G.obj U₁)

Tactic:
clear iZU₁ Z

Goal state after:
case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈
    K (G.obj U₁)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ e.hom.s₁ (e.inv.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.inv_hom_id
  simpa using! hs₁ i j k

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
⊢ ∀ (F : WidePullbackShape J → α),
    (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePullbackShape J), F j = F j'

Tactic:
F

Goal state after:
J α : Type u_1
F : WidePullbackShape J → α
⊢ (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePullbackShape J), F j = F j'
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
⊢ ∀ (F : WidePushoutShape J → α),
    (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePushoutShape J), F j = F j'

Tactic:
F

Goal state after:
J α : Type u_1
F : WidePushoutShape J → α
⊢ (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePushoutShape J), F j = F j'
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.obj
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
Z : Cᵒᵖ
W : C
a : W ⟶ Opposite.unop Z
i : I
b : W ⟶ Y i
⊢ (f ≫ c.π.app Z) ≫ F.obj.map { Y := W, f := a, hf := ⋯ }.f.op =
    (g ≫ c.π.app Z) ≫ F.obj.map { Y := W, f := a, hf := ⋯ }.f.op

Tactic:
simpa using h i =≫ F.1.map b.op

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.obj
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
⊢ f = g

Tactic:
by
  refine hc.hom_ext (fun Z => F.2.hom_ext (hY.cover Z.unop) _ _ ?_)
  rintro ⟨W, a, ⟨i, ⟨b⟩⟩⟩
  simpa using h i =≫ F.1.map b.op

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

Goal state before:
pp: case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
i : ι
hi : x ∈ U i
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1

Tactic:
exact ⟨U i, ⟨homOfLE le_top, ⟨i, ⟨𝟙 _⟩⟩⟩, hi⟩

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

Goal state before:
pp: case refine_2
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ ∀ ⦃Y : Opens ↑X⦄ ⦃f : Y ⟶ unop U⦄,
    Presieve.ofArrows V (fun x ↦ homOfLE ⋯) f →
      (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) s = (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) t

Tactic:
rintro _ _ ⟨x⟩; exact H x

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
V : Opens ↑Y
i : V ⟶ U
hi : S.arrows i
hxV : (ConcreteCategory.hom f) x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
exact ⟨_, (Opens.map f).map i, ⟨_, _, 𝟙 _, hi, Subsingleton.elim _ _⟩, hxV⟩

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
inst✝¹³ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
⊢ ((pushforward φ).obj M).IsQuasicoherent

Tactic:
apply +allowSynthFailures isQuasicoherent_pushforward G φ η _
  intro X Y f
  let G' := Over.post (X := X) G ⋙ Over.map f
  have : G'.IsContinuous (K.over X) (J.over Y) := Functor.isContinuous_comp _ _ _ (J.over _) _
  have : G'.IsCocontinuous (K.over X) (J.over Y) := isCocontinuous_comp _ _ _ (J.over _)
  let a : S.over X ⟶
      (G'.sheafPushforwardContinuous RingCat.{u} (K.over X) (J.over Y)).obj (R.over Y) :=
    ((Over.forget X).sheafPushforwardContinuous RingCat.{u} (K.over X) K).map φ
  have : (pushforward.{u} a).IsLeftAdjoint := isLeftAdjoint_pushforward_of_isIso a
  infer_instance

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 Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
⊢ stalkPullbackHom C f F x ≫ stalkPullbackInv C f F x = 𝟙 (F.stalk ((ConcreteCategory.hom f) x))

Tactic:
ext U hU
    dsimp
    rw [germ_stalkPullbackHom_assoc, germ_stalkPullbackInv, Category.comp_id,
      pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk]

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
by apply DFunLike.ext; simp [succ_nsmul]

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = -↑(n + 1)

Tactic:
by apply DFunLike.ext; simp [succ_nsmul]

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ✝ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ✝ σ'
inst✝⁵ : RingHomInvPair σ' σ✝
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ✝
hσ' : Continuous ⇑σ'
e : A ≃SL[σ✝] B'
g : A →ₛₗ[σ✝] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
σ : TopologicalSpace A
hσ1 : ContinuousSMul R A
hσ2 : ContinuousAdd A
⊢ TopologicalSpace.induced (⇑e.toHomeomorph.symm) σ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'}

Tactic:
exact ⟨continuousSMul_inducedₛₗ g' hσ', continuousAdd_induced h'⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
⊢ Function.Exact ⇑(ConcreteCategory.hom (S.map (uliftFunctor.{u_1, v, u} R)).f)
    ⇑(ConcreteCategory.hom (S.map (uliftFunctor.{u_1, v, u} R)).g)

Tactic:
dsimp [uliftFunctor]

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
⊢ Function.Exact (⇑ULift.moduleEquiv.symm ∘ ⇑(Hom.hom S.f) ∘ ⇑ULift.moduleEquiv)
    (⇑ULift.moduleEquiv.symm ∘ ⇑(Hom.hom S.g) ∘ ⇑ULift.moduleEquiv)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b

Tactic:
intro x y r

Goal state after:
case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F) x y
⊢ descFunLift F s x = descFunLift F s y
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case refine_1
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₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M ∧ Subsingleton M₂

pp: case refine_2
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₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0

Tactic:
· have A : Subsingleton M := by
      refine ⟨fun x y ↦ e.injective ?_⟩
      simp [he, ← ContinuousLinearEquiv.coe_coe]
    exact ⟨A, e.toEquiv.symm.subsingleton⟩

Goal state after:
case refine_2
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₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0
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
⊢ f.inverse = g

Tactic:
have : f = ContinuousLinearEquiv.equivOfInverse' f g hf hg := rfl

Goal state after:
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)
⊢ f.inverse = g
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ((if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
      if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0).Nodup

Tactic:
split_ifs with h₁ h₂
        · simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
          let f : ((left a : WalkingMulticospan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False
          apply ne_of_apply_ne f
          conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]
          conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]
          simp
        all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this✝ : IsIso (F.map π)
this : IsIso (F.map (φ ≫ π))
⊢ IsIso (F.map φ)

Tactic:
exact IsIso.of_isIso_fac_right (F.map_comp φ π).symm

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

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
⊢ ∀ (F : A ⥤ J), Nonempty (Cocone F)

Tactic:
F

Goal state after:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
⊢ ∀ (F : A ⥤ J), HasCardinalLT (Arrow A) Cardinal.aleph0 → Nonempty (Cocone F)

Tactic:
F

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
⊢ HasCardinalLT (Arrow A) Cardinal.aleph0 → Nonempty (Cocone F)
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
i : ι
⊢ (piScalarRightInv R S N ι) (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1

Tactic:
simp [piScalarRightInv, Pi.single_apply, TensorProduct.ite_tmul]

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

Goal state before:
pp: R A : CommRingCat
inst✝² : TopologicalSpace ↑R
inst✝¹ : IsTopologicalRing ↑R
inst✝ : T1Space ↑R
⊢ IsClosedEmbedding fun f ↦ ⇑(Hom.hom f)

Tactic:
by
  let f : CommRingCat.of (MvPolynomial A (⊥_ CommRingCat)) ⟶ A :=
    CommRingCat.ofHom (MvPolynomial.eval₂Hom (initial.to A).hom id)
  have : Function.Surjective f := Function.LeftInverse.surjective (g := .X) fun x ↦ by simp [f]
  convert!
    ((mvPolynomialHomeomorph A R (.of _)).trans
          (.uniqueProd (⊥_ CommRingCat ⟶ R) _)).isClosedEmbedding.comp
      (isClosedEmbedding_precomp_of_surjective f this) using
    2 with g
  ext x
  simp +instances [f]

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

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
heq : Y.hom = hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ P (hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } })

Tactic:
← hd.coconePointUniqueUpToIso_hom_desc (hc _),

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
heq : Y.hom = hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ P
    ((hd.coconePointUniqueUpToIso (hc (d.diag ⋙ proj L X ⋙ L))).hom ≫
      (hc (d.diag ⋙ proj L X ⋙ L)).desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } })
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : a * ↑p + b * ↑(ringChar R) = 1
⊢ IsUnit ↑p

Tactic:
apply_fun ((↑) : ℤ → R) at hab

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑(a * ↑p + b * ↑(ringChar R)) = ↑1
⊢ IsUnit ↑p
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
let c : Fork f g := Under.equalizerFork f g

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
x y : M
⊢ { toFun := fun a ↦ ⟨(x + y) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun a ↦ ⟨y ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; simp [add_tmul]

Goal state after: