mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.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✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R C
S : NonUnitalSubalgebra R A
s : Set A
hs : s = ↑S
r : R
a : A
⊢ a ∈ (S.copy s hs).carrier → r • a ∈ (S.copy s hs).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
inst✝ : Subsingleton (Subalgebra R B)
f g : A ≃ₐ[R] B
⊢ f = g

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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
S T : NonUnitalSubalgebra R A
h : (fun S ↦ S.toSubmodule) S = (fun S ↦ S.toSubmodule) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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
S T : NonUnitalSubalgebra R A
h : (fun S ↦ S.toNonUnitalSubsemiring) S = (fun S ↦ S.toNonUnitalSubsemiring) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
by

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝² : CommRing R
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : (fun S ↦ S.toNonUnitalSubring) S = (fun S ↦ S.toNonUnitalSubring) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
⊢ ∀ (a : Subalgebra R R), a = default

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R A
inst✝³ : Module R B
inst✝² : Module R C
S✝ : NonUnitalSubalgebra R A
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
b : B
hb : b ∈ (NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring).carrier
⊢ r • b ∈ (NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
⊢ φ.equalizer ψ = ⊤ ↔ φ = ψ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : B
⊢ a ∈ (NonUnitalRingHom.srange ↑φ).carrier → r • a ∈ (NonUnitalRingHom.srange ↑φ).carrier

Tactic:
by

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

Goal state before:
pp: F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
⊢ ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ x + y ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
F : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : Set.EqOn ⇑φ ⇑ψ ↑S
hT : Set.EqOn ⇑φ ⇑ψ ↑T
⊢ Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
⊢ 0 ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R B
h : S ≤ f.range
⊢ map f (comap f S) = S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
S : Subalgebra R B
⊢ S ≤ f.range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ x * y ∈ {a | ϕ a = ψ a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.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✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : ϕ x = ψ x
⊢ r • x ∈ {a | ϕ a = ψ a}

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
s : NonUnitalSubalgebra R A
⊢ Submodule.span R ↑s = s.toSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
⊢ ∀ {a b : S}, a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
p q : Subalgebra R A
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 1 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ (linearEquivFunOnFintype R ι M) ((lof R ι M i) m) = Pi.single i m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 0 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ (component R ι M x✝) f = (component R ι M x✝) g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i j : ι
⊢ component R ι M i ∘ₗ lof R ι M j = if h : j = i then h ▸ LinearMap.id else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
⊢ component R ι M i ∘ₗ lof R ι M i = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M i →ₗ[R] N i
⊢ Function.Injective ⇑(lmap f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
⊢ ∀ {a b : S}, a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a + b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝¹ x✝ : Subalgebra R A
⊢ x✝¹.toNonUnitalSubalgebra = x✝.toNonUnitalSubalgebra → x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M i →ₗ[R] N i
⊢ Function.Surjective ⇑(lmap f) ↔ ∀ (i : ι), Function.Surjective ⇑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
e : ι ≃ κ
i : ι
k : κ
hik : i = e.symm k
x : M i
y : M (e.symm k)
hxy : cast ⋯ x = y
⊢ (lequivCongrLeft R e) ((lof R ι M i) x) = (lof R κ (fun i ↦ M (e.symm i)) k) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
r : R
⊢ 1 * (algebraMap R S) r ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubring = T.toSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
x : S
hx : x ∈ s
⊢ 1 * x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
h : ι ≃ κ
k : κ
x : M (h.symm k)
⊢ (lequivCongrLeft R h).symm ((lof R κ (fun k ↦ M (h.symm k)) k) x) = (lof R ι M (h.symm k)) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
ι : Type v
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → Module R (δ i j)
r : R
⊢ ∀ (x : ⨁ (i : (x : ι) × α x), δ i.fst i.snd), (↑sigmaCurry).toFun (r • x) = (RingHom.id R) r • (↑sigmaCurry).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : DecidableEq A
α : Type u_2
s : Finset α
f : ↥s → Finset A
⊢ adjoin R ↑(s.attach.biUnion f) = ⨆ x, adjoin R ↑(f x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (coeLinearMap A) x = DFinsupp.sum x fun i x ↦ ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i : ι
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) i = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
S : Subalgebra R A
inst✝³ : CommSemiring R'
inst✝² : SMul R' R
inst✝¹ : Algebra R' A
inst✝ : IsScalarTower R' R A
x : R'
⊢ (algebraMap R' A) x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i j : ι
hij : i ≠ j
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) j = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ ↑⟨(algebraMap R A) 1, ⋯⟩ = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
⊢ ⇑(h.collectedBasis v) = fun a ↦ ↑((v a.fst) a.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
x✝¹ x✝ : R
⊢ ↑⟨(algebraMap R A) (x✝¹ * x✝), ⋯⟩ = ↑(⟨(algebraMap R A) x✝¹, ⋯⟩ * ⟨(algebraMap R A) x✝, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (h.collectedBasis v) a ∈ A a.fst

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ ↑⟨(algebraMap R A) 0, ⋯⟩ = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i : ι
a : α i
hx : x ∈ A i
⊢ ((h.collectedBasis v).repr x) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
⊢ ∀ {a b : A},
    a ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} → a * b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
x✝¹ x✝ : R
⊢ ↑⟨(algebraMap R A) (x✝¹ + x✝), ⋯⟩ = ↑(⟨(algebraMap R A) x✝¹, ⋯⟩ + ⟨(algebraMap R A) x✝, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i j : ι
hij : i ≠ j
a : α j
hx : x ∈ A i
⊢ ((h.collectedBasis v).repr x) ⟨j, a⟩ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p✝ p : Submodule R A
h_one : 1 ∈ p
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
r : R
⊢ (algebraMap R A) r ∈ p.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ iSup A = A i ⊔ A j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
⊢ ∀ {a b : A},
    a ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} → a + b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
k : ι
⊢ k = i ∨ k = j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
⊢ ∀ (r : R),
    (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
φ : A →ₐ[R] B
⊢ φ.range.val.comp φ.rangeRestrict = φ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ (e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r) = (algebraMap R ↥(Subalgebra.map (↑e) S)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B✝ : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B✝
inst✝¹ : Algebra R B✝
S T U : Subalgebra R A
inst✝ : Subsingleton A
B C : Subalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
⊢ IsInternal A ↔ IsCompl (A i) (A j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
⊢ (IsInternal fun i ↦ A ↑i) ↔ IsInternal A

Tactic:
by

Goal state after: