mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x y : R}, x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → x * y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ∀ {w x y z : R}, f w = f x → f y = f z → f (w + y) = f (x + z)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x : R
⊢ x ∈ ker f ↔ f x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : OrzechProperty R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
h : finrank R M ≤ finrank R M'
⊢ Bijective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ker f = ⊥ ↔ Function.Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ ker I.ringCon.mk'
⊢ x✝ ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ I
⊢ x✝ - 0 ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
⊢ ∃! c, u = c • LinearMap.id

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
x✝ x : M
⊢ x = e.symm x • e 1

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
⊢ ∃! c, u = c • LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
⊢ (c + d) • LinearMap.id = c • LinearMap.id + d • LinearMap.id

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
⊢ (c • d) • LinearMap.id = (RingHom.id R) c • d • LinearMap.id

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c : R
⊢ (fun u ↦ Exists.choose ⋯) ((fun c ↦ c • LinearMap.id) c) = c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : IsSimpleRing R
⊢ Nontrivial R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : NonAssocRing A
inst✝ : IsSimpleRing A
I : TwoSidedIdeal A
x : A
hx : x ≠ 0
hxI : x ∈ I
⊢ I ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ I = ⊥ ∨ I = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
⊢ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
H : ∀ {S : Type u} [inst : NonAssocSemiring S] (f : R →+* S), Function.Injective ⇑f ∨ Subsingleton S
x✝² : Type u
x✝¹ : NonAssocSemiring x✝²
x✝ : Nontrivial x✝²
f : R →+* x✝²
⊢ ¬Subsingleton x✝²

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon } ≤ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon } ≤ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ J
h2 : I ≤ K
⊢ I ≤ { ringCon := J.ringCon ⊓ K.ringCon }

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ x✝ ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ ⊥ ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
h : 1 ∈ I
x : R
x✝ : x ∈ ⊤
⊢ x ∈ I

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
⊢ ↑(restrictScalars R ⊤) = ↑⊤

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ U ↔ x ∈ V

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ Submodule.restrictScalars R 1 = toSubmodule S

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ Codisjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Codisjoint (toSubmodule S) (Submodule.restrictScalars R I)

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ Disjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Disjoint (toSubmodule S) (Submodule.restrictScalars R I)

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (↑(toAlgHom R (↥S) A)).range = toSubmodule S

Tactic:
by

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
⊢ ∑ i, (of β i) (x i) = x

Tactic:
by

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
by

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ f = (toAddMonoid fun i ↦ ψ.comp (of β i)) f

Tactic:
by

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ fromAddMonoid ((of (fun i ↦ γ →+ β i) i) f) = (of β i).comp f

Tactic:
by

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ (fromAddMonoid ((of (fun i ↦ γ →+ β i) i) f)) x = (of β i) (f x)

Tactic:
by

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

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) 0) = 0

Tactic:
by

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

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) ((of (fun i ↦ M) p) x)) = (of (fun i ↦ M) p) x

Tactic:
by

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

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ x y : ⨁ (i : ι), M
ihx : (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) x) = x
ihy : (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) y) = y
⊢ (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) (x + y)) = x + y

Tactic:
by

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

Goal state before:
pp: M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (DirectSum.id M ι) x = x default

Tactic:
by

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

Goal state before:
pp: ι₁ ι₂ : Type v
inst✝² : DecidableEq ι₂
f : ι₁ → ι₂
β : ι₁ → Type w
inst✝¹ : (i : ι₁) → AddCommMonoid (β i)
inst✝ : DecidableEq ι₁
i : ι₁
x : β i
h : (y : ι₂) × { x // f x = y } ≃ ι₁ := Equiv.sigmaFiberEquiv f
k : (j : ι₂) × { i₁ // f i₁ = j } := ⟨f i, ⟨i, ⋯⟩⟩
⊢ (sigmaFiberAddEquiv f) ((of β (h k)) x) = sigmaCurry ((of (fun k ↦ β ↑k.snd) k) x)

Tactic:
by

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

Goal state before:
pp: ι₁ ι₂ : Type v
inst✝² : DecidableEq ι₂
f : ι₁ → ι₂
β : ι₁ → Type w
inst✝¹ : (i : ι₁) → AddCommMonoid (β i)
inst✝ : DecidableEq ι₁
i : ι₁
x : β i
h : (y : ι₂) × { x // f x = y } ≃ ι₁ := Equiv.sigmaFiberEquiv f
k : (j : ι₂) × { i₁ // f i₁ = j } := ⟨f i, ⟨i, ⋯⟩⟩
⊢ sigmaCurry ((of (fun k ↦ β ↑k.snd) k) x) =
    (of (fun i ↦ ⨁ (j : { i_1 // f i_1 = i }), β ↑j) k.fst) ((of (fun i ↦ β ↑i) k.snd) x)

Tactic:
by

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

Goal state before:
pp: ι : Type v
inst✝⁴ : DecidableEq ι
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun i x ↦ ↑x

Tactic:
by

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

Goal state before:
pp: case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ 0 = ↑0

Tactic:
ZeroMemClass.coe_zero

Goal state after:
case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ 0 = 0
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
by

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

Goal state before:
pp: ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
by

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

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike S M
inst✝² : AddSubmonoidClass S M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (support fun i ↦ ↑(x i)) ⊆ ↑(DFinsupp.support x)

Tactic:
by

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

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ HasFiniteSupport fun i ↦ ↑(x i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (α i)
inst✝ : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → α i →+ β i
⊢ Injective ⇑(map f) ↔ ∀ (i : ι), Injective ⇑(f i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (α i)
inst✝ : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → α i →+ β i
⊢ Surjective ⇑(map f) ↔ ∀ (i : ι), Surjective ⇑(f i)

Tactic:
by

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

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
⊢ (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
⊢ ↑(Subalgebra.toSubmodule (sInf S)) = ↑(sInf (⇑Subalgebra.toSubmodule '' S))

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
⊢ ↑(sInf S).toSubsemiring = ↑(sInf (Subalgebra.toSubsemiring '' S))

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (α i)
inst✝ : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → α i →+ β i
x y : ⨁ (i : ι), α i
⊢ (map f) x = (map f) y ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S

Tactic:
by

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

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
ι : Type u_1
inst✝¹ : Fintype ι
G : ι → Type u_2
inst✝ : (i : ι) → AddCommMonoid (G i)
g h : DirectSum ι G
x✝ : ι
⊢ DFinsupp.equivFunOnFintype.toFun (g + h) x✝ =
    (DFinsupp.equivFunOnFintype.toFun g + DFinsupp.equivFunOnFintype.toFun h) x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

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
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ Subalgebra.map f (iInf s) = ⨅ i, Subalgebra.map f (s i)

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ ↑(toSubmodule (⨅ i, S i)) = ↑(⨅ i, toSubmodule (S i))

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
⊢ (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
⊢ motive x

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r) ⋯
⊢ motive x mem

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
R : Subring A
⊢ ⊥.toSubring = R

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

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
x✝ t : NonUnitalSubalgebra R A
s : NonUnitalSubsemiring A
hs : ∀ (c : R) {x : A}, x ∈ s.carrier → c • x ∈ s.carrier
⊢ { toNonUnitalSubsemiring := s, smul_mem' := hs }.toNonUnitalSubsemiring = t.toNonUnitalSubsemiring →
    { toNonUnitalSubsemiring := s, smul_mem' := hs } = 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
f : A →ₐ[R] B
⊢ Subalgebra.toSubmodule (Subalgebra.map f ⊥) = Subalgebra.toSubmodule ⊥

Tactic:
by

Goal state after: