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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (φ (x' - x)) y₁ ∈ W'

Tactic:
forall_mem_comm

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ (a b : β), a ∈ U₂ → b ∈ U₂ → (φ (b - a)) y₁ ∈ W'
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioi (x i₀) ∩ Iic (y i₀)

Tactic:
inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Ioi m ∩ Iic (y i₀) = Ioi m ∩ Iic (y i₀)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = generateFrom {s | ∃ a, s = Iio a ∨ s = Ioi a}

Tactic:
simp_rw [or_comm]

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ i ∈ s.1, (Ioi ↑i).OrdConnected

Tactic:
intro _ _

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Iio a))
hi✝ : i✝ ∈ s.1
⊢ (Ioi ↑i✝).OrdConnected
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ i ∈ s.2, (Iio ↑i).OrdConnected

Tactic:
intro _ _

Goal state after:
case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Ioi a))
hi✝ : i✝ ∈ s.2
⊢ (Iio ↑i✝).OrdConnected
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : IsEmpty α
⊢ ∃ c, c.Countable ∧ ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

pp: case inr
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
⊢ ∃ c, c.Countable ∧ ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
· exact ⟨∅, by simp, Subsingleton.elim _ _⟩

Goal state after:
case inr
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
⊢ ∃ c, c.Countable ∧ ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
⊢ (e.prod e').symm = e.symm.prod e'.symm

Tactic:
ext x <;> simp [prod_coe_symm]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: X✝ Y✝ : MonCat
f : X✝ ⟶ Y✝
⊢ η ≫ ↾⇑(hom f) = η

Tactic:
simp +instances only

Goal state after:
X✝ Y✝ : MonCat
f : X✝ ⟶ Y✝
⊢ (↾fun x ↦ 1) ≫ ↾⇑(hom f) = ↾fun x ↦ 1
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: X✝ Y✝ : MonCat
f : X✝ ⟶ Y✝
⊢ μ ≫ ↾⇑(hom f) = MonoidalCategoryStruct.tensorHom (↾⇑(hom f)) (↾⇑(hom f)) ≫ μ

Tactic:
simp +instances only

Goal state after:
X✝ Y✝ : MonCat
f : X✝ ⟶ Y✝
⊢ (↾fun p ↦ p.1 * p.2) ≫ ↾⇑(hom f) = MonoidalCategoryStruct.tensorHom (↾⇑(hom f)) (↾⇑(hom f)) ≫ ↾fun p ↦ p.1 * p.2
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
p : 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ ↑a
⊢ ContinuousAt (⇑(equivIco p a)) x

Tactic:
by
  induction x using QuotientAddGroup.induction_on
  rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
  exact (continuousAt_toIcoMod hp.out a <| not_modEq_iff_ne_mod_zmultiples.mpr hx).codRestrict _

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

Goal state before:
pp: case refine_2
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
⊢ a ∈ Ioi (sSup (f ⁻¹' Iic z))

Tactic:
· apply lt_of_le_of_ne
        · exact csSup_le ne fun b hb ↦ (hf.mono.reflect_lt (hb.trans_lt ha)).le
        · have : sSup (f '' f ⁻¹' Iic z) ≤ z := csSup_le (.image _ ne) fun _ ⟨b, hb, heq⟩ ↦ heq ▸ hb
          exact fun h ↦ this.not_gt ((h ▸ ha).trans_eq (hf.map_csSup ne bdd))

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ addOrderOf ↑(p / ↑n) = n

Tactic:
by
  rw [addOrderOf_eq_iff h]
  replace h : 0 < (n : 𝕜) := Nat.cast_pos.2 h
  refine ⟨?_, fun m hn h0 => ?_⟩ <;> simp only [Ne, ← coe_nsmul, nsmul_eq_mul]
  · rw [mul_div_cancel₀ _ h.ne', coe_period]
  rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]
  rintro ⟨k, hk⟩
  rw [mul_div, eq_div_iff h.ne', nsmul_eq_mul, mul_right_comm, ← Nat.cast_mul,
    (mul_left_injective₀ hp.out.ne').eq_iff, Nat.cast_inj, mul_comm] at hk
  exact (Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_gt hn

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ (𝟭 (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C)).map f ≫
      (isoOfComponents (fun x ↦ Y✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom =
    (isoOfComponents (fun x ↦ X✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom ≫ (laxBraidedToCommMon C ⋙ commMonToLaxBraided C).map f

Tactic:
by ext ⟨⟨⟩⟩; dsimp; simp

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

Goal state before:
pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = (Hom.hom (↟N.subtype)).range

Tactic:
· exact (Submodule.range_subtype _).symm

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
q : 𝕋
⊢ ?m.37

Tactic:
simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q

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

Goal state before:
pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
    { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T
⊢ S = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range

Tactic:
← hom_comp,

Goal state after:
case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
    { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T
⊢ S = (Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h ≫ ↟T.subtype)).range
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_4
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
    { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T
⊢ T = (Hom.hom (↟T.subtype)).range

Tactic:
· exact (Submodule.range_subtype _).symm

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
X Y : ModuleCat R
f g : X ⟶ Y
h : ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R), (Hom.hom f) ((Hom.hom h) x) = (Hom.hom g) ((Hom.hom h) x)
x : ↑X
⊢ (Hom.hom f) x = (Hom.hom g) x

Tactic:
simpa using h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp
    (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ y ≫ Cofork.π c = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
by
  refine ⟨fun hy ↦ ?_, ?_⟩
  · have h := (ShortComplex.mk _ _ c.condition).exact_of_g_is_cokernel
      (IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by simp)))
    rw [ShortComplex.exact_iff_exact_up_to_refinements] at h
    obtain ⟨A', π, hπ, x₁, fac⟩ := h y hy
    exact ⟨A', π, hπ, x₁, fac⟩
  · rintro ⟨A', π, hπ, x, fac⟩
    simp [← cancel_epi π, reassoc_of% fac, condition]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
⊢ (fun j ↦
      match j with
      | WalkingMulticospan.left a => ↑x a
      | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b))) ∈
    (I.multicospan ⋙ forget C).sections

Tactic:
rintro (a | b) (a' | b') (f | f | f)
        · simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl
        · rfl
        · dsimp
          exact (x.2 b').symm
        · simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl

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

Goal state before:
pp: case some
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
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y

Tactic:
use j, y

Goal state after:
case h
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
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (hom (ι f j)) y = (hom (colimit.ι (wideSpan B X f) (some j))) y
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) (x + y)) =
    (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x) + fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) y

Tactic:
simp only [Functor.const_obj_obj, map_add]

Goal state after:
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x + (ConcreteCategory.hom (s.π.app { as := j })) y) =
    (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x) + fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) y
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✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) =
      (match X with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) ≫
        ((Functor.const (WalkingMultispan J)).obj P).map f

Tactic:
by
        rintro (_ | _) (_ | _) (_ | _ | _) <;> dsimp <;>
          simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]
        symm
        apply w

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ adj.unit ≫ i.hom ≫ (adj.toMonad.transport i).μ = 𝟙 (𝟭 C)

Tactic:
by
    rw [← assoc]
    ext X
    exact (adj.toMonad.transport i).right_unit X

Goal state after:
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
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯ = 𝟙 F

Tactic:
apply hom_ext_succ
    · simp
    · ext ⟨i, hi⟩
      simp

Goal state after:
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
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w = 𝟙 G

Tactic:
apply hom_ext_succ
    · simp
    · ext ⟨i, hi⟩
      simp

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 : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j ≫ t.desc (newCocone D c))

Tactic:
t.fac (newCocone D c) j,

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 : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) = (D.obj j).a ≫ T.map ((newCocone D 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
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
⊢ CreatesLimit K R

Tactic:
letI : PreservesLimit
    (((K ⋙ A) ⋙ Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))) ⋙
      (Adjunction.toComonad (comonadicAdjunction R)).toFunctor)
      (Adjunction.toComonad (comonadicAdjunction R)).toFunctor := by
    dsimp
    exact preservesLimit_of_iso_diagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm

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
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
this : PreservesLimit
  (((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) ⋙ (comonadicAdjunction R).toComonad.toFunctor)
  (comonadicAdjunction R).toComonad.toFunctor :=
  comonadicCreatesLimitOfPreservesLimit._proof_2 R K
⊢ CreatesLimit K R
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
P : Ideal B
p : Ideal A
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
⊢ (stabilizerHom P p G).ker = inertia (↥(MulAction.stabilizer G P)) P

Tactic:
by
  ext σ
  simp [DFunLike.ext_iff, mk_surjective.forall, Quotient.eq]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

Tactic:
rw [← mem_nilradical, nilradical_eq_sInf, Submodule.mem_sInf]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) f ^ k = 0 ↔ f ^ k = 0

Tactic:
rw [toMatrix_pow]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) (f ^ k) = 0 ↔ f ^ k = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ map (Quotient.mk (I ^ 2)) I ^ 2 = ⊥

Tactic:
rw [← Ideal.map_pow, Ideal.map_quotient_self]

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x y : R
e : (algebraMap R' S') (f (x - y)) = 0
⊢ ∃ c, ↑c * f x = ↑c * f y

Tactic:
← RingHom.comp_apply,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x y : R
e : ((algebraMap R' S').comp f) (x - y) = 0
⊢ ∃ c, ↑c * f x = ↑c * f y
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
H : ∀ (P : Ideal S) [inst : P.IsMaximal], Flat R (Mₚ P)
⊢ Flat R M

Tactic:
simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢
  simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]
  refine fun _ _ _ N ↦ injective_of_isLocalized_maximal _
    (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _
    (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _ fun P hP ↦ ?_
  simpa [IsLocalizedModule.map_lTensor] using H P N

Goal state after: