mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: case mk.mk
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
toNonUnitalSubalgebra✝¹ : NonUnitalSubalgebra R A
star_mem'✝¹ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝¹.carrier → star a ∈ toNonUnitalSubalgebra✝¹.carrier
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝¹, star_mem' := star_mem'✝¹ } =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
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
toNonUnitalSubalgebra✝¹ : NonUnitalSubalgebra R A
star_mem'✝¹ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝¹.carrier → star a ∈ toNonUnitalSubalgebra✝¹.carrier
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝¹, star_mem' := star_mem'✝¹ } =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: case mk.mk
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
toNonUnitalSubalgebra✝¹ : NonUnitalSubalgebra R A
star_mem'✝¹ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝¹.carrier → star a ∈ toNonUnitalSubalgebra✝¹.carrier
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ toNonUnitalSubalgebra✝¹ = toNonUnitalSubalgebra✝

Tactic:
;

Goal state after:
case mk.mk
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
toNonUnitalSubalgebra✝¹ : NonUnitalSubalgebra R A
star_mem'✝¹ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝¹.carrier → star a ∈ toNonUnitalSubalgebra✝¹.carrier
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ toNonUnitalSubalgebra✝¹ = toNonUnitalSubalgebra✝
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
f : F
S : NonUnitalStarSubalgebra R A
a : A
ha : a ∈ ↑S.toNonUnitalSubsemiring
⊢ star (↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) a) ∈
    (NonUnitalSubalgebra.map (NonUnitalAlgHomClass.toNonUnitalAlgHom f) S.toNonUnitalSubalgebra).carrier

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
f : F
S : NonUnitalStarSubalgebra R A
a : A
ha : a ∈ ↑S.toNonUnitalSubsemiring
⊢ star (↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) a) ∈
    (NonUnitalSubalgebra.map (NonUnitalAlgHomClass.toNonUnitalAlgHom f) S.toNonUnitalSubalgebra).carrier
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
φ : F
a : A
⊢ star (↑(NonUnitalAlgHomClass.toNonUnitalAlgHom φ) a) ∈
    (NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ)).carrier

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
φ : F
a : A
⊢ star (↑(NonUnitalAlgHomClass.toNonUnitalAlgHom φ) a) ∈
    (NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ)).carrier
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
x✝ : A
⊢ x✝ ∈ ⊤.toNonUnitalSubalgebra ↔ x✝ ∈ ⊤

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
x✝ : A
⊢ x✝ ∈ ⊤.toNonUnitalSubalgebra ↔ x✝ ∈ ⊤
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₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 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₀
x₁_mem : shift x₁ ∈ t'
nz : g (shift x₁) ≠ 0
this : x₁ ≠ x₀ ∧ x₁ ∈ t
⊢ x₁ ∈ t ∧ f x₁ ≠ 0

Tactic:
simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]

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 : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

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 : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
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 : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

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 : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : Subsingleton M
⊢ finrank R M ≤ 0

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : Subsingleton M
⊢ finrank R M ≤ 0
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalSemiring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Module R A
inst✝⁹ : NonUnitalSemiring B
inst✝⁸ : StarRing B
inst✝⁷ : Module R B
inst✝⁶ : StarRing R
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : StarModule R A
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalSemiring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Module R A
inst✝⁹ : NonUnitalSemiring B
inst✝⁸ : StarRing B
inst✝⁷ : Module R B
inst✝⁶ : StarRing R
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : StarModule R A
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ
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✝¹⁵ : 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
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ ((f k).comp (inclusion hik)) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
hf j k hjk

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✝¹⁶ : 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
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ ((f k).comp (inclusion hik)) ⟨x, hxi⟩ = ((f k).comp (inclusion hjk)) ⟨x, hxj⟩
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✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S < 1 ↔ S = ⊥

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S < 1 ↔ S = ⊥
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
left✝ : Module.Finite R M
right✝ : Finite ι
⊢ Module.Finite R (ι →₀ M)

Tactic:
;

Goal state after:
case intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
left✝ : Module.Finite R M
right✝ : Finite ι
⊢ Module.Finite R (ι →₀ M)
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f : E →ₛₗ.[σ] F
⊢ f.domain = f.domain ∧ ∀ ⦃x : E⦄ ⦃hf hg : x ∈ f.domain⦄, ↑f ⟨x, hf⟩ = ↑f ⟨x, hg⟩

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f : E →ₛₗ.[σ] F
⊢ f.domain = f.domain ∧ ∀ ⦃x : E⦄ ⦃hf hg : x ∈ f.domain⦄, ↑f ⟨x, hf⟩ = ↑f ⟨x, hg⟩
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
⊢ ∀ (m : K) (x : V),
    Finsupp.single default ((b.repr (m • x)) default / (b.repr v) default) =
      (RingHom.id K) m • Finsupp.single default ((b.repr x) default / (b.repr v) default)

Tactic:
by simp [mul_div]

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
h' : v₀ = 0
H : ¬⟨0, ⋯⟩ = 0
⊢ False

Tactic:
;

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
h' : v₀ = 0
H : ¬⟨0, ⋯⟩ = 0
⊢ False
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f
⊢ g * f = 1

Tactic:
;

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f
⊢ g * f = 1
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ ∀ x ∈ f.ker, g x ∈ f.ker

Tactic:
;

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ ∀ x ∈ f.ker, g x ∈ f.ker
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : K ∙ x = ⊤
⊢ y ∈ ⊤

Tactic:
;

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : K ∙ x = ⊤
⊢ y ∈ ⊤
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ Quot.mk (Rel R X) (Pre.ofScalar 0) = 0

Tactic:
;

Goal state after:
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ Quot.mk (Rel R X) (Pre.ofScalar 0) = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_scalar
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝ : FreeAlgebra R X
a b : Pre R X
r✝ s✝ : R
⊢ liftFun R X f (Pre.ofScalar (r✝ + s✝)) = liftFun R X f (Pre.ofScalar r✝ + Pre.ofScalar s✝)

Tactic:
exact (algebraMap R A).map_add _ _

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : S
φ : R[X]
⊢ eval₂ f s φ = eval₂ f s φ

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : S
φ : R[X]
⊢ eval₂ f s φ = eval₂ f s φ
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
p : R[ℕ]
⊢ eval₂ f x ({ toFinsupp := p } * q) = eval₂ f x { toFinsupp := p } * eval₂ f x q

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
p : R[ℕ]
⊢ eval₂ f x ({ toFinsupp := p } * q) = eval₂ f x { toFinsupp := p } * eval₂ f x q
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.add
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (a.add b)) = F (Quot.mk (Rel R X) (a.add b))

Tactic:
let fa : FreeAlgebra R X := Quot.mk (Rel R X) a

Goal state after:
case mk.add
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (a.add b)) = F (Quot.mk (Rel R X) (a.add b))
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (a.mul b)) = F (Quot.mk (Rel R X) (a.mul b))

Tactic:
let fa : FreeAlgebra R X := Quot.mk (Rel R X) a

Goal state after:
case mk.mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (a.mul b)) = F (Quot.mk (Rel R X) (a.mul b))
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : X
a✝ : FreeMonoid X
⊢ (((↑(((lift R) fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x)).comp
                  ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X)) (FreeMonoid.lift (ι R))))).comp
            (MonoidAlgebra.of R (FreeMonoid X)))
          (FreeMonoid.of x✝)).coeff
      a✝ =
    (((↑(AlgHom.id R R[FreeMonoid X])).comp (MonoidAlgebra.of R (FreeMonoid X))) (FreeMonoid.of x✝)).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : X
a✝ : FreeMonoid X
⊢ (((↑(((lift R) fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x)).comp
                  ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X)) (FreeMonoid.lift (ι R))))).comp
            (MonoidAlgebra.of R (FreeMonoid X)))
          (FreeMonoid.of x✝)).coeff
      a✝ =
    (((↑(AlgHom.id R R[FreeMonoid X])).comp (MonoidAlgebra.of R (FreeMonoid X))) (FreeMonoid.of x✝)).coeff a✝