mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
slice_lhs 3 4 =>
    rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c) ≫ R₂.map (H.map (𝟙 (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case mul
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : TensorAlgebra R M
hx : x ∈ Algebra.adjoin R (Set.range ⇑(ι R))
hy : y ∈ Algebra.adjoin R (Set.range ⇑(ι R))
⊢ x * y ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
exact mul_mem hx hy

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α)) by simpa using this
  infer_instance

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -((inr m).fst⁻¹ •> (inr m).snd <• (inr m).fst⁻¹) = snd 0

Tactic:
snd_inr,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -((inr m).fst⁻¹ •> m <• (inr m).fst⁻¹) = snd 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul

Tactic:
TensorProduct.map_id,

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = LinearMap.id ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul

Tactic:
TensorProduct.map_id,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = LinearMap.id ∘ₗ comul
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) ((inl r₁ + inr m₁) * (inl r₂ + inr m₂)) =
    ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) (inl r₁ + inr m₁) *
      ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) (inl r₂ + inr m₂)

Tactic:
by
        dsimp
        simp only [add_zero, zero_add, add_mul, mul_add, hg]
        rw [← map_mul, map_add, add_comm (g _), add_assoc, hfg, hgf]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ Δ = Δ ≫ (F.map f ⊗ₘ F.map f)

Tactic:
by
    dsimp
    rw [Category.assoc, δ_natural, ← F.map_comp_assoc, ← F.map_comp_assoc, hom_comul]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
⊢ a ∣ b

Tactic:
let : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ a ∣ b
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
by
  constructor
  · intro h x hx
    rw [← h, Ideal.jacobson, mem_sInf] at hx
    push Not at hx
    exact hx
  · refine fun h => le_antisymm (fun x hx => ?_) le_jacobson
    contrapose hx
    rw [Ideal.jacobson, mem_sInf]
    push Not
    exact h x hx

Goal state after:
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ (maximalIdeal R).IsMaximal

Tactic:
by
  rw [Ideal.isMaximal_iff]
  constructor
  · intro h
    apply h
    exact isUnit_one
  · intro I x _ hx H
    rw [mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] at hx
    rcases hx with ⟨u, rfl⟩
    simpa using I.mul_mem_left (↑u⁻¹) H

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

Goal state before:
pp: R : CommRingCat
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))

Tactic:
cases R

Goal state after:
case of
carrier✝ : Type u_1
commRing✝ : CommRing carrier✝
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of carrier✝)) (Localization.Away 1)))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inl.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
· rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_nonneg _ _ hm,
      selfZPow_of_nonneg _ _ (add_nonneg hn hm), Int.natAbs_add_of_nonneg hn hm, pow_add]

Goal state after:
case inl.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

case inr.inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
hf : Injective f
i j : ↥s
h : integerMultiple M s f i = integerMultiple M s f j
⊢ i = j

Tactic:
rw [← SetLike.coe_eq_coe, ← hf.eq_iff,
    ← (IsLocalization.smul_bijective S (commonDenom M s f)).injective.eq_iff,
    ← map_integerMultiple M s f i, ← map_integerMultiple M s f j, h]

Goal state after:
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₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
⊢ { 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:
refine ⟨l₁, hl₁, by simp [reassoc_of% hl₁', hl₂'], ?_⟩

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₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
⊢ ∀ {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.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_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
← (map_units A s).smul_left_cancel

Goal state after:
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_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x y : Multiplicative (Multiset α)
⊢ (Multiset.map f (Multiplicative.toAdd (x * y))).prod = (Multiset.map f x + Multiset.map f y).prod

Tactic:
by
            rw [← Multiset.map_add]
            rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimitsOfShape WalkingCospan F

Tactic:
suffices h : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F from
    ⟨fun {K} ↦ preservesLimit_of_iso_diagram _ (Limits.diagramIsoCospan K).symm⟩
  intro X Y Z f g
  refine .mk' fun h ↦ ?_
  obtain ⟨P, fst, snd, h, h'⟩ := H f g
  rwa [h.preservesLimit_cospan_iff]

Goal state after:
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
x : T
| x • 0

Tactic:
← zero_mk 1,

Goal state after:
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
x : T
| x • mk 0 1
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'
s : ↥S
r : R
x : LocalizedModule S M
⊢ (r • x).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ = (RingHom.id R) r • x.liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
refine x.induction_on (fun _ _ ↦ ?_)

Goal state after:
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'
s : ↥S
r : R
x : LocalizedModule S M
x✝¹ : M
x✝ : ↥S
⊢ (r • mk x✝¹ x✝).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    (RingHom.id R) r • (mk x✝¹ x✝).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
r : R
f : M →ₗ[A] N
h : IsLocalizedModule (Submonoid.powers ((algebraMap R A) r)) f
⊢ IsLocalizedModule (Submonoid.powers r) (↑R f)

Tactic:
rw [← Algebra.algebraMapSubmonoid_powers] at h

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
r : R
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A (Submonoid.powers r)) f
⊢ IsLocalizedModule (Submonoid.powers r) (↑R f)
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = ((map f).obj y).hom

Tactic:
simp only [map_obj_hom]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ y.hom
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m } = ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom

Tactic:
apply CommRingCat.hom_ext

Goal state after:
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m }.hom =
    Hom.hom (ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ IsLimit (pullbackCone f g)

Tactic:
fapply PullbackCone.IsLimit.mk

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)))

case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ?lift s ≫
        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

case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ?lift s ≫
        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

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 = ?lift s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular
    ((fun x ↦
        match x with
        | (r, m) => IsLocalization.mk' A r m)
      (a, s))
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₁, t₁)) =
    (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₂, t₂))
hS : ∀ s ∈ S, IsRegular s
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)

Tactic:
IsLocalization.isRegular_mk' hS

Goal state after:
case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₁, t₁)) =
    (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₂, t₂))
hS : ∀ s ∈ S, IsRegular s
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
⊢ f.hom ≫
      { pt := Over.mk (t₂.π.app star),
            π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.pt.hom =
    { pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.pt.hom

Tactic:
by simp [dsimp% f.w star]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ j₂ : J
⊢ r j₁ j₂

Tactic:
have z : ∀ j : J, r j₁ j :=
    induct_on_objects {k | r j₁ k} (hr.1 j₁)
      fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ j₂ : J
z : ∀ (j : J), r j₁ j
⊢ r j₁ j₂
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G H : D ⥤ C
α : G ≅ H
X✝ Y✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
⊢ (pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom =
    ({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
      (map (whiskerRight α.hom F) ⋙ pre F H).map f

Tactic:
fapply Grothendieck.ext <;> simp

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
⊢ ∀ (k₂ : X ⟶ F.obj Z₂) (f_1 : Z₁ ⟶ Z₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂

Tactic:
k₂

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
⊢ ∀ (f_1 : Z₁ ⟶ Z₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂