mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (X ⊗ Y) ▷ G.obj Z ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (X ⊗ Y) Z ≫ i.hom.app ((X ⊗ Y) ⊗ Z) ≫ G.map (α_ X Y Z).hom =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z)

Tactic:
rw [← i.hom.naturality, map_associator_assoc, Functor.OplaxMonoidal.associativity_assoc,
      whiskerLeft_δ_μ_assoc, δ_μ_assoc]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (X ⊗ Y) ▷ G.obj Z ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ i.hom.app (X ⊗ Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
⊢ (quotUliftToQuot F) ((quotToQuotUlift F) x) = (AddMonoidHom.id (Quot F)) x

Tactic:
rw [← AddMonoidHom.comp_apply, Quot.addMonoidHom_ext F (f := (quotUliftToQuot F).comp
      (quotToQuotUlift F)) (fun j a ↦ ?_)]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ ((quotUliftToQuot F).comp (quotToQuotUlift F)) ((Quot.ι F j) a) = (AddMonoidHom.id (Quot F)) ((Quot.ι F j) a)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ ∀ (j : J) (x : ↑(F.obj j)),
    ((Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h)) ((Quot.ι F j) x) = (Quot.desc F s) ((Quot.ι F j) x)

Tactic:
simp [← hm]

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case of
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝¹ i✝ x✝ y✝ : N
a : Relation.Map (⇑c) (⇑f) (⇑f) x✝ y✝
⊢ Relation.Map (⇑c) (⇑f) (⇑f) x✝ y✝

Tactic:
exact a

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
⊢ x.fst⁻¹ ≠ 0 ↔ x.fst ≠ 0

Tactic:
ne_eq,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
⊢ ¬x.fst⁻¹ = 0 ↔ ¬x.fst = 0
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ comul = (comul ∘ₗ ↑e.toLinearEquiv) ∘ₗ ↑e.toLinearEquiv.symm

Tactic:
LinearEquiv.comp_symm_cancel_right

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ comul = comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
⊢ rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul = (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1

Tactic:
ext : 1
    rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
⊢ rTensor (ι →₀ A) counit ∘ₗ comul = (TensorProduct.mk R R (ι →₀ A)) 1

Tactic:
ext : 1
    rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

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

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f g : R →+* S
e : f = g
X : ModuleCat S
x✝¹ : R
x✝ : ↑((restrictScalars f).obj X)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun x✝

Tactic:
subst e

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
x✝¹ : R
x✝ : ↑((restrictScalars f).obj X)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f g : R →+* S
e : f = g
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
⊢ (restrictScalars f).map x✝ ≫
      (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj Y✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom =
    (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj X✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom ≫
      (restrictScalars g).map x✝

Tactic:
subst e

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
⊢ (restrictScalars f).map x✝ ≫
      (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj Y✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom =
    (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj X✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom ≫
      (restrictScalars f).map x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalars f₁₂).map ((extendScalarsId R₁).hom.app M))) (1 ⊗ₜ[R₁] (1 ⊗ₜ[R₁] m)) =
    LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
rw [ExtendScalars.map_tmul]

Goal state after:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] (ConcreteCategory.hom ((extendScalarsId R₁).hom.app M)) (1 ⊗ₜ[R₁] m) = LinearMap.id (1 ⊗ₜ[R₁] m)
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
← unit_leftAdjointUniq_hom adj1 adj2

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B) (comul a ⊗ₜ[R] comul 1)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A) (comul 1 ⊗ₜ[R] comul a)

Tactic:
← (ℛ R a).eq

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B)
        ((∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i) ⊗ₜ[R] comul 1)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A)
      (comul 1 ⊗ₜ[R] ∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i)
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B) (comul 1 ⊗ₜ[R] comul a)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A) (comul a ⊗ₜ[R] comul 1)

Tactic:
← (ℛ R a).eq

Goal state after:
case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B)
        (comul 1 ⊗ₜ[R] ∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A)
      ((∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i) ⊗ₜ[R] comul 1)
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)
⊢ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f

Tactic:
rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq]

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

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) (normalize a) ≤ normalizedFactors b

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ ((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
      Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
        ⋯ =
    Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
        ⋯ ≫
      (𝟭 (Under R)).map f

Tactic:
by
      ext : 2
      apply MonoidAlgebra.ringHom_ext <;>
        intro <;> simp [MonoidAlgebra.liftNCRingHom, ← Under.w f, -Under.w]

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

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Tactic:
by
  rw [← pow_dvd_iff_le_emultiplicity]
  revert b
  induction n with
  | zero => simp
  | succ n ih => ?_
  intro b hb
  constructor
  · rintro ⟨c, rfl⟩
    rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb
    rw [pow_succ', mul_assoc, normalizedFactors_mul hb.1 hb.2, replicate_succ,
      normalizedFactors_irreducible ha, singleton_add, cons_le_cons_iff, ← ih hb.2]
    apply Dvd.intro _ rfl
  · rw [Multiset.le_iff_exists_add]
    rintro ⟨u, hu⟩
    rw [← (prod_normalizedFactors hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]
    exact (Associated.pow_pow <| associated_normalize a).dvd.trans (Dvd.intro u.prod rfl)

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N

Tactic:
convert! map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)

Goal state after:
case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Submodule.map N.subtype (Ring.jacobson R • ⊤)

case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I J : Ideal R
⊢ I ≤ J → I.jacobson ≤ J.jacobson

Tactic:
intro h x hx
  rw [jacobson, mem_sInf] at hx ⊢
  exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩

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

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : IsUnit x
H : x ∈ I
⊢ 1 ∈ I

Tactic:
rcases hx with ⟨u, rfl⟩

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
a✝ : maximalIdeal R ≤ I
u : Rˣ
H : ↑u ∈ I
⊢ 1 ∈ I
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ IsLocalHom f

Tactic:
have := IsLocalRing.of_surjective' f ‹_›

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalRing S
⊢ IsLocalHom f
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ IsUnit (f b)

Tactic:
by rw [hb]; exact Units.isUnit _

Goal state after:
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
⊢ (algebraMap R B) x ^ (n.natAbs + m.natAbs) = (algebraMap R B) x ^ n.natAbs * (algebraMap R B) x ^ m.natAbs

Tactic:
pow_add

Goal state after:
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
⊢ (algebraMap R B) x ^ n.natAbs * (algebraMap R B) x ^ m.natAbs =
    (algebraMap R B) x ^ n.natAbs * (algebraMap R B) x ^ m.natAbs
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
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
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ selfZPow x B (n + m) = selfZPow x B n * (algebraMap R B) x ^ m.natAbs

Tactic:
selfZPow_of_neg _ _ hn,

Goal state after:
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
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ selfZPow x B (n + m) = mk' B 1 (Submonoid.pow x n.natAbs) * (algebraMap R B) x ^ m.natAbs
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
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:
selfZPow_of_neg _ _ hn,

Goal state after:
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) = mk' B 1 (Submonoid.pow x n.natAbs) * selfZPow x B m
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 = (algebraMap R B) x ^ m * (algebraMap R B) a

Tactic:
exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩

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₂
⊢ IsColimit (t₁.pasteHoriz t₂ hi₂)

Tactic:
by
  apply PushoutCocone.isColimitAux'
  intro s
  -- Obtain the induced map from descending from both the small squares consecutively.
  obtain ⟨l₁, hl₁, hl₁'⟩ := PushoutCocone.IsColimit.desc' H s.inl (f₂ ≫ s.inr)
    (by rw [s.condition, Category.assoc])
  obtain ⟨l₂, hl₂, hl₂'⟩ := PushoutCocone.IsColimit.desc' H' l₁ s.inr (by rw [← hl₁', hi₂])
  refine ⟨l₂, by simp [hl₂, hl₁], hl₂', ?_⟩
  -- Uniqueness also follows from the universal property of both the small squares.
  intro m hm₁ hm₂
  apply PushoutCocone.IsColimit.hom_ext H' _ (by simpa [hl₂'] using hm₂)
  simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hm₁ hm₂
  apply PushoutCocone.IsColimit.hom_ext H
  · rw [hm₁, ← hl₁, hl₂]
  · rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']

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

Goal state before:
pp: case lift
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') → s.pt ⟶ (Fork.ofι f ⋯).pt

pp: case fac
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'), ?lift s ≫ (Fork.ofι f ⋯).ι = s.ι

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 = ?lift s

Tactic:
· exact fun s => H.isLimit.lift (PullbackCone.mk s.ι s.ι s.condition)

Goal state after:
case fac
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'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι

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: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
⊢ f₁ ≫ f₃ = f₂ ≫ f₄

Tactic:
ext X
    simpa using (h X).w

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₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
⊢ f₁ ≫ f₃ = f₂ ≫ f₄

Tactic:
ext X
    simpa using (h X).w

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 : T.free.obj X ⟶ Y
⊢ (fun f ↦ { f := T.map f ≫ Y.a, h := ⋯ }) ((fun f ↦ T.η.app X ≫ f.f) f) = f

Tactic:
ext
            simp

Goal state after: