mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
⊢ HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g) = g

Tactic:
let m1 : Module R S := Module.compHom S f

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
⊢ HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g) = g
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
r : R
x : ↑X
⊢ 1 ⊗ₜ[R] (r • x) = (RingHom.id R) r • 1 ⊗ₜ[R] x

Tactic:
let m1 : Module R S := Module.compHom S f

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ 1 ⊗ₜ[R] (r • x) = (RingHom.id R) r • 1 ⊗ₜ[R] x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
s : S
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • z) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        z

Tactic:
let m1 : Module R S := Module.compHom S f

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
s : S
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
m1 : Module R S := Module.compHom S f
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • z) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        z
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
⊢ (restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f = Counit.map f ≫ (𝟭 (ModuleCat S)).map g

Tactic:
let m1 : Module R S := Module.compHom S f

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
⊢ (restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f = Counit.map f ≫ (𝟭 (ModuleCat S)).map g
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq]

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
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b = count (normalize a) (normalizedFactors b)

Tactic:
have := emultiplicity_eq_count_normalizedFactors ha hb
  rwa [(finiteMultiplicity_of_emultiplicity_eq_natCast this).emultiplicity_eq_multiplicity,
    ENat.natCast_inj] at this

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

Goal state before:
pp: case e'_2.e'_3
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ p = normalize p

pp: case e'_3
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ ↑n = emultiplicity p x

Tactic:
· exact hnorm.symm

Goal state after:
case e'_3
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ ↑n = emultiplicity p x
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
⊢ IsUnit ((algebraMap R T) (y * x))

pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
⊢ ∃ n a, z * (algebraMap R T) (y * x) ^ n = (algebraMap R T) a

pp: case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap R T) a = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
· simp only [map_mul, IsUnit.mul_iff, IsScalarTower.algebraMap_apply R S T]
    exact ⟨algebraMap_isUnit _, IsUnit.map _ (algebraMap_isUnit x)⟩

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
⊢ ∃ n a, z * (algebraMap R T) (y * x) ^ n = (algebraMap R T) a

case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap R T) a = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
this : (AddMonoidHom.mulLeft x) y ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
⊢ x * y ∈ closure s

Tactic:
refine closure_mono ?_ this

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
this : (AddMonoidHom.mulLeft x) y ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
⊢ ⇑(AddMonoidHom.mulLeft x) '' s ⊆ s
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
y x : R
hy : y ∈ closure s
this : (AddMonoidHom.mulRight x) y ∈ closure (⇑(AddMonoidHom.mulRight x) '' s)
⊢ y * x ∈ closure s

Tactic:
refine closure_mono ?_ this

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
y x : R
hy : y ∈ closure s
this : (AddMonoidHom.mulRight x) y ∈ closure (⇑(AddMonoidHom.mulRight x) '' s)
⊢ ⇑(AddMonoidHom.mulRight x) '' s ⊆ s
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ jacobson R M
⊢ comap f (jacobson R₂ M₂) = jacobson R M

Tactic:
← map_jacobson_of_ker_le surj le,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ jacobson R M
⊢ comap f (map f (jacobson R M)) = jacobson R M
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ f.ker ≤ Module.jacobson R (R ⧸ I)

Tactic:
· rintro _ rfl; exact zero_mem _

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsMaximal} = sInf {m | IsCoatom m}

Tactic:
bot_le,

Goal state after:
R : Type u
inst✝ : Ring R
⊢ sInf {J | True ∧ J.IsMaximal} = sInf {m | IsCoatom m}
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
⊢ IsUnit r

Tactic:
obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r h

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial I
this : IsIso (f ≫ hI.to (⊥_ C))
⊢ f ≫ hI.to (⊥_ C) ≫ inv (f ≫ hI.to (⊥_ C)) = 𝟙 A

Tactic:
rw [← assoc, IsIso.hom_inv_id]

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✝⁴ : SymmetricCategory C
M N W X Y Z : C
inst✝³ : MonObj M
inst✝² : MonObj N
inst✝¹ : IsCommMonObj M
inst✝ : IsCommMonObj N
⊢ (β_ (M ⊗ N) (M ⊗ N)).hom ≫ μ = μ

Tactic:
by
    simp [← IsIso.inv_comp_eq, tensorμ, ← associator_inv_naturality_left_assoc,
      ← associator_naturality_right_assoc, SymmetricCategory.braiding_swap_eq_inv_braiding M N,
      ← tensorHom_def_assoc, -whiskerRight_tensor, -tensor_whiskerLeft, MonObj.tensorObj.mul_def,
      ← MonoidalCategory.whiskerLeft_comp_assoc, -MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: case uniq.h₀
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
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst = s.ι

Tactic:
exact H.isLimit.fac _ _

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

Goal state before:
pp: case uniq.h₁
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
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd = s.ι

Tactic:
exact H.isLimit.fac _ _

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

Goal state before:
pp: case desc
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') → (Cofork.ofπ g ⋯).pt ⟶ s.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 : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ ?desc s = 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 : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt), (Cofork.ofπ g ⋯).π ≫ m = s.π → m = ?desc s

Tactic:
· exact fun s => H.isColimit.desc (PushoutCocone.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 : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

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.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
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Away r A
⊢ Away ((algebraMap R S) r) (S ⊗[R] A)

Tactic:
by
  simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]
  infer_instance

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
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Away r A
⊢ Away ((algebraMap R S) r) (A ⊗[R] S)

Tactic:
by
  simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
this : ∃ n, X = ↑n
⊢ p ∈ s

Tactic:
exfalso

Goal state after:
case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
this : ∃ n, X = ↑n
⊢ False
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)

pp: case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom = ofHom (algebraMap R B) ≫ ?inr

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

Goal state after:
case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ ∃ u, u • b' • a = u • b • a'

Tactic:
← IsLocalizedModule.eq_iff_exists S f,

Goal state after:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ f (b' • a) = f (b • a')
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
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ ∃ u, u • b • ⋯.choose.1 = u • ⋯.choose.2 • a

Tactic:
← IsLocalizedModule.eq_iff_exists S f,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ f (b • ⋯.choose.1) = f (⋯.choose.2 • a)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ (algebraMap R S') m * f x = (algebraMap R S') m * 0

Tactic:
by
        rw [← Algebra.smul_def]
        simpa [Submonoid.smul_def] using f.congr_arg e

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.isoClosure.unop = P.unop.isoClosure

Tactic:
rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]

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:
intro j₁ j₂

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
⊢ r j₁ j₂
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ ∀ (j₁ j₂ : J), Zigzag j₁ j₂

Tactic:
intro j₁ j₂

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
⊢ Zigzag j₁ j₂
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
X : C
hX : X ∈ Set.range (Subtype.val ∘ φ)
⊢ P X

Tactic:
simp only [Set.mem_range, Function.comp_apply, Subtype.exists] at hX

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
X : C
hX : ∃ a, ∃ (b : P' a), ↑(φ ⟨a, b⟩) = X
⊢ P X
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A → ∃ n I x, I.FG

Tactic:
rintro ⟨n, f, hf⟩

Goal state after:
case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ n I x, I.FG
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1.inr
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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := ⋯
AX : Type (max w₂ 0) := ⋯
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := ⋯
s₀✝ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⋯
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid

Tactic:
exact ⟨X i, map_X _ _⟩

Goal state after: