mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal fun k ↦ (M k)ᵀ.map star) = blockDiagonal fun k ↦ (M k)ᵀ.map star

Tactic:
]

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ b j = b j

Tactic:
]

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M i' j = M i' j

Tactic:
]

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ c i = c i

Tactic:
]

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M i j' = M i j'

Tactic:
]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ f (if i✝ = i then b j✝ else M i✝ j✝) = if i✝ = i then (f ∘ b) j✝ else f (M i✝ j✝)

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ f (if i✝ = i then b j✝ else M i✝ j✝) = if i✝ = i then (f ∘ b) j✝ else f (M i✝ j✝)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ f (if j✝ = j then c i✝ else M i✝ j✝) = if j✝ = j then (f ∘ c) i✝ else f (M i✝ j✝)

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ f (if j✝ = j then c i✝ else M i✝ j✝) = if j✝ = j then (f ∘ c) i✝ else f (M i✝ j✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case e_c
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (i = j ∧ k = k') = (i = j ∧ k = k')

Tactic:
]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ (if i✝ = j then c j✝ else Mᵀ i✝ j✝) = if i✝ = j then c j✝ else M j✝ i✝

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ (if i✝ = j then c j✝ else Mᵀ i✝ j✝) = if i✝ = j then c j✝ else M j✝ i✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : One α
⊢ (diagonal fun ik ↦ 1) = diagonal fun x ↦ 1

Tactic:
]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ (if j✝ = i then b i✝ else Mᵀ i✝ j✝) = if j✝ = i then b i✝ else M j✝ i✝

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ (if j✝ = i then b i✝ else Mᵀ i✝ j✝) = if j✝ = i then b i✝ else M j✝ i✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Tactic:
]

Goal state after:
case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ v j = v j

Tactic:
]

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

Goal state before:
pp: case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
]

Goal state after:
case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ diagonal (Function.update v i x) = diagonal (Function.update v i x)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ d (i, k) = d (i, k)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ 0 = 0

pp: m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j

Tactic:
]

Goal state after:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0) =
    if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0

Tactic:
]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : m
j : n
r : α
⊢ updateCol 0 j (A.col i <• r) = updateCol 0 j (A.col i <• r)

Tactic:
]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
j : m
r : α
B : Matrix m n α
⊢ updateRow 0 i (r • B.row j) = updateRow 0 i (r • B.row j)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : (i : o) → DecidableEq (m' i)
inst✝ : One α
⊢ (diagonal fun ik ↦ 1) = diagonal fun x ↦ 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x, (if h : k = k then M k i (cast ⋯ x) else 0) * if h : k = k' then N k x (cast ⋯ j) else 0

pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k → (∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0

Tactic:
]

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x, (if h : k = k then M k i (cast ⋯ x) else 0) * if h : k = k' then N k x (cast ⋯ j) else 0

o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k → (∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
x✝¹ : n' j'
x✝ : x✝¹ ∈ Finset.univ
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq l
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
⊢ of (Pi.single i (Pi.single j (r ⬝ᵥ c))) = of (Pi.single i (Pi.single j (r ⬝ᵥ c)))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ d ⟨k, i⟩ = d ⟨k, i⟩

Tactic:
]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ 0 = 0

pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : ⟨k, i⟩ = ⟨k, j⟩
⊢ i = j

Tactic:
]

Goal state after:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : ⟨k, i⟩ = ⟨k, j⟩
⊢ i = j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ a, A ↑i ↑a * B ↑a ↑k = ∑ j, A ↑i ↑j * B ↑j ↑k

pp: case h
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∀ (x : n), x ∈ Finset.univ ↔ ?m.38 x

pp: R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ n → Prop

pp: R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ Fintype (Subtype ?m.38)

Tactic:
]

Goal state after:
case h
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∀ (x : n), x ∈ Finset.univ ↔ ⊤ x
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
r : R
a : A
⊢ r • e₂.toFun (e₁.toFun a) = r • e₂.toFun (e₁.toFun a)

Tactic:
]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
⊢ ∀ x ∈ N, x = 0

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
⊢ ∀ x ∈ N, x = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = (b.repr 0) i

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = (b.repr 0) i
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = 0

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
⊢ ∀ x ∈ N, x = 0

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
⊢ ∀ x ∈ N, x = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = (b.repr 0) i

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = (b.repr 0) i
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = 0

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ R ∙ generator (span R {a, ψ ⟨y, ⋯⟩}) = R ∙ generator (ϕ.submoduleImage N)

pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∈ span R {a, ψ ⟨y, ⋯⟩}

Tactic:
]

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ R ∙ generator (span R {a, ψ ⟨y, ⋯⟩}) = R ∙ generator (ϕ.submoduleImage N)

R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∈ span R {a, ψ ⟨y, ⋯⟩}
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q) ((b * a) ⊗ₜ[R] (n ⊗ₜ[R] q)) = (b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q)

Tactic:
]

Goal state after:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q) ((b * a) ⊗ₜ[R] (n ⊗ₜ[R] q)) = (b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q)
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ∃ y, ∃ (yN : y ∈ N), ψ' ⟨y, ⋯⟩ = d

Tactic:
]

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ∃ y, ∃ (yN : y ∈ N), ψ' ⟨y, ⋯⟩ = d
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ r₁ * generator (ϕ.submoduleImage N) + r₂ * ψ ⟨y, ⋯⟩ = r₁ * a + r₂ * ψ ⟨y, ⋯⟩

Tactic:
]

Goal state after: