mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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
x : ↥p
m n : N
e : 1 • (m - n) ∈ localized' S p f M'
⊢ Submodule.Quotient.mk m = Submodule.Quotient.mk n

Tactic:
one_smul,

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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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
x : ↥p
m n : N
e : m - n ∈ localized' S p f M'
⊢ Submodule.Quotient.mk m = Submodule.Quotient.mk n
Module: Mathlib.RingTheory.Localization.Ideal

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
I : Ideal R
z : S
⊢ map_ideal M S I = Ideal.map (algebraMap R S) I

Tactic:
map_ideal,

Goal state after:
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
I : Ideal R
z : S
⊢ Submodule.localized' S M (Algebra.linearMap R S) I = Ideal.map (algebraMap R S) I
Module: Mathlib.RingTheory.Localization.Ideal

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
I : Ideal R
z : S
⊢ z ∈ map_ideal M S I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

Tactic:
map_ideal,

Goal state after:
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
I : Ideal R
z : S
⊢ z ∈ Submodule.localized' S M (Algebra.linearMap R S) I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1
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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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
m n : M ⧸ M'
e : (Submodule.toLocalizedQuotient' S p f M') m = (Submodule.toLocalizedQuotient' S p f M') n
⊢ ∃ c, c • m = c • n

Tactic:
by
    obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
    obtain ⟨x, hx, s, hs⟩ : f (m - n) ∈ _ := by simpa [Submodule.Quotient.eq] using! e
    obtain ⟨c, hc⟩ := exists_of_eq (S := p) (show f (s • (m - n)) = f x by simp [-map_sub, ← hs])
    exact ⟨c * s, by simpa only [← Quotient.mk_smul, Submodule.Quotient.eq,
      ← smul_sub, mul_smul, hc] using! M'.smul_mem c hx⟩

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_1
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 ∈ τ, ∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
intro t ht

Goal state after:
case refine_1
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 τ
t : T
ht : t ∈ τ
⊢ ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
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 τ
⊢ ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
by
  refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht
  · intro t ht
    exact ⟨1, Subalgebra.one_mem _, isUnit_one,
      (one_smul S t).symm ▸ Algebra.mem_sup_right (Algebra.subset_adjoin ht)⟩
  · intro s
    obtain ⟨s', hs₁, hs₂, hs₃⟩ := hσ s
    refine ⟨_, hs₁, hs₂, Algebra.mem_sup_left ?_⟩
    rw [Algebra.smul_def, ← map_mul, mul_comm]
    exact ⟨_, hs₃, rfl⟩
  · rintro x y - - ⟨sx, hsx, hsx', hsx''⟩ ⟨sy, hsy, hsy', hsy''⟩
    refine ⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩
    rw [smul_add, mul_smul, mul_smul, Algebra.smul_def sx (sy • y), smul_comm,
      Algebra.smul_def sy (sx • x)]
    apply add_mem (mul_mem _ hsx'') (mul_mem _ hsy'') <;>
      exact Algebra.mem_sup_left ⟨_, ‹_›, rfl⟩
  · rintro x y - - ⟨sx, hsx, hsx', hsx''⟩ ⟨sy, hsy, hsy', hsy''⟩
    refine ⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩
    rw [mul_smul, ← smul_eq_mul, smul_comm sy x, ← smul_assoc, smul_eq_mul]
    exact mul_mem hsx'' hsy''

Goal state after:
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 : S
hx : coeSubmodule S I = R ∙ x
⊢ Submodule.IsPrincipal I

Tactic:
have x_mem : x ∈ coeSubmodule S I := hx.symm ▸ Submodule.mem_span_singleton_self x

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 : S
hx : coeSubmodule S I = R ∙ x
x_mem : x ∈ coeSubmodule S I
⊢ Submodule.IsPrincipal I
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_3
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    mk' S 1 (z * z') • (algebraMap R S) ↑z' • y + mk' S 1 (z * z') • (algebraMap R S) ↑z • y'

Tactic:
smul_smul,

Goal state after:
case mp.refine_3
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y + mk' S 1 (z * z') • (algebraMap R S) ↑z • y'
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.refine_3
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 y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ (algebraMap S T) t₁ * t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
exact mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) h₆

Goal state after:
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • (algebraMap R S) y' • y

Tactic:
smul_smul,

Goal state after:
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ (mk' S y' z' * mk' S 1 z) • y = mk' S 1 (z' * z) • (algebraMap R S) y' • y
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S (y' * 1) (z' * z) • y = mk' S 1 (z' * z) • (algebraMap R S) y' • y

Tactic:
smul_smul,

Goal state after:
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S (y' * 1) (z' * z) • y = (mk' S 1 (z' * z) * (algebraMap R S) y') • y
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.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = Ideal.map f ⊤
⊢ P f

Tactic:
Ideal.map_top

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
⊢ P f
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : β • α • x ∈ pS
⊢ x ∈ pS

Tactic:
smul_smul,

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : (β * α) • x ∈ pS
⊢ x ∈ pS
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : sign g = -1
⊢ (-(1 • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i)).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree

Tactic:
one_smul,

Goal state after:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : sign g = -1
⊢ (-∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[T;T⁻¹]
h : ∀ (a : ℤ), p.coeff a = q.coeff a
⊢ p = q

Tactic:
by ext; exact h _

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

Goal state before:
pp: case h.refine_2
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ (algebraMap S Sₚ) (α • β • x) - (algebraMap S Sₚ) x = (algebraMap S Sₚ) (γ • x)

Tactic:
smul_smul,

Goal state after:
case h.refine_2
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ (algebraMap S Sₚ) ((α * β) • x) - (algebraMap S Sₚ) x = (algebraMap S Sₚ) (γ • x)
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case h.refine_2
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ (algebraMap S Sₚ) (1 • x + γ • x - x) = (algebraMap S Sₚ) (γ • x)

Tactic:
one_smul,

Goal state after:
case h.refine_2
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ (algebraMap S Sₚ) (x + γ • x - x) = (algebraMap S Sₚ) (γ • x)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ ∀ (a : ℤ) (s : Finset ℤ), a ∉ s → M (∑ n ∈ s, C (p.coeff n) * T n) → M (∑ n ∈ insert a s, C (p.coeff n) * T n)

Tactic:
intro n s ns ih
      rw [Finset.sum_insert ns]
      exact h_add A ih

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
⊢ A.adjugate = 1

Tactic:
by
  ext i j
  simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i, one_apply]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ ↑x⁻¹ ^ m = ↑(x ^ m)⁻¹

Tactic:
← inv_pow,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ ↑x⁻¹ ^ m = ↑(x⁻¹ ^ m)
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : CommMagma R
A : Matrix m n R
B : Matrix n m R
⊢ (A * B).trace = (B * A).trace

Tactic:
← trace_transpose,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : CommMagma R
A : Matrix m n R
B : Matrix n m R
⊢ (A * B)ᵀ.trace = (B * A).trace
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (A * B).det • 1 = B.det • A.det • 1

Tactic:
smul_smul,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (A * B).det • 1 = (B.det * A.det) • 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A.det
⊢ ⅟A.det • A.det • 1 = 1

Tactic:
smul_smul,

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A.det
⊢ (⅟A.det * A.det) • 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
this : A.det • 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Tactic:
Matrix.smul_mul,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
this : A.det • (1 * A.adjugate.adjugate) = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A