mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: case intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
hbi : b i = (Finset.affineCombination k Finset.univ p) (A i)
⊢ (Finset.affineCombination k Finset.univ p) (A i) ∈ affineSpan k (range p)

Tactic:
]

Goal state after:
case intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
hbi : b i = (Finset.affineCombination k Finset.univ p) (A i)
⊢ (Finset.affineCombination k Finset.univ p) (A i) ∈ affineSpan k (range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j =
    (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ ⇑b₂)) fun i ↦ (b₂.coord i) x

Tactic:
]

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j =
    (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ ⇑b₂)) fun i ↦ (b₂.coord i) x
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ 1 l m = 1 l m

Tactic:
]

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

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Tactic:
]

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
Module: Mathlib.LinearAlgebra.BilinearForm.Isometry

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
g : B₂ →bᵢ B₃
f : B₁ →bᵢ B₂
x y : M₁
⊢ (B₃ (g (f x))) (g (f y)) = (B₃ (g (f x))) (g (f y))

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Isometry

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
inst✝ : Subsingleton M₁
x y : M₁
⊢ (B₂ ((toAddHom 0).toFun 0)) ((toAddHom 0).toFun 0) = (B₁ 0) 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
inst✝ : Subsingleton M₁
x y : M₁
⊢ (B₂ ((toAddHom 0).toFun 0)) ((toAddHom 0).toFun 0) = (B₁ 0) 0
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b₂.coords x = b₂.coords x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ (B₂ (f ((↑f.symm).toFun n✝))) (f ((↑f.symm).toFun m✝)) = (B₂ n✝) m✝

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ (B₂ (f ((↑f.symm).toFun n✝))) (f ((↑f.symm).toFun m✝)) = (B₂ n✝) m✝
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)

Tactic:
]

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x) = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) =
    (B₃ (g (f n))) (g (f m))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) =
    (B₃ (g (f n))) (g (f m))
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x = q
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑p) +ᵥ y = (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x

Tactic:
]

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x = q
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑p) +ᵥ y = (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑p) +ᵥ x = q
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ y = (1 - r) • (c -ᵥ ↑p) +ᵥ x

Tactic:
]

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑p) +ᵥ x = q
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ y = (1 - r) • (c -ᵥ ↑p) +ᵥ x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case mp.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x = q
⊢ (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case mpr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑p) +ᵥ x = q
⊢ (1 - r) • (c -ᵥ ↑p) +ᵥ x = (1 - r) • (c -ᵥ ↑p) +ᵥ x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
h : Nonempty ↥s
c : P
⊢ ∃ x ∈ s, (c -ᵥ ↑h.some) +ᵥ x = c

Tactic:
exact ⟨h.some, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((basis b ibc).repr ((b.repr v) i • ε (b i))) i = (algebraMap R S) ((b.repr v) i)

pp: case h₀
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ∀ (b_1 : ι), (b.repr v) b_1 ≠ 0 → b_1 ≠ i → ((basis b ibc).repr ((b.repr v) b_1 • ε (b b_1))) i = 0

pp: case h₁
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ (b.repr v) i = 0 → ((basis b ibc).repr (0 • ε (b i))) i = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((basis b ibc).repr ((b.repr v) i • ε (b i))) i = (algebraMap R S) ((b.repr v) i)

case h₀
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ∀ (b_1 : ι), (b.repr v) b_1 ≠ 0 → b_1 ≠ i → ((basis b ibc).repr ((b.repr v) b_1 • ε (b b_1))) i = 0

case h₁
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ (b.repr v) i = 0 → ((basis b ibc).repr (0 • ε (b i))) i = 0
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((algebraMap R S) ((b.repr v) i) • (basis b ibc).repr ((basis b ibc) i)) i = (algebraMap R S) ((b.repr v) i)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((algebraMap R S) ((b.repr v) i) • (basis b ibc).repr ((basis b ibc) i)) i = (algebraMap R S) ((b.repr v) i)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈
    map (↑(AffineEquiv.constVAdd k P ((1 - (1 - w i)) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (affineSpan k (p '' {i}ᶜ))

Tactic:
]

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈
    map (↑(AffineEquiv.constVAdd k P ((1 - (1 - w i)) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (affineSpan k (p '' {i}ᶜ))
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: case h₀
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i i' : ι
a✝ : (b.repr v) i' ≠ 0
h : i' ≠ i
⊢ ((algebraMap R S) ((b.repr v) i') • (basis b ibc).repr ((basis b ibc) i')) i = 0

Tactic:
]

Goal state after:
case h₀
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i i' : ι
a✝ : (b.repr v) i' ≠ 0
h : i' ≠ i
⊢ ((algebraMap R S) ((b.repr v) i') • (basis b ibc).repr ((basis b ibc) i')) i = 0
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
H : σ₁⁻¹ * σ₂ ∈ (Perm.sumCongrHom ιa ιb).range
⊢ Perm.sign σ₁ • MultilinearMap.domDomCongr σ₁ ((↑a).domCoprod ↑b) =
    Perm.sign σ₂ • MultilinearMap.domDomCongr σ₂ ((↑a).domCoprod ↑b)

Tactic:
]

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
H : σ₁⁻¹ * σ₂ ∈ (Perm.sumCongrHom ιa ιb).range
⊢ Perm.sign σ₁ • MultilinearMap.domDomCongr σ₁ ((↑a).domCoprod ↑b) =
    Perm.sign σ₂ • MultilinearMap.domDomCongr σ₂ ((↑a).domCoprod ↑b)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) (-(w i • (Pi.single i 1 - Pi.single j 1)) + w) ∈ affineSpan k (p '' {i}ᶜ)

Tactic:
]

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) (-(w i • (Pi.single i 1 - Pi.single j 1)) + w) ∈ affineSpan k (p '' {i}ᶜ)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
V : Type u_2
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : Module A V
inst✝ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
⊢ Function.Bijective ⇑(Finsupp.linearCombination R ⇑b)

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
V : Type u_2
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : Module A V
inst✝ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
⊢ Function.Bijective ⇑(Finsupp.linearCombination R ⇑b)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈
      map (↑(AffineEquiv.constVAdd k P ((1 - c) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (affineSpan k (p '' {i}ᶜ)) →
    w i = 1 - c

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈
      map (↑(AffineEquiv.constVAdd k P ((1 - c) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (affineSpan k (p '' {i}ᶜ)) →
    w i = 1 - c
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : ιa ⊕ ιb → Mᵢ
h : σ₂ = σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)
this : Perm.sign (σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) = Perm.sign σ₁ * (Perm.sign sl * Perm.sign sr)
⊢ (Perm.sign sl • a ((fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ∘ ⇑sl)) ⊗ₜ[R']
      (Perm.sign sr • b ((fun i₂ ↦ v (σ₁ (Sum.inr i₂))) ∘ ⇑sr)) =
    (Perm.sign sl • a fun i₁ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inl i₁))) ⊗ₜ[R']
      (Perm.sign sr • b fun i₂ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inr i₂)))

Tactic:
]

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : ιa ⊕ ιb → Mᵢ
h : σ₂ = σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)
this : Perm.sign (σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) = Perm.sign σ₁ * (Perm.sign sl * Perm.sign sr)
⊢ (Perm.sign sl • a ((fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ∘ ⇑sl)) ⊗ₜ[R']
      (Perm.sign sr • b ((fun i₂ ↦ v (σ₁ (Sum.inr i₂))) ∘ ⇑sr)) =
    (Perm.sign sl • a fun i₁ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inl i₁))) ⊗ₜ[R']
      (Perm.sign sr • b fun i₂ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inr i₂)))