mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥H → R
hf : f ∈ sU
hg : f ∈ sV
⊢ ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥H → R
hf : f ∈ sU
hg : f ∈ sV
⊢ ∃ n, ¬n = 0 ∧ f = -∑ x, ↑(n x) * ⇑(b.baseSupp x)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥H → R
hf : f ∈ sU
hg : f ∈ sV
n : ι → ℕ
hn : n ≠ 0
hn' : f = -⇑(∑ i, n i • b.baseSupp i)
⊢ ∃ m, m ≠ 0 ∧ f = ⇑(∑ i, m i • b.baseSupp i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥H → R
hf : f ∈ sU
hg : f ∈ sV
n : ι → ℕ
hn : n ≠ 0
hn' : f = -⇑(∑ i, n i • b.baseSupp i)
⊢ ∃ m, ¬m = 0 ∧ f = ∑ x, ↑(m x) * ⇑(b.baseSupp x)
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id * LinearMap.id + LinearMap.id * ↑n • LinearMap.smulRight (f - g) x +
      (LinearMap.smulRight (f - g) x * LinearMap.id +
        LinearMap.smulRight (f - g) x * ↑n • LinearMap.smulRight (f - g) x) =
    LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x

Tactic:
Module.End.mul_eq_comp,

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id ∘ₗ LinearMap.id + LinearMap.id ∘ₗ (↑n • LinearMap.smulRight (f - g) x) +
      (LinearMap.smulRight (f - g) x ∘ₗ LinearMap.id +
        LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x)) =
    LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : IsOfFinOrder u
n : ℕ
hn₀ : 0 < n
hn₁ : ↑(u ^ n) = LinearMap.id
⊢ f = g

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : IsOfFinOrder u
n : ℕ
hn₀ : 0 < n
hn₁ : ↑(u ^ n) = LinearMap.id
⊢ f = g
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
x✝ : M
⊢ P.pairing i j = 0 ∧ P.pairing j i = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
x✝ : M
⊢ P.pairing i j = 0 ∧ P.pairing j i = 0
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : (P.reflectionPerm i) j = j
⊢ P.pairing j i • P.root i = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : (P.reflectionPerm i) j = j
⊢ P.pairing j i • P.root i = 0
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i✝ j✝ : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
i j : ι
h : P.pairing i j = 0
⊢ P.pairing j i = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i✝ j✝ : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
i j : ι
h : P.pairing i j = 0
⊢ P.pairing j i = 0
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
i✝ j✝ : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
i j : ι₂
⊢ ((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding) j -
      (↑(f.symm ≪≫ₗ P.toPerfPair ≪≫ₗ g.symm.dualMap)
            (((e.symm.toEmbedding.trans P.root).trans f.toAddEquiv.toEmbedding) i))
          (((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding) j) •
        ((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding) i =
    ((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding)
      ((e.symm.trans ((P.reflectionPerm (e.symm i)).trans e)) j)

Tactic:
by simp [coreflection_apply]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ Bᵀ * Aᵀ = 1

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ Bᵀ * Aᵀ = 1
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
n : N'
⊢ (p.toPerfPair (i m)) (j n) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
n : N'
⊢ (p (i m)) (j n) = 0
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : i m ∈ Submodule.map (↑p.toPerfPair.symm) j.range.dualAnnihilator
this : i m ∈ ⊥
⊢ m ∈ ⊥

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : i m ∈ Submodule.map (↑p.toPerfPair.symm) j.range.dualAnnihilator
this : i m ∈ ⊥
⊢ m = 0
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : i m ∈ Submodule.map (↑p.toPerfPair.symm) j.range.dualAnnihilator
⊢ i m ∈ ⊥

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : i m ∈ Submodule.map (↑p.toPerfPair.symm) j.range.dualAnnihilator
⊢ i m ∈ i.range ∧ i m ∈ Submodule.map (↑p.toPerfPair.symm) j.range.dualAnnihilator
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this✝ : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0
i : ι
this : m i = 0 ∧ n i = 0
⊢ n i = 0 i

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this✝ : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0
i : ι
this : m i = 0 ∧ n i = 0
⊢ n i = 0
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
this : ∀ (k : ι), (c i) (r k) = (c j) (r k)
⊢ (c i) (r j) = 2

Tactic:
by rw [this, h_two]

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
k : ι
⊢ (c i) (r k) = (c j) (r k)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
k : ι
⊢ (c i) (r k) = (c j) (r k)
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N := f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF✝ : F = f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toPerfPair.symm F
hm : m = p.toPerfPair.symm F
m₀ : M'
n : N'
g : Dual R N
hg : ∀ w ∈ j.range, g w = 0
hm' : i m₀ + ↑p.toPerfPair.symm g = m
⊢ (p (↑p.toPerfPair.symm g)) (j n) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N := f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF✝ : F = f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toPerfPair.symm F
hm : m = p.toPerfPair.symm F
m₀ : M'
n : N'
g : Dual R N
hg : ∀ w ∈ j.range, g w = 0
hm' : i m₀ + ↑p.toPerfPair.symm g = m
⊢ g (j n) = 0
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n : N
n' : N'
⊢ (p (i x)) (j n') = 0

Tactic:
simpa using

Goal state after:
case mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n : N
n' : N'
⊢ (p (i x)) (j n') = 0
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
p : Submodule R M
⊢ Surjective ⇑(tensorToSpan A p)

Tactic:
intro v
  obtain ⟨f, hf⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp v.property
  use f.sum fun x a ↦ a ⊗ₜ x
  rw [map_finsuppSum, Subtype.ext_iff, ← Submodule.subtype_apply, map_finsuppSum]
  simpa using! hf

Goal state after: