mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (fun q ↦ q.IsPrime ∧ ⊥ ≤ q) = Ideal.IsPrime

Tactic:
by simp

Goal state after:
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'' M' : Submodule R M
N' : Submodule S N
h : localized' S p f M' ≤ N'
m : M
hm : m ∈ M'
⊢ IsLocalizedModule.mk' f m 1 = f m

Tactic:
by simp

Goal state after:
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
a✝ b✝ : R
ha : a✝ ∈ {r | r • S ⊆ ↑N}
hb : b✝ ∈ {r | r • S ⊆ ↑N}
⊢ ↑N + ↑N = ↑N

Tactic:
by simp

Goal state after:
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
⊢ 0 ⊆ ↑N

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
⊢ I = ⊤

Tactic:
by_contra hI
  obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes hI
  exact Set.notMem_empty p (h ▸ hp)

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid 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
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r 1 = (algebraMap R S) r

Tactic:
by simp

Goal state after:
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
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' f x 1 = f x

Tactic:
by simp

Goal state after:
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' : Submodule R M
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' f x 1 = f x

Tactic:
by simp

Goal state after:
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
x : R
s✝ : ↥M
x✝ : ∃ s ∈ M, s * x ∈ I
s : R
hs : s ∈ M
h : s * x ∈ I
⊢ ↑(1 * (⟨s * x, h⟩, ⟨s, hs⟩).2) * x = ↑1 * ↑(⟨s * x, h⟩, ⟨s, hs⟩).1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: 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
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
a : M
b c : ↥p
hc : c • g a = 0
⊢ mk' f (c • a) (c * b) = Function.uncurry (mk' f) (a, b)

Tactic:
by simp

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)
N₁ N₂ : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized₀ P.primeCompl (f P) N₁ ≤ localized₀ P.primeCompl (f P) N₂
m : M
hm : m ∈ N₁
P : Ideal R
hP : P.IsMaximal
⊢ IsLocalizedModule.mk' (f P) m 1 = (f P) m

Tactic:
by simp

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
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
N P : Submodule R M
h : ∀ (r : ↑s), localized₀ (Submonoid.powers ↑r) (f r) N ≤ localized₀ (Submonoid.powers ↑r) (f r) P
m : M
hm : m ∈ N
r : ↑s
⊢ mk' (f r) m 1 = (f r) m

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A✝ : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A✝
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A✝
inst✝² : IsScalarTower R S A✝
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
⊢ (polyEquivTensor R A).toFun ((algebraMap A A[X]) a) = (algebraMap A (A ⊗[R] R[X])) a

Tactic:
by simp

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

Goal state before:
pp: R : Type u_5
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_6
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
x✝ : R[X]
⊢ ↑(polyEquivTensor' R A).symm (1 ⊗ₜ[R] x✝) = (IsScalarTower.toAlgHom R R[X] A[X]).toLinearMap x✝

Tactic:
by simp

Goal state after:
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
I : Ideal R
⊢ RingHom.ker (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ≤
    Ideal.map (algebraMap R S) (RingHom.ker (Ideal.Quotient.mk I))

Tactic:
by simp

Goal state after:
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 : M ⊗[R] N
hx : x ∈ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range
⊢ x ∈ (map m.mkQ n.mkQ).ker

Tactic:
rw [Submodule.mem_sup] at hx

Goal state after:
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 : M ⊗[R] N
hx : ∃ y ∈ (map m.subtype LinearMap.id).range, ∃ z ∈ (map LinearMap.id n.subtype).range, y + z = x
⊢ x ∈ (map m.mkQ n.mkQ).ker
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case hr
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
a : ↥m ⊗[R] N
b : M ⊗[R] ↥n
f : ↥m ⊗[R] N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : M ⊗[R] ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
x : M
y : ↥n
⊢ ((AlgebraTensorModule.curry (f.coprod g ∘ₗ LinearMap.inr R (↥m ⊗[R] N) (M ⊗[R] ↥n))) x) y =
    ((AlgebraTensorModule.curry (0 ∘ₗ LinearMap.inr R (↥m ⊗[R] N) (M ⊗[R] ↥n))) x) y

Tactic:
simp [g, Submodule.Quotient.mk_eq_zero _ |>.2 y.2]

Goal state after:
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
I : Ideal R
⊢ ((↑(TensorProduct.lid R M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
        ↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv)).range =
    Submodule.map₂ (LinearMap.lsmul R M) I ⊤

Tactic:
map₂_eq_range_lift_comp_mapIncl

Goal state after:
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
I : Ideal R
⊢ ((↑(TensorProduct.lid R M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
        ↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv)).range =
    (lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤).range
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
I : Ideal R
x✝¹ : ↥I
x✝ : ↥⊤
⊢ ((↑(TensorProduct.lid R M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
        ↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv))
      (x✝¹ ⊗ₜ[R] x✝) =
    (lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤) (x✝¹ ⊗ₜ[R] x✝)

Tactic:
by simp

Goal state after:
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
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
⊢ I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)

Tactic:
by simp

Goal state after:
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✝ : Type u_3
inst✝¹ : CommSemiring P✝
I : Ideal R
hI : I.IsPrime
P : Ideal S
inst✝ : P.IsPrime
s : Subalgebra R S
⊢ P.primeCompl ⊓ s.toSubmonoid ≤ s.toSubmonoid

Tactic:
by simp

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

Goal state before:
pp: case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝⁵ : a ∈ s
b : S
a✝⁴ : b ∈ s
a✝³ : b ∉ P
c : S
a✝² : c ∈ s
d : S
a✝¹ : d ∈ s
a✝ : d ∉ P
x : S
⊢ x ∉ P → x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
hxP

Goal state after:
case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝⁵ : a ∈ s
b : S
a✝⁴ : b ∈ s
a✝³ : b ∉ P
c : S
a✝² : c ∈ s
d : S
a✝¹ : d ∈ s
a✝ : d ∉ P
x : S
hxP : x ∉ P
⊢ x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
x✝¹ : M
x✝ : N
⊢ ((curry (F ∘ₗ mapOfCompatibleSMul A R A M N)) x✝¹) x✝ = ((curry S.mkQ) x✝¹) x✝

Tactic:
simp [S, F]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ under R (map (algebraMap R S) p) = p

Tactic:
by
  have disj : Disjoint (q.primeCompl : Set R) p := by
    simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]
  exact IsLocalization.under_map_of_isPrime_disjoint _ _ (by simpa) disj

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : (under R ⊤).IsMaximal
⊢ under R ⊤ = ⊤

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
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ₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
h : x✝ ∈ p ^ n
⊢ 1 ∈ p.primeCompl

Tactic:
by simp

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
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ 0 * 1 ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul S A
ι : Type u_4
v : ι → S
⊢ Set.InjOn ⇑(IsScalarTower.toAlgHom R S A).toLinearMap ↑(Submodule.span R (Set.range v))

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul S A
s : Set S
⊢ Set.InjOn (⇑(algebraMap S A)) s

Tactic:
by simp

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

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective ⇑f
this : Algebra R S := f.toAlgebra
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid R

Tactic:
by simp

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 : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝ : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ IsUnit (f 1)

Tactic:
by simp

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 : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝ : Algebra S R := e.symm.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ IsUnit (f 1)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ toLaurent (Polynomial.C a * X ^ n) = C a * T (Int.ofNat n) * T ↑0

Tactic:
by simp

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 α
A : Matrix n n α
b : n → α
i : n
⊢ (Aᵀ.updateCol i b).det = (A.updateRow i b).det

Tactic:
updateCol_transpose,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
⊢ (A.updateRow i b)ᵀ.det = (A.updateRow i b).det
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ (Aᵀ.updateCol j (A i)).det = 0

Tactic:
updateCol_transpose,

Goal state after:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ (A.updateRow j (A i))ᵀ.det = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j✝ j : n
⊢ Pi.single i 1 j = 1 j i

Tactic:
Matrix.one_eq_pi_single,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j✝ j : n
⊢ Pi.single i 1 j = Pi.single j 1 i
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ lift.{uM, max uM uR} (Module.rank R (LocalizedModule R⁰ M)) = lift.{max uR uM, uM} (Module.rank R M)

Tactic:
IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ lift.{max uM uR, uM} (Module.rank R M) = lift.{max uR uM, uM} (Module.rank R M)
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 j : n
⊢ (Aᵀ.updateCol j (Pi.single i 1)).det = (A.updateRow j (Pi.single i 1)).det

Tactic:
updateCol_transpose,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A.updateRow j (Pi.single i 1))ᵀ.det = (A.updateRow j (Pi.single i 1)).det
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ IsLocalization.mk' R[T;T⁻¹] p ⟨X ^ n, ⋯⟩ * (algebraMap R[X] R[T;T⁻¹]) (X ^ n) = toLaurent p

Tactic:
IsLocalization.mk'_spec,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (algebraMap R[X] R[T;T⁻¹]) p = toLaurent p
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (t : TransvectionStruct n R), Commute t.toMatrix M

Tactic:
refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : M ∈ Set.range ⇑(scalar n)
t : TransvectionStruct n R
⊢ Commute t.toMatrix M
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
t : TransvectionStruct n R
⊢ (sumInl p t).toMatrix = fromBlocks t.toMatrix 0 0 1

Tactic:
cases t

Goal state after:
case mk
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case MX
R : Type u_3
inst✝ : CommSemiring R
a✝¹ : Nontrivial R
p✝ : R[X]
hp : p✝ ≠ 0
a✝ : toLaurent p✝.reverse = invert (toLaurent p✝) * T ↑p✝.natDegree
⊢ toLaurent (p✝ * X).reverse = invert (toLaurent (p✝ * X)) * T ↑(p✝ * X).natDegree

Tactic:
simpa [natDegree_mul_X hp]

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 α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)

Tactic:
← pow_succ',

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det ^ (Fintype.card n - 1 + 1)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case cons
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ reindexEquiv e) L).prod = (reindexAlgEquiv R R e) (List.map toMatrix L).prod
⊢ (List.map (toMatrix ∘ reindexEquiv e) (t :: L)).prod = (reindexAlgEquiv R R e) (List.map toMatrix (t :: L)).prod

Tactic:
simp [toMatrix_reindexEquiv, IH]

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ (listTransvecCol M).length = r

Tactic:
by simp [listTransvecCol]

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ ∑ x, 1 x = ↑(Fintype.card n)

Tactic:
Pi.one_def,

Goal state after:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ ∑ x, 1 = ↑(Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: R : Type u_6
n : ℕ
inst✝ : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace

Tactic:
delta trace
  rw [← (finSuccEquiv n).symm.sum_comp]
  simp

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

Goal state before:
pp: R : Type u_1
m : Type u_10
n : Type u_11
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
refine (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_

Goal state after:
R : Type u_1
m : Type u_10
n : Type u_11
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (A.map fun a ↦ ((Algebra.lmul ℕ R).toLinearMap a) 1).det ^ Fintype.card n *
      (B.map fun b ↦ ((Algebra.lmul ℕ R).toLinearMap 1) b).det ^ Fintype.card m =
    A.det ^ Fintype.card n * B.det ^ Fintype.card m