mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.1 i)).map f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (((Functor.const J).obj (F.1 i)).obj Y)) =
      (if h : X = i then eqToHom ⋯ else (H X h).from (((Functor.const J).obj (F.1 i)).obj X)) ≫ F.map f

pp: case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
              naturality := ?refine_2 } } =
    𝟙 (limit F)

pp: case refine_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.lift F
        { pt := F.1 i,
          π :=
            { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
              naturality := ?refine_2 } } ≫
      limit.π F i =
    𝟙 (F.obj i)

Tactic:
· intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        have : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext

Goal state after:
case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
              naturality := ⋯ } } =
    𝟙 (limit F)

case refine_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.lift F
        { pt := F.1 i,
          π :=
            { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
              naturality := ⋯ } } ≫
      limit.π F i =
    𝟙 (F.obj i)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ selfZPow x B ↑m * mk' B a 1 = selfZPow x B ↑d * b

Tactic:
selfZPow_natCast,

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = selfZPow x B ↑d * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = selfZPow x B ↑d * b

Tactic:
selfZPow_natCast,

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = (algebraMap R B) x ^ d * b
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ (PullbackCone.mk h k ⋯).fst = s.fst ∧
        l ≫ (PullbackCone.mk h k ⋯).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt},
            m ≫ (PullbackCone.mk h k ⋯).fst = s.fst → m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = l }

Tactic:
intro s

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ { l //
    l ≫ (PullbackCone.mk h k ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk h k ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt},
          m ≫ (PullbackCone.mk h k ⋯).fst = s.fst → m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
⊢ (s : PushoutCocone h k) →
    { l //
      (PushoutCocone.mk f g ⋯).inl ≫ l = s.inl ∧
        (PushoutCocone.mk f g ⋯).inr ≫ l = s.inr ∧
          ∀ {m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt},
            (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl → (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = l }

Tactic:
intro s

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ { l //
    (PushoutCocone.mk f g ⋯).inl ≫ l = s.inl ∧
      (PushoutCocone.mk f g ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt},
          (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl → (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
⊢ (s : PullbackCone (g₁ ≫ g₂) i₃) →
    { l //
      l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst ∧
        l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
            m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l }

Tactic:
intro s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
⊢ { l //
    l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst ∧
      l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
          m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
⊢ (s : PullbackCone g₁ i₂) →
    { l //
      l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }

Tactic:
intro s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
⊢ { l //
    l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
⊢ (s : PushoutCocone i₁ (f₁ ≫ f₂)) →
    { l //
      (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
        (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
          ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
            (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }

Tactic:
intro s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
⊢ { l //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : Epi f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit sq.cocone

Tactic:
refine
        PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => ?_)
          (by simp) (by simp)
      simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁷ : CommSemiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : IsLocalization S A
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
M' : Type u_4
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : Module A M'
inst✝⁹ : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
⊢ IsLocalizedModule S (Finsupp.mapRange.linearMap f)

Tactic:
classical
  let e : Localization S ⊗[R] M ≃ₗ[R] M' :=
    (LocalizedModule.equivTensorProduct S M).symm.restrictScalars R ≪≫ₗ IsLocalizedModule.iso S f
  let e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] (α →₀ M') :=
    finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
  suffices IsLocalizedModule S (e'.symm.toLinearMap ∘ₗ Finsupp.mapRange.linearMap f) by
    convert! this.of_linearEquiv (e := e')
    ext
    simp
  rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
  convert! TensorProduct.isBaseChange R (α →₀ M) (Localization S) using 1
  ext a m
  apply (finsuppRight R R (Localization S) M α).injective
  ext b
  apply e.injective
  suffices (if a = b then f m else 0) = e (1 ⊗ₜ[R] if a = b then m else 0) by
    simpa [e', Finsupp.single_apply, -EmbeddingLike.apply_eq_iff_eq, apply_ite]
  split_ifs with h
  · simp [e]
  · simp only [tmul_zero, map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
⊢ (s : PushoutCocone «i₂» f₂) →
    { l //
      t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }

Tactic:
intro s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
⊢ { l //
    t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt),
    m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
intro s

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
⊢ ∀ (m : s.pt ⟶ (Fork.ofι f ⋯).pt), m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
intro s

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
⊢ ∀ (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt), (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ a.2 • a.1 • s • p.2 • p'.1 = s • (a.2 * p.2) • a.1 • p'.1

Tactic:
simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]; ring_nf

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ mk (a • 1) (s * 1) = mk ((algebraMap R A) a) s

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ mk (a • 1) (s * 1) = mk (a • 1) s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
p : LocalizedModule S M
⊢ (r • x) • p = r • x • p

Tactic:
induction p with | _ m s
    rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ (𝟭 C).map f ≫ 𝟙 Y.A = f

Tactic:
apply Category.comp_id

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

Goal state before:
pp: case inr
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of B ⟶ of (A ⊗[R] B)

Tactic:
exact ofHom <| Algebra.TensorProduct.includeRight.toRingHom (A := B)

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r * inv j) = (ConcreteCategory.hom (F.map f)) 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (F.map f)) (inv j) = inv k

Tactic:
rw [map_mul, map_one, this] at h

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (F.map f)) (inv j) = inv k
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
⊢ (s : Fork f g) →
    { l //
      l ≫ (equalizerFork f g).ι = s.ι ∧ ∀ {m : s.pt ⟶ (equalizerFork f g).pt}, m ≫ (equalizerFork f g).ι = s.ι → m = l }

Tactic:
intro s

Goal state after:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ { l //
    l ≫ (equalizerFork f g).ι = s.ι ∧ ∀ {m : s.pt ⟶ (equalizerFork f g).pt}, m ≫ (equalizerFork f g).ι = s.ι → m = l }
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case lift
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ (s : PullbackCone f g) →
    s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))

Tactic:
intro s

Goal state after:
case lift
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case lift
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ (s : PullbackCone f g) →
    s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))

Tactic:
intro s
    refine ofHom ((s.fst.hom.prod s.snd.hom).codRestrict _ ?_)
    intro x
    exact congr_arg (fun f : s.pt →+* C => f x) (congrArg Hom.hom s.condition)

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

Goal state before:
pp: case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        ofHom
          ((RingHom.fst ↑A ↑B).comp
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
      s.fst

Tactic:
intro s

Goal state after:
case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        ofHom
          ((RingHom.snd ↑A ↑B).comp
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
      s.snd

Tactic:
intro s

Goal state after:
case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g)
    (m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))),
    m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
        s.fst →
      m ≫
            ofHom
              ((RingHom.snd ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
          s.snd →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)

Tactic:
intro s

Goal state after:
case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ ∀ (m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))),
    m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
        s.fst →
      m ≫
            ofHom
              ((RingHom.snd ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
          s.snd →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, X i = unop Z) → ∃ i, op (X i) = Z

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : X i = unop Z
⊢ ∃ i, op (X i) = Z
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, op (X i) = Z) → ∃ i, X i = unop Z

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
⊢ ∃ i, X i = unop Z
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hmap : (map f I).FG
hk : (I ⊓ RingHom.ker f).FG
hf : Function.Surjective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
⊢ (Submodule.map (Module.compHom.toLinearMap f) I).FG

Tactic:
have : RingHomSurjective f := ⟨hf⟩

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hmap : (map f I).FG
hk : (I ⊓ RingHom.ker f).FG
hf : Function.Surjective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
this : RingHomSurjective f
⊢ (Submodule.map (Module.compHom.toLinearMap f) I).FG