mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Surjective ⇑(c.lift f h) ↔ Surjective ⇑f

Tactic:
refine ⟨fun H ↦ (Quot.surjective_lift fun x x_1 h_1 ↦ h h_1).mp H,
    fun H ↦ AddCon.lift_surjective_of_surjective h H⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x ^ 0).snd = snd 1

Tactic:
by simp [snd_pow_eq_sum]

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

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a ι
this :
  (LinearMap.lTensor R ↑f) (∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i) =
    (LinearMap.lTensor R ↑f) (1 ⊗ₜ[R] a)
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a

Tactic:
simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_coe]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
⊢ LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul = (mk S (A ⊗[R] B) S).flip 1

Tactic:
ext x y
    convert!
      congr((TensorProduct.rid S _).symm
        (TensorProduct.rid _ _ $(lTensor_counit_comul (R := S) x) ⊗ₜ[R]
          TensorProduct.rid _ _ $(lTensor_counit_comul (R := R) y)))
    · dsimp
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := R) y with y₁ y₂
      apply (TensorProduct.rid S _).injective
      dsimp
      rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
    · dsimp
      simp only [one_smul]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ Away ((algebraMap R S) r) T

Tactic:
by
  refine Away.of_surjective h₁ ?_ n ?_
  · rwa [← IsScalarTower.algebraMap_apply]
  · rw [← (RingHom.ker (algebraMap S T)).map_comap_of_surjective _ h₂, ← map_pow,
      ← Ideal.map_pointwise_smul, RingHom.comap_ker, ← IsScalarTower.algebraMap_eq]
    rwa [RingHom.ker_eq_comap_bot (algebraMap R S), ← Ideal.map_le_iff_le_comap] at hn

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : comap (Quotient.mk I) ⊥.radical = comap (Quotient.mk I) ⊥.jacobson
⊢ I.radical = I.jacobson

Tactic:
comap_radical,

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : (comap (Quotient.mk I) ⊥).radical = comap (Quotient.mk I) ⊥.jacobson
⊢ I.radical = I.jacobson
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
⊢ ∃ b, ∀ i ∈ s, IsInteger R (↑b • f i)

Tactic:
have := Classical.propDecidable
  refine ⟨∏ i ∈ s, (sec M (f i)).2, fun i hi => ⟨?_, ?_⟩⟩
  · exact (∏ j ∈ s.erase i, (sec M (f j)).2) * (sec M (f i)).1
  rw [map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]
  congr 2
  refine _root_.trans ?_ (map_prod (Submonoid.subtype M) _ _).symm
  rw [mul_comm, Submonoid.coe_finsetProd,
    -- Porting note: explicitly supplied `f`
    ← Finset.prod_insert (f := fun i => ((sec M (f i)).snd : R)) (s.notMem_erase i),
    Finset.insert_erase hi]
  rfl

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

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ ⊤ ≤ span Rₛ (Set.range (⇑f ∘ ⇑b))

Tactic:
by
    rw [Set.range_comp, span_eq_top_of_isLocalizedModule Rₛ S _ b.span_eq]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst✝ : MonObj (F.obj X)
⊢ F.map (hF.preimage («η» F ≫ η) ▷ X ≫ hF.preimage (δ F X X ≫ μ)) = F.map (λ_ X).hom

Tactic:
simp [← δ_natural_left_assoc]

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
⊢ prod.lift s.fst (s.snd ≫ prod.snd) ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd

Tactic:
ext
      · simp [PullbackCone.condition]
      · simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
s : ↥S
⊢ (equivTensorProduct S M).symm (Localization.mk r s ⊗ₜ[R] x) = r • mk x s

Tactic:
by
  simp [equivTensorProduct, IsBaseChange.equiv_tmul, mk_smul_mk, smul'_mk]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝ : IsIso i
h : HasPushout (f ≫ i) g
⊢ HasPushout (f ≫ 𝟙 X) g

Tactic:
← IsIso.hom_inv_id i,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝ : IsIso i
h : HasPushout (f ≫ i) g
⊢ HasPushout (f ≫ i ≫ inv i) g
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case add
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ + y✝

Tactic:
rcases hx with ⟨x, rfl⟩

Goal state after:
case add
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x + y✝
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case mul
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ * y✝

Tactic:
rcases hx with ⟨x, rfl⟩

Goal state after:
case mul
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x * y✝
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
A B : Under R
f : A ⟶ B
a : ↑R
this : (ConcreteCategory.hom (A.hom ≫ Under.Hom.right f)) a = (ConcreteCategory.hom B.hom) a
⊢ (↑↑(Hom.hom (Under.Hom.right f))).toFun ((algebraMap ↑R ↑A.right) a) = (algebraMap ↑R ↑B.right) a

Tactic:
simpa only [Functor.const_obj_obj, Functor.id_obj, CommRingCat.comp_apply] using! this

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

Goal state before:
pp: case property.left
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
x : ↑(of A)
⊢ (Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom))
      x =
    (Hom.hom s.inl) x

Tactic:
exact Algebra.TensorProduct.productMap_left_apply (A := A) _ _ x

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
A B : Type u
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra (↑R) A
inst✝ : Algebra (↑R) B
f : A →ₐ[↑R] B
⊢ (R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom = (R.mkUnder B).hom

Tactic:
ext a
    exact f.commutes' a

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
⊢ (fun f ↦ (initial.to (StructuredArrow.mk f)).right) ((fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g

Tactic:
let g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g rfl

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
⊢ (fun f ↦ (initial.to (StructuredArrow.mk f)).right) ((fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid M'
inst✝¹⁵ : AddCommMonoid M''
A : Type u_5
inst✝¹⁴ : CommSemiring A
inst✝¹³ : Algebra R A
inst✝¹² : Module A M'
inst✝¹¹ : IsLocalization S A
inst✝¹⁰ : Module R M
inst✝⁹ : Module R M'
inst✝⁸ : Module R M''
inst✝⁷ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₁ x₂ : M × ↥S₁
c : ↥S₂
e : ↑c • ↑x₁.2 • x₂.1 = ↑c • ↑x₂.2 • x₁.1
⊢ ∃ c s, ↑s • ↑x₁.2 • ↑c • x₂.1 = ↑s • ↑x₂.2 • ↑c • x₁.1

Tactic:
exact ⟨c, 1, by simpa [← smul_comm c.1]⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : AddCommMonoid M''
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
inst✝¹¹ : Module A M'
inst✝¹⁰ : IsLocalization S A
inst✝⁹ : Module R M
inst✝⁸ : Module R M'
inst✝⁷ : Module R M''
inst✝⁶ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ : M →ₗ[R] M''
inst✝⁵ : IsLocalizedModule S f
N : Type ?u.59
N' : Type ?u.61
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (r • h)) ⋯ = (RingHom.id R) r • lift S f (g ∘ₗ h) ⋯

Tactic:
by
    apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
    simp only [lift_comp, LinearMap.smul_comp, LinearMap.comp_smul, RingHom.id_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.map₂ (η ◁ η✝) ≫ F.mapComp η g'✝) ≫ G.mapComp (F.map η) (F.map g'✝) =
    (G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)

Tactic:
mapComp_naturality_right,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.mapComp η g✝ ≫ F.map η ◁ F.map₂ η✝) ≫ G.mapComp (F.map η) (F.map g'✝) =
    (G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.mapComp η g✝) ≫ G.map₂ (F.map η ◁ F.map₂ η✝) ≫ G.mapComp (F.map η) (F.map g'✝) =
    (G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)

Tactic:
mapComp_naturality_right,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝) =
    (G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.mapComp f x✝¹ ≫ F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)

Tactic:
mapComp_naturality_right,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.map f ◁ F.map₂ η ≫ F.mapComp f x✝) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case singleton
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ ∃ n, (R ∙ x) ^ n ≤ I

Tactic:
exact ⟨n, by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsConnected J
X✝ Y✝ : C
f : (const J).obj X✝ ⟶ (const J).obj Y✝
⊢ (const J).map (f.app (Classical.arbitrary J)) = f

Tactic:
by
    ext j
    apply nat_trans_from_is_connected f (Classical.arbitrary J) j

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
h : ((↑e).comp f).toRingHom = (↑e).comp f.toRingHom
h1 : ↑e.toRingEquiv = (↑e).toRingHom
⊢ (↑e).comp f.toRingHom = (↑e.toRingEquiv).comp f.toRingHom

Tactic:
h1

Goal state after:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
h : ((↑e).comp f).toRingHom = (↑e).comp f.toRingHom
h1 : ↑e.toRingEquiv = (↑e).toRingHom
⊢ (↑e).comp f.toRingHom = (↑e).comp f.toRingHom
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
F : C ⥤ D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P
  exact ⟨Q.strictMap F, inferInstance, (map_monotone h₂ F).trans (by simp)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (F.map (Groupoid.inv ↑f))) q.snd =
    (ConcreteCategory.hom (F.map (Groupoid.inv ↑f))) ((ConcreteCategory.hom (F.map ↑f)) p.snd)

Tactic:
rw [f.2]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
⊢ (F.map (G.map (StructuredArrow.Hom.right g))).toFunctor.obj ((F.map X✝.hom).toFunctor.obj f) =
    (F.map Y✝.hom).toFunctor.obj f

Tactic:
rw [← StructuredArrow.w g, map_comp, Cat.Hom.comp_obj]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
g₁ g₂ : Z ⟶ X
e : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
obtain ⟨l', rfl, rfl⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit _ _ e

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f
⊢ l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₁ =
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₂

Tactic:
by
  ext
  · simp only [Category.assoc, pullback_diagonal_map_snd_fst_fst,
      pullback_diagonal_map_snd_snd_fst]
  · simp only [Category.assoc, condition]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫
      snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) =
    fst f g

Tactic:
Iso.inv_comp_eq

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫
      snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) =
    snd f g

Tactic:
Iso.inv_comp_eq

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) =
    (pullbackDiagonalMapIdIso f g i).hom ≫ snd f g
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
⊢ ∀ (X₁ X₂ : J ⥤ C) (c₁ : Cone X₁) (c₂ : Cone X₂) (x : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ

Tactic:
intro X₁

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
X₁ : J ⥤ C
⊢ ∀ (X₂ : J ⥤ C) (c₁ : Cone X₁) (c₂ : Cone X₂) (x : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
⊢ ∀ (X₁ X₂ : J ⥤ C) (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₁ : IsColimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ

Tactic:
intro X₁

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
X₁ : J ⥤ C
⊢ ∀ (X₂ : J ⥤ C) (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₁ : IsColimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ ∃ J, W.colimitsOfShape (Discrete J) f

Tactic:
refine ⟨Shrink J, ?_⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ W.colimitsOfShape (Discrete (Shrink.{w, w'} J)) f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

Tactic:
intro X₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ : C
⊢ ∀ ⦃Y : C⦄ (f : X₁ ⟶ Y), W f → W.colimitsOfShape (Discrete PUnit.{w + 1}) f