mathlib-initiative/mathlib-tactics huggingface dataset:
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[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 1) = (monomial n) a

pp: case refine_2.hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 0) = 0

Tactic:
<;>

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[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 1) = (monomial n) a

case refine_2.hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 0) = 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)
z : S'
⊢ ∃ x, z * (algebraMap R' S') ↑x.2 = (algebraMap R' S') x.1

Tactic:
obtain ⟨z, rfl⟩ := hg z

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)
z : S
⊢ ∃ x, g z * (algebraMap R' S') ↑x.2 = (algebraMap R' S') x.1
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)
⊢ ∀ (z : S'), ∃ x, z * (algebraMap R' S') ↑x.2 = (algebraMap R' S') x.1

Tactic:
intro z
    obtain ⟨z, rfl⟩ := hg z
    obtain ⟨⟨r, s⟩, e⟩ := IsLocalization.surj M z
    refine ⟨⟨f r, _, s.1, s.2, rfl⟩, ?_⟩
    simpa only [map_mul, ← RingHom.comp_apply, H] using DFunLike.congr_arg g e

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑a * (y₁ * ↑s₂)

pp: case e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₂ * ↑s₁)) = ↑a * (y₂ * ↑s₁)

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑a * (y₁ * ↑s₂)

case e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₂ * ↑s₁)) = ↑a * (y₂ * ↑s₁)
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 ≠ 0

Tactic:
intro hx'

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
hx' : x = 0
⊢ False
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S →
    ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ (∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ) →
    IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S →
    ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ (∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ) →
    IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S → ∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S) → EssFiniteType R S

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S → ∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S) → EssFiniteType R S
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x : N
hx : x ∈ n
⊢ x ∈ ((mk R M N).flip.compr₂ ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ).ker

Tactic:
ext y
      simp only [LinearMap.compr₂_apply, LinearMap.flip_apply, mk_apply, Submodule.mkQ_apply,
        LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]
      exact Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (algebraMap S T) sy ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

pp: 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (algebraMap S T) sx ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
<;>

Goal state after:
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (algebraMap S T) sy ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (algebraMap S T) sx ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
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
⊢ (coeSubmodule S I).IsPrincipal → Submodule.IsPrincipal I

pp: case mpr
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
⊢ Submodule.IsPrincipal I → (coeSubmodule S I).IsPrincipal

Tactic:
<;>

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
⊢ (coeSubmodule S I).IsPrincipal → Submodule.IsPrincipal I

case mpr
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
⊢ Submodule.IsPrincipal I → (coeSubmodule S I).IsPrincipal
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
y : B ⧸ Ideal.map (algebraMap A B) I
u : B
⊢ (quotIdealMapEquivTensorQuotAux B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) u * y) =
    (quotIdealMapEquivTensorQuotAux B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) u) *
      (quotIdealMapEquivTensorQuotAux B I) y

Tactic:
obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective y

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
u v : B
⊢ (quotIdealMapEquivTensorQuotAux B I)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) u * (Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) v) =
    (quotIdealMapEquivTensorQuotAux B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) u) *
      (quotIdealMapEquivTensorQuotAux B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) v)
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_4
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (a_1 : S),
    ∀ x ∈ Submodule.span S a,
      (∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Submodule.span R a, ∃ z, a_1 • x = mk' S 1 z • y

Tactic:
rintro a _ _ ⟨y, hy, z, rfl⟩
      obtain ⟨y', z', rfl⟩ := exists_mk'_eq M a
      refine ⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, ?_⟩
      rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_mul]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty (OreSet S) → ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx : ∀ (i : Ideal R) (i_1 : i.IsPrime), I ≤ i → (algebraMap R (Localization.AtPrime i)) x = 0
hle : I ≤ m
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx : ∀ (i : Ideal R) (i_1 : i.IsPrime), I ≤ i → (algebraMap R (Localization.AtPrime i)) x = 0
hle : ¬I ≤ m
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I

Tactic:
· simp [hx _ _ hle]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx : ∀ (i : Ideal R) (i_1 : i.IsPrime), I ≤ i → (algebraMap R (Localization.AtPrime i)) x = 0
hle : ¬I ≤ m
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (X • A.map ⇑C + B.map ⇑C).det.natDegree ≤ Fintype.card n

Tactic:
det_apply

Goal state after:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (∑ σ, sign σ • ∏ i, (X • A.map ⇑C + B.map ⇑C) (σ i) i).natDegree ≤ Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∑ b, (sign b • ∏ i, (X • A.map ⇑C + B.map ⇑C) (b i) i).coeff 0 = B.det

Tactic:
det_apply

Goal state after:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∑ b, (sign b • ∏ i, (X • A.map ⇑C + B.map ⇑C) (b i) i).coeff 0 = ∑ σ, sign σ • ∏ i, B (σ i) i
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case e'_3.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ p ∈ Finset.univ, ((X • A.map ⇑C + B.map ⇑C) (g p) p).natDegree ≤ 1

Tactic:
· rintro p -
    dsimp only [Matrix.add_apply, Matrix.smul_apply, map_apply, smul_eq_mul]
    compute_degree

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

pp: case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uN, uM} (Module.rank R M) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)

Tactic:
<;>

Goal state after:
case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uN, uM} (Module.rank R M) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ⨆ i, Cardinal.lift.{uM, uN} #↑↑i ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

pp: case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ⨆ i, Cardinal.lift.{uN, uM} #↑↑i ≤ Cardinal.lift.{uM, uN} (Module.rank R N)

Tactic:
<;>

Goal state after:
case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ⨆ i, Cardinal.lift.{uM, uN} #↑↑i ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ⨆ i, Cardinal.lift.{uN, uM} #↑↑i ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), Cardinal.lift.{uM, uN} #↑↑i ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

pp: case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), Cardinal.lift.{uN, uM} #↑↑i ≤ Cardinal.lift.{uM, uN} (Module.rank R N)

Tactic:
<;>

Goal state after:
case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), Cardinal.lift.{uM, uN} #↑↑i ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), Cardinal.lift.{uN, uM} #↑↑i ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank S N ≤ Module.rank R N

pp: case a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R N ≤ Module.rank S N

Tactic:
<;>

Goal state after:
case inr.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank S N ≤ Module.rank R N

case a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R N ≤ Module.rank S N
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
a : R
⊢ motive (C a)

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
⊢ ∀ (n : ℕ) (a : R), motive (C a * T ↑n) → motive (C a * T (↑n + 1))

pp: case refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
⊢ ∀ (n : ℕ) (a : R), motive (C a * T (-↑n)) → motive (C a * T (-↑n - 1))

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
a : R
⊢ motive (C a)

case refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
⊢ ∀ (n : ℕ) (a : R), motive (C a * T ↑n) → motive (C a * T (↑n + 1))

case refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
⊢ ∀ (n : ℕ) (a : R), motive (C a * T (-↑n)) → motive (C a * T (-↑n - 1))