mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
hs : ⊤ ≤ span K s
⊢ ⋯.extend ⋯ = ⋯.extend ⋯

Tactic:
]

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)

Tactic:
]

Goal state after:
ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = ↑x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case left
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ∃ x ∈ K ∙ v, x ≠ 0

Tactic:
]

Goal state after:
case left
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ∃ x ∈ K ∙ v, x ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} (Module.rank R M)

Tactic:
]

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

Goal state before:
pp: R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : Nonempty (Fintype { i // p i ≠ ⊥ })
⊢ Fintype { i // p i ≠ ⊥ }

Tactic:
]

Goal state after:
R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : Nonempty (Fintype { i // p i ≠ ⊥ })
⊢ Fintype { i // p i ≠ ⊥ }
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case right.inr
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
⊢ v ∈ T

Tactic:
]

Goal state after:
case right.inr
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
⊢ v ∈ T
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False

Tactic:
specialize h (span K {v})

Goal state after:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
h : K ∙ v < W → K ∙ v = ⊥
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
h : K ∙ v ≤ W ∧ K ∙ v ≠ W → v = 0
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False

Tactic:
]

Goal state after:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
h : K ∙ v ≤ W ∧ K ∙ v ≠ W → v = 0
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ g z ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ g z ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ extend Subtype.val g 0 ↑z ≠ 0

Tactic:
rwa [Subtype.val_injective.extend_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
⊢ LinearIndepOn K _root_.id (⇑f '' B)

Tactic:
have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
h₁ : LinearIndepOn K _root_.id (⇑f '' Set.range ⇑(Basis.ofVectorSpace K V))
⊢ LinearIndepOn K _root_.id (⇑f '' B)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∑ i, extend Subtype.val g 0 ↑i • ↑i = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∑ i, extend Subtype.val g 0 ↑i • ↑i = 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
h₁ : LinearIndepOn K _root_.id (⇑f '' Basis.ofVectorSpaceIndex K V)
⊢ LinearIndepOn K _root_.id (⇑f '' B)

Tactic:
]

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
h₁ : LinearIndepOn K _root_.id (⇑f '' Basis.ofVectorSpaceIndex K V)
⊢ LinearIndepOn K _root_.id (⇑f '' B)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)

Tactic:
]

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubalgebra = T.toNonUnitalSubalgebra
x : A
⊢ x ∈ T.toNonUnitalSubalgebra ↔ x ∈ T.toNonUnitalSubalgebra

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = ↑S
x : A
hx : x ∈ ↑S
⊢ star x ∈ ↑S

Tactic:
]

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = ↑S
x : A
hx : x ∈ ↑S
⊢ star x ∈ ↑S
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ T.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
⊢ finrank R M < #t - 1

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
⊢ finrank R M < #t - 1
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ C.domRestrict (invFun ⇑f) ⟨f ↑b, ⋯⟩ = ↑b

Tactic:
]

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ C.domRestrict (invFun ⇑f) ⟨f ↑b, ⋯⟩ = ↑b
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
g : B → A
f : F
h : Function.LeftInverse g ⇑f
x : ↥(NonUnitalStarAlgHom.range f)
x' : A
hx' : f x' = ↑x
⊢ f x' = f x'

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
p : Submodule K V
f : ↥p →ₗ[K] V'
g : V →ₗ[K] ↥p
hg : g ∘ₗ p.subtype = id
⊢ f = f

Tactic:
]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : StarRing B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : StarHomClass F A B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ NonUnitalAlgebra.adjoin R (s ∪ star s)

Tactic:
]

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : StarRing B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : StarHomClass F A B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ NonUnitalAlgebra.adjoin R (s ∪ star s)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0

Tactic:
simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul,
             ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum, smul_sub]

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x ∈ t.erase x₀, ((if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x - g (x - x₀) • x₀) =
    ∑ x ∈ t.erase x₀, (g (x - x₀) • x - g (x - x₀) • x₀)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x : M
x_mem : x ∈ t.erase x₀
⊢ g (x - x₀) • x - g (x - x₀) • x₀ = g (x - x₀) • x - g (x - x₀) • x₀

Tactic:
]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e = 0

pp: case refine_3
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
· rw [sum_map, Embedding.coeFn_mk] at gsum
    simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul,
             ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum, smul_sub]
    refine sum_congr rfl fun x x_mem ↦ ?_
    rw [if_neg (mem_erase.mp x_mem).1]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e = 0

case refine_3
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x ∈ t, f x ≠ 0
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ⊆ ↑S

Tactic:
]

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ⊆ ↑S
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ Submodule.span R ↑(Subsemigroup.closure (s ∪ star s)) = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
]

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ S ≤ S ⊔ T