mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    (ConcreteCategory.hom (D.φ₁ ≫ D.v₂₃.τ₁)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁

Tactic:
ConcreteCategory.comp_apply,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ)
      ((ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)) =
    (ConcreteCategory.hom (D.φ₁ ≫ D.v₂₃.τ₁)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃ ≫ D.v₁₂.τ₂)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    (ConcreteCategory.hom D.L₂.f) x₁

Tactic:
ConcreteCategory.comp_apply,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.v₁₂.τ₂)
      ((ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)) =
    (ConcreteCategory.hom D.L₂.f) x₁
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
⊢ F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i i ⋯ hj'

Tactic:
F.map'_self i,

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
⊢ 𝟙 (F.obj ⟨i, ⋯⟩) ≫ app ⟨i, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i i ⋯ hj'
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4
h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5
i : Fin (1 + 1)
⊢ φ.app i = φ'.app i

Tactic:
match i with
    | 0 => exact h₀
    | 1 => exact h₁

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
⊢ f = g

Tactic:
apply hK.hom_ext
  rintro (_ | _) <;> simp [h]

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
exact ⟨StructuredArrow.mk (Y := zero) (𝟙 _)⟩

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑N.subtype

Tactic:
exact Subtype.val_injective

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
intro x

Goal state after:
case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x : R
⊢ ∀ {y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N✝ N₁ N₂ : Submodule R M
S✝ S₁ S₂ : Set M
N : Submodule R M
S : Set M
r : R
⊢ ∀ {x : R}, (∀ ⦃b : M⦄, b ∈ S → x • b ∈ ↑N) → ∀ ⦃b : M⦄, b ∈ S → r • x • b ∈ ↑N

Tactic:
intro x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N✝ N₁ N₂ : Submodule R M
S✝ S₁ S₂ : Set M
N : Submodule R M
S : Set M
r x : R
⊢ (∀ ⦃b : M⦄, b ∈ S → x • b ∈ ↑N) → ∀ ⦃b : M⦄, b ∈ S → r • x • b ∈ ↑N
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ ↑s • IsLocalizedModule.mk' f m s ∈ N'

Tactic:
← algebraMap_smul S

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ (algebraMap R S) ↑s • IsLocalizedModule.mk' f m s ∈ N'
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes ≤ sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
intro x

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ x ∈ sInf I.minimalPrimes → x ∈ sInf {J | I ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) (f ^ k) = 0 ↔ f ^ k = 0

Tactic:
exact (toMatrix b b).map_eq_zero_iff

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ (f.restrict hf ^ n) m = 0 m

Tactic:
simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ ⟨0, ⋯⟩ = 0
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp.refine_2
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
J : Ideal S
h : J.IsPrime
⊢ ∀ {x y : R}, x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J

Tactic:
intro x

Goal state after:
case mp.refine_2
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
J : Ideal S
h : J.IsPrime
x : R
⊢ ∀ {y : R}, x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr.refine_2
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
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
intro x

Goal state after:
case mpr.refine_2
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
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x : S
⊢ ∀ {y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
⊢ ∀ (y : M), y = 0

Tactic:
intro x

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
x : M
⊢ x = 0
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I

Tactic:
intro x

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
⊢ x ∈ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) → x ∈ I
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) ((toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p

Tactic:
rw [toFunAlgHom_apply_tmul, eval₂_sum]

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) ((monomial n) (a * (algebraMap R A) a_1))) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) ((monomial n) (a * (algebraMap R A) a_1))) = a ⊗ₜ[R] p

Tactic:
eval₂_monomial,

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ ↑includeLeft (a * (algebraMap R A) a_1) * 1 ⊗ₜ[R] X ^ n) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : Rₚ
⊢ (algebraMap Rₚ Sₚ) x = 0 → x = 0
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
⊢ ∀ {x y : R'}, (algebraMap R' S') x = (algebraMap R' S') y → ∃ c, ↑c * x = ↑c * y

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x : R'
⊢ ∀ {y : R'}, (algebraMap R' S') x = (algebraMap R' S') y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

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
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
⊢ ∀ (x : S), IsUnit x → x ∈ p.primeCompl

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
x : S
⊢ IsUnit x → x ∈ p.primeCompl
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

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
N : Submonoid S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
x : Ideal R
H : x.IsPrime
inst✝ : IsDomain R
a : R
ha : a ∈ x.primeCompl
⊢ a ∈ nonZeroDivisors R

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
x : Ideal R
H : x.IsPrime
inst✝ : IsDomain R
a : R
ha : a ∈ x.primeCompl
⊢ a ≠ 0
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
⊢ M ≤ nonZeroDivisors R

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
⊢ x ∈ M → x ∈ nonZeroDivisors R
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ∈ nonZeroDivisors R

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ≠ 0
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ↑⟨x, hx⟩ * 1 = 0

Tactic:
simp [hx']

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ {x y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
intro x

Goal state after:
case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x : ↥(adjoin R ↑σ)
⊢ ∀ {y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this : Nontrivial S := nontrivial S P
⊢ ∀ (a b : S), a ∈ nonunits S → b ∈ nonunits S → a + b ∈ nonunits S

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this : Nontrivial S := nontrivial S P
x : S
⊢ ∀ (b : S), x ∈ nonunits S → b ∈ nonunits S → x + b ∈ nonunits S
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
⊢ ∀ (s_1 : T),
    ∃ t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t,
      IsUnit t_1 ∧ s_1 * t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
intro x

Goal state after:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x : T
⊢ ∃ t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t,
    IsUnit t_1 ∧ x * t_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = R ∙ (algebraMap R S) x
x_mem : (algebraMap R S) x ∈ coeSubmodule S I
⊢ R ∙ (algebraMap R S) x = coeSubmodule S (Ideal.span {x})

Tactic:
coeSubmodule_span_singleton

Goal state after:
case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = R ∙ (algebraMap R S) x
x_mem : (algebraMap R S) x ∈ coeSubmodule S I
⊢ R ∙ (algebraMap R S) x = R ∙ (algebraMap R S) x