mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑sb * (↑sa * ↑s₂) ∈ S

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑sb * (↑sa * ↑s₂) ∈ S
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ ⟨↑sb * ra * ↑s₃, hs₃rasb⟩) • (r₁ /ₒ s₁)

Tactic:
]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ ⟨↑sb * ra * ↑s₃, hs₃rasb⟩) • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁)

Tactic:
]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + rc • r₁ /ₒ (sc * (sb * sa * s₂))

Tactic:
]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + rc • r₁ /ₒ (sc * (sb * sa * s₂))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
R : Type u_1
inst✝⁴ : CommSemiring R
n✝ : Type u_4
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n✝ R M₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ ((toLin v₁ v₁) A ^ n) ∘ₗ (toLin v₁ v₁) A = ((toLin v₁ v₁) A ^ n) ∘ₗ (toLin v₁ v₁) A

Tactic:
]

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝⁴ : Fintype m
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
x : M₁
⊢ ((toLin v₂ v₃) A) (((toLin v₁ v₂) B) x) = ((toLin v₂ v₃) A) (((toLin v₁ v₂) B) x)

Tactic:
]

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_2.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i✝ : Fin (n' + 1)
i : Fin n'
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i.succ) =
    Fin.cons a as i.succ • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ i).succ)

Tactic:
]

Goal state after:
case neg.intro.refine_2.refine_2.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i✝ : Fin (n' + 1)
i : Fin n'
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i.succ) =
    Fin.cons a as i.succ • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ i).succ)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * rb + rc) * ↑s₁ /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * rb + rc) * ↑s₁ /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ x = x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
⊢ f = f

Tactic:
]

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ (↑sc * rb + rc) • r₁ /ₒ (sc * sb * (sa * s₂)) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ (↑sc * rb + rc) • r₁ /ₒ (sc * sb * (sa * s₂)) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ M = M

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
S : Submonoid R
inst✝⁷ : OreSet S
X : Type u_2
inst✝⁶ : AddCommMonoid X
inst✝⁵ : Module R X
R₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
x : OreLocalization S X
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
⊢ ∑ i, (M *ᵥ ⇑(v₁.repr v)) i • v₁ i = ∑ j, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j

Tactic:
]

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

Goal state before:
pp: case c
R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ r₁ * (algebraMap R₀ R) r /ₒ s₁ = r₁ * (algebraMap R₀ R) r /ₒ s₁

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = r • x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
⊢ ↑(fS 1)⁻¹ * ↑f 0 = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
⊢ ↑(fS 1)⁻¹ * ↑f 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
subst N_bot

Goal state after:
case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
ih : ∀ N' ≤ ⊥, ∀ x ∈ ⊥, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥⊥)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
h₃' : r₁ /ₒ s₁ + r₂ /ₒ s₂ = (s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)
⊢ (universalMulHom (↑f) fS ⋯) ((s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)) =
    (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) (r₂ /ₒ s₂)

Tactic:
]

Goal state after:
case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
h₃' : r₁ /ₒ s₁ + r₂ /ₒ s₂ = (s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)
⊢ (universalMulHom (↑f) fS ⋯) ((s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)) =
    (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) (r₂ /ₒ s₂)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
x : R
i✝ j✝ : n
⊢ (if i✝ = j✝ then x else 0) = if i✝ = j✝ then x else 0

Tactic:
]

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

Goal state before:
pp: case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * (↑((fS s₃)⁻¹ * fS s₃) * f r₁) + ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) =
    ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₂)⁻¹ * f r₂

Tactic:
]

Goal state after:
case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * (↑((fS s₃)⁻¹ * fS s₃) * f r₁) + ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) =
    ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₂)⁻¹ * f r₂
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ * f r₂ = ↑(fS s₂)⁻¹ * f r₂

Tactic:
]

Goal state after:
case c.c.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ * f r₂ = ↑(fS s₂)⁻¹ * f r₂
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) x) * (toMatrix b b) ((lmul R S) y) =
    (toMatrix b b) ((lmul R S) x) * (toMatrix b b) ((lmul R S) y)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ ↑(fS ⟨r₃ * ↑s₂, ⋯⟩)⁻¹ * f r₃ = ↑(fS s₂)⁻¹

Tactic:
]

Goal state after:
case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ ↑(fS ⟨r₃ * ↑s₂, ⋯⟩)⁻¹ * f r₃ = ↑(fS s₂)⁻¹
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) x) + (toMatrix b b) ((lmul R S) y) =
    (toMatrix b b) ((lmul R S) x) + (toMatrix b b) ((lmul R S) y)

Tactic:
]

Goal state after: