Theorem: TrivSqZeroExt.sqZero (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ kerIdeal R M ^ 2 = ⊥
Tactic:
simp only [pow_two, zero_eq_bot, eq_bot_iff, mul_le, mem_kerIdeal_iff_inr]
State after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (r : TrivSqZeroExt R M), r = inr r.snd → ∀ (s : TrivSqZeroExt R M), s = inr s.snd → r * s ∈ ⊥

State before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (r : TrivSqZeroExt R M), r = inr r.snd → ∀ (s : TrivSqZeroExt R M), s = inr s.snd → r * s ∈ ⊥
Tactic:
rintro x hx y hy
State after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ x * y ∈ ⊥

State before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ x * y ∈ ⊥
Tactic:
rw [hx, hy, mem_bot, inr_mul_inr]
State after:
no goals