mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderTopology (α i)
f : (i : ι) → α i
⊢ TendstoIxxClass Icc (𝓝 f) (𝓝 f)

Tactic:
by
  constructor
  conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi]
  simp only [smallSets_iInf, smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff]
  intro i
  have : Tendsto (fun g : ∀ i, α i => g i) (𝓝 f) (𝓝 (f i)) := (continuous_apply i).tendsto f
  refine (this.comp tendsto_fst).Icc (this.comp tendsto_snd) |>.smallSets_mono ?_
  filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst✝³] (Ioc (z x) x)

Tactic:
rw [H]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst✝³] (Ioo (z x) (y x))
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this✝ : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
this : ∀ u ∈ s, ∀ v ∈ s, f u ≠ f v → u ≤ v → (Disjoint on fun x ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
hle : ¬u ≤ v
⊢ (Disjoint on fun x ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
exact (this v vs u us huv.symm (le_of_not_ge hle)).symm

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0

Tactic:
rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) ((hom (piComparison F f)) x) =
    (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) ((hom (piComparison F f)) y)

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (piComparison F f ≫ limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) x =
    (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) ((hom (piComparison F f)) y)
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (piComparison F f ≫ limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) x =
    (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) ((hom (piComparison F f)) y)

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (piComparison F f ≫ limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) x =
    (hom (piComparison F f ≫ limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) y
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) ((ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x) = 0

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.f ≫ (forget₂ C Ab).map S.g)) x = 0
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ (ConcreteCategory.hom ((S.mapCyclesIso (forget₂ C Ab)).hom ≫ (forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.L₂.f) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)) =
    (ConcreteCategory.hom D.L₂.f) x₁

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom (D.φ₁ ≫ D.L₂.f)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    (ConcreteCategory.hom D.L₂.f) x₁
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j + 1 < n + 1 + 1
⊢ 1 ≤ ⟨j + 1, hj⟩

Tactic:
simp [Fin.le_def]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π

Tactic:
by
  apply Cofan.IsColimit.hom_ext hc
  simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (T.mapCocone (T.mapCocone c)).ι.app j ≫ T.μ.app c.pt ≫ lambda c t =
    (T.mapCocone (T.mapCocone c)).ι.app j ≫ T.map (lambda c t) ≫ lambda c t

Tactic:
rw [Functor.mapCocone_ι_app, Functor.mapCocone_ι_app,
      show (T : C ⥤ C).map ((T : C ⥤ C).map _) ≫ _ ≫ _ = _ from T.μ.naturality_assoc _ _, ←
      Functor.map_comp_assoc, commuting, Functor.map_comp, Category.assoc, commuting]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map (D.obj j).a ≫ (D.obj j).a ≫ c.ι.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : MonadicRightAdjoint R
inst✝ : PreservesColimitsOfShape J R
⊢ PreservesColimitsOfShape J (monadicLeftAdjoint R)

Tactic:
apply (Adjunction.leftAdjoint_preservesColimits (monadicAdjunction R)).1

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ 𝟙 c.pt ≫ c.π.app B = c.π.app A ≫ (D.map f).f

Tactic:
rw [id_comp, ← c.w]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ c.π.app ?m.162 ≫ (D ⋙ T.forget).map ?m.164 = c.π.app A ≫ (D.map f).f

C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ ?m.162 ⟶ B

C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ J
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ (comonadicAdjunction R).toComonad.forget ≅ K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R)) (comonadicAdjunction R).toComonad.forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
this : PreservesLimit ((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget)
  (comonadicAdjunction R).toComonad.toFunctor :=
  comonadicCreatesLimitOfPreservesLimit._proof_1 R K
⊢ PreservesLimit (((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) ⋙ (comonadicAdjunction R).toComonad.toFunctor)
    (comonadicAdjunction R).toComonad.toFunctor

Tactic:
by
    dsimp
    exact preservesLimit_of_iso_diagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ ↑(localized' S p f ⊤) = ↑⊤

Tactic:
by apply SetLike.ext'_iff.mp <| Submodule.localized₀_top p f

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
⊢ P ∈ (map (algebraMap R S) I ⊔ J).minimalPrimes

Tactic:
refine ⟨⟨inferInstance, sup_le_iff.mpr ?_⟩, fun q ⟨_, hleq⟩ hqle ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
⊢ map (algebraMap R S) I ≤ P ∧ J ≤ P

case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ⊔ J ≤ q
⊢ P ≤ q
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (I ^ n)) x) ↔ IsUnit ((mk I) x)

Tactic:
rw [← IsNilpotent.isUnit_quotient_mk_iff (I := Ideal.map (Ideal.Quotient.mk (I ^ n)) I)]
  · rw [← isUnit_map_iff (DoubleQuot.quotQuotEquivQuotOfLE (Ideal.pow_le_self hn))]
    rfl
  · use n
    simp [← Ideal.map_pow]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
⊢ IsUnit ((mk (I ^ n)) x)

Tactic:
by_cases! hn : n = 0

Goal state after:
case pos
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit ((mk (I ^ n)) x)

case neg
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n ≠ 0
⊢ IsUnit ((mk (I ^ n)) x)
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ (coeSubmodule S I).IsPrincipal

Tactic:
· refine ⟨⟨algebraMap R S x, ?_⟩⟩
    rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank S N ≤ Module.rank R N

Tactic:
(rw [Module.rank]; apply ciSup_le'; intro ⟨s, hs⟩)

Goal state after:
case inr.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
s : Set N
hs : LinearIndepOn S id s
⊢ #↑↑⟨s, hs⟩ ≤ Module.rank R N
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R N ≤ Module.rank S N

Tactic:
(rw [Module.rank]; apply ciSup_le'; intro ⟨s, hs⟩)

Goal state after:
case a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
s : Set N
hs : LinearIndepOn R id s
⊢ #↑↑⟨s, hs⟩ ≤ Module.rank S N
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
⊢ finrank S N = finrank R N

Tactic:
by
  simp_rw [finrank, rank_eq S p hp]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit ((algebraMap R[X] R[T;T⁻¹]) ↑⟨(fun x ↦ X ^ x) n, ⋯⟩)

Tactic:
rw [algebraMap_eq_toLaurent, toLaurent_X_pow]

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (T ↑n)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
M : Matrix n n α
v : n → α
h : M *ᵥ v = 0
i : n
hi : v i ∈ nonZeroDivisors α
⊢ M.det = 0

Tactic:
apply mul_right_mem_nonZeroDivisors_eq_zero_iff hi |>.mp
  simpa [adjugate_mul, smul_mulVec] using congr((M.adjugate *ᵥ $h) i)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
f g : R[T;T⁻¹]
x y : Sˣ
⊢ f = g → x = y → f.smeval x = g.smeval y

Tactic:
by rintro rfl rfl; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v ↦ v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows i ᵥ* A) j = Pi.single i 1 j

Tactic:
← hrows

Goal state after:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v ↦ v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows i ᵥ* A) j = (fun v ↦ v ᵥ* A) (rows i) j