mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
h : ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0
⊢ ∀ ⦃x : A⦄, x ∈ s → f (commonDenomOfFinset M s • x) = 0

Tactic:
]

Goal state after:
R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
h : ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0
⊢ ∀ ⦃x : A⦄, x ∈ s → f (commonDenomOfFinset M s • x) = 0
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
h : ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0
inj : Function.Injective fun s_1 ↦ commonDenomOfFinset M s • s_1
⊢ ∑ x ∈ s, commonDenomOfFinset M s • f (commonDenomOfFinset M s • x) • id x =
    ∑ x ∈ s, f (commonDenomOfFinset M s • x) • id (commonDenomOfFinset M s • x)

Tactic:
]

Goal state after:
R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
h : ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0
inj : Function.Injective fun s_1 ↦ commonDenomOfFinset M s • s_1
⊢ ∑ x ∈ s, commonDenomOfFinset M s • f (commonDenomOfFinset M s • x) • id x =
    ∑ x ∈ s, f (commonDenomOfFinset M s • x) • id (commonDenomOfFinset M s • x)
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.updateRow i b).det = (A.updateRow i b).det

Tactic:
]

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 α
i j : n
⊢ (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0
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.updateRow j (A i)).det = 0

Tactic:
]

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: 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 i = A i

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (toLaurent f' * T (-↑n))

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (toLaurent f' * T (-↑n))
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
h : ∀ (j : n), b j = A j i
⊢ Aᵀᵀ.cramer b = Pi.single i Aᵀ.det

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ Aᵀᵀ.cramer b = Pi.single i Aᵀ.det
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 j 1 i = Pi.single j 1 i

Tactic:
]

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 α
b : n → α
i : n
⊢ b i = b i

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support ⊆ {n}

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support ⊆ {n}
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support = {n}

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support = {n}
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 α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (A.updateCol i (∑ x ∈ s, fun j ↦ f j x)).det = A.cramer (fun j ↦ ∑ x ∈ s, f j x) i

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (A.updateCol i (∑ x ∈ s, fun j ↦ f j x)).det = A.cramer (fun j ↦ ∑ x ∈ s, f j x) 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.{max uM uR, uM} (Module.rank R M) = lift.{max uR uM, uM} (Module.rank R M)

Tactic:
]

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

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

Tactic:
]

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 α
i j : n
⊢ (A.updateRow j (Pi.single i 1)).det = (A.updateRow j (Pi.single i 1)).det

Tactic:
]

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 α
i j : n
⊢ (A.updateRow i (Pi.single j 1)).det = (A.updateCol j (Pi.single i 1)).det

Tactic:
]

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 i (Pi.single j 1)).det = (A.updateCol j (Pi.single i 1)).det
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
⊢ ∑ σ, ↑↑(sign σ) * ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 =
    ∑ σ, ↑↑(sign σ) * ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ σ, ↑↑(sign σ) * ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 =
    ∑ σ, ↑↑(sign σ) * ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ {n}.max = ↑n

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ {n}.max = ↑n
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if σ j' = σ j then Pi.single j 1 j' else A (σ j') j') = if j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'

Tactic:
]

Goal state after:
case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if σ j' = σ j then Pi.single j 1 j' else A (σ j') j') = if j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if x : j' = j then Pi.single j 1 j' else A (σ j') j') = if x : j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'

Tactic:
]

Goal state after:
case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if x : j' = j then Pi.single j 1 j' else A (σ j') j') = if x : j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case pos.e_f.e_t
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j' ↔ j' = j'
⊢ 1 = 1

Tactic:
]

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 α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
⊢ 0 = 0

Tactic:
]

Goal state after:
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
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = 0

Tactic:
]

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
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = 0
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Cardinal.lift.{max uM (max uN uS) uT, uP} (Module.rank T P) =
    Cardinal.lift.{max uP (max uN uS) uT, uM} (Module.rank R M)

Tactic:
]

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Cardinal.lift.{max uM (max uN uS) uT, uP} (Module.rank T P) =
    Cardinal.lift.{max uP (max uN uS) uT, 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 α
hA : A.IsSymm
⊢ A.adjugate = A.adjugate

Tactic:
]

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

Goal state before:
pp: m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j ↦ Pi.single i 1 (e.symm j)) = Pi.single (e i) 1
⊢ ((A.updateRow (e j) (Pi.single (e i) 1)).submatrix ⇑e ⇑e).det =
    ((A.updateRow (e j) (Pi.single (e i) 1)).submatrix ⇑e ⇑e).det

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (C 1 * T n).degree = ↑n

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (C 1 * T n).degree = ↑n
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a * T 0).degree = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a * T 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 α
b : n → α
⊢ A.cramer b = Aᵀᵀ.adjugate *ᵥ b

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = Aᵀᵀ.adjugate *ᵥ b
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ (T n).degree = (T n).degree

Tactic:
]

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 → α
⊢ A.cramer b = (of fun i ↦ Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = (of fun i ↦ Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).degree = (C a).degree

Tactic:
]

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

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
inst✝¹ : Semiring R✝
R : Type u_3
inst✝ : Semiring R
x y : R[X]
z : R[T;T⁻¹]
⊢ x • y • z = x • y • z

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (T ↑n)

Tactic:
]

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (T ↑n)
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 k : n
⊢ Aᵀ.cramer (Pi.single k (A i k)) j = Aᵀ.cramer (Pi.single k (A i k)) j

Tactic:
]

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
h : i ≠ j
c : R
⊢ 1 = 1

Tactic:
]

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 α
i j : n
⊢ ∑ j_1, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ j_1, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g

Tactic:
]

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g
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.adjugate * A = A.adjugate * A

Tactic:
]

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 α
⊢ A.det • 1 = A.det • 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ toLaurent p = toLaurent p

Tactic:
]

Goal state after:
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, ⋯⟩ * T ↑n = toLaurent p

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ IsLocalization.mk' R[T;T⁻¹] p ⟨X ^ n, ⋯⟩ * T ↑n = toLaurent p
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ (of fun i ↦ (r ^ (Fintype.card n - 1) • Aᵀ.cramer) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • of fun i ↦ Aᵀ.cramer (Pi.single i 1)

Tactic:
]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ (of fun i ↦ (r ^ (Fintype.card n - 1) • Aᵀ.cramer) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • of fun i ↦ Aᵀ.cramer (Pi.single i 1)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ T (-↑n) = T (-↑n)

Tactic:
]

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 → α
⊢ A.det • b = A.det • b

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
⊢ Polynomial.eval₂ f (↑x) p = Polynomial.eval₂ f (↑x) p

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ ↑x ^ n = ↑x ^ n

Tactic:
]

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

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max uS uT uN, max (max uP uS) uT} (Module.rank ST (ST ⊗[T] P)) =
    Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N))

Tactic:
]

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max uS uT uN, max (max uP uS) uT} (Module.rank ST (ST ⊗[T] P)) =
    Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N))
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ (eval₂ f x) (IsLocalization.mk' R[T;T⁻¹] 1 ⟨X ^ n, ⋯⟩) = ↑x⁻¹ ^ n

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ (eval₂ f x) (IsLocalization.mk' R[T;T⁻¹] 1 ⟨X ^ n, ⋯⟩) = ↑x⁻¹ ^ n
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
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L).prod * (List.map toMatrix L.reverse).prod =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L).prod * (List.map toMatrix L.reverse).prod

Tactic:
]

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

Goal state before:
pp: case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i : n
⊢ ∏ x ∈ univ.erase i, v x = ∏ j ∈ univ.erase i, v j

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ 1 = 1

Tactic:
]

Goal state after:
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
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute t.toMatrix M

Tactic:
]

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 : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute t.toMatrix M
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = 0

Tactic:
]

Goal state after:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case inr.inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i k : n
hij : i ≠ k
⊢ 0 = 0

Tactic:
]

Goal state after: