mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ localized₀ p f (I • M') ≤ I • localized₀ p f M'

pp: case a
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ I • localized₀ p f M' ≤ localized₀ p f (I • M')

Tactic:
· rintro _ ⟨a, ha, s, rfl⟩
    refine Submodule.smul_induction_on ha ?_ ?_
    · intro r hr n hn
      rw [IsLocalizedModule.mk'_smul]
      exact Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩
    · simp +contextual only [IsLocalizedModule.mk'_add, add_mem, implies_true]

Goal state after:
case a
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ I • localized₀ p f M' ≤ localized₀ p f (I • M')
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
y : N ⧸ localized' S p f M'
⊢ ∃ x, x.2 • y = (Submodule.toLocalizedQuotient' S p f M') x.1

Tactic:
obtain ⟨y, rfl⟩ := mk_surjective _ y

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
y : N
⊢ ∃ x, x.2 • Submodule.Quotient.mk y = (Submodule.toLocalizedQuotient' S p f M') 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
y : M
s : ↥p
⊢ (Submodule.Quotient.mk y, s).2 • Submodule.Quotient.mk (Function.uncurry (mk' f) (y, s)) =
    (Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk y, s).1

Tactic:
simp only [Function.uncurry_apply_pair, toLocalizedQuotient'_mk, ← mk_smul, mk'_cancel']

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)

Tactic:
use n
    simp [← Ideal.map_pow]

Goal state after:
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)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : (t * s) • m = (t * 1) • a
⊢ ↑(t * s) ∈ I

Tactic:
apply ht ▸ smul_mem _ _ ha

Goal state after:
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)
m : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = 0
P : Ideal R
x✝ : P.IsMaximal
⊢ (f P) m = (f P) 0

Tactic:
h,

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)
m : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = 0
P : Ideal R
x✝ : P.IsMaximal
⊢ 0 = (f P) 0
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
J : Ideal S
⊢ Disjoint ↑M ↑(Ideal.under R J) ↔ J ≠ ⊤

Tactic:
rw [← iff_not_comm, Set.not_disjoint_iff]

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
J : Ideal S
⊢ J = ⊤ ↔ ∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: 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₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
h₂ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) ↔
    (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁)
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
simp only [IsScalarTower.algebraMap_apply R S T, map_mul, ← e₁, ← e₂, ← mul_assoc,
        mul_right_comm _ (algebraMap R S s₂),
        (IsLocalization.map_units S s₁).mul_left_inj,
        (IsLocalization.map_units S s₂).mul_left_inj] at this

Goal state after:
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₂
h₁ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
h₂ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) ↔
    (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁)
this :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) →
    ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
Module: Mathlib.RingTheory.Localization.AtPrime.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✝
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
h,

Goal state after:
case refine_1
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case h
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 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
h,

Goal state after:
case h
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 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case C_mul_T
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
s : R
⊢ r • (C s * T n) = C r * (C s * T n)

Tactic:
rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C,
      AddMonoidAlgebra.smul_single']

Goal state after:
case C_mul_T
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
s : R
⊢ AddMonoidAlgebra.single 0 (r * s) = C (r * s)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ f.degree = ⊥

Tactic:
h,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ degree 0 = ⊥
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 α
⊢ (Aᵀ * Aᵀ.adjugate)ᵀ = A.det • 1

Tactic:
rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ (C r * p + C r * q).smeval x = r • (p + q).smeval x

Tactic:
smeval_add,

Goal state after:
case add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ (C r * p).smeval x + (C r * q).smeval x = r • (p + q).smeval x
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ (C r * p).smeval x + (C r * q).smeval x = r • (p + q).smeval x

Tactic:
smeval_add,

Goal state after:
case add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ (C r * p).smeval x + (C r * q).smeval x = r • (p.smeval x + q.smeval x)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
h : A = C * B
⊢ ⅟C * A = B

Tactic:
h,

Goal state after:
case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
h : A = C * B
⊢ ⅟C * (C * B) = B
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ ⅟C * A = B ↔ A = C * B

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← h, Matrix.mul_invOf_cancel_left]
  · rw [h, Matrix.invOf_mul_cancel_left]

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

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
h : A = B * C
⊢ A * ⅟C = B

Tactic:
h,

Goal state after:
case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
h : A = B * C
⊢ B * C * ⅟C = B
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ∀ k ≤ r, ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
intro k

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ k ≤ r → ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
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 α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A'.det = ∑ j, A' (e i) j * A'.adjugate j (e i)
⊢ A.det = ∑ j, A i j * A.adjugate j i

Tactic:
simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
      Equiv.symm_apply_apply] at this

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A.det = ∑ x, A i x * A.adjugate x i
⊢ A.det = ∑ j, A i j * A.adjugate j i
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 α
h : B * A = 1
⊢ (B * A).det = 1

Tactic:
h,

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 α
h : B * A = 1
⊢ det 1 = 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 α
h : A * B = 1
⊢ (A * B).det = 1

Tactic:
h,

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 α
h : A * B = 1
⊢ det 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
intro k

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ k ≤ r → (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix n m α
h : B = A * C
⊢ A⁻¹ * B = C

Tactic:
h,

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix n m α
h : B = A * C
⊢ A⁻¹ * (A * C) = C
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix m n α
h : B = C * A
⊢ B * A⁻¹ = C

Tactic:
h,

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix m n α
h : B = C * A
⊢ C * A * A⁻¹ = C
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v ↦ v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows i ᵥ* A) j = 1 i j

Tactic:
one_eq_pi_single,

Goal state after:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v ↦ v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows i ᵥ* A) j = Pi.single i 1 j
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
⊢ Function.Surjective A.mulVec ↔ ∃ B, A * B = 1

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩

Goal state after:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
⊢ ∃ B, A * B = 1