Theorem: TrivSqZeroExt.mem_kerIdeal_iff_exists (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
x : TrivSqZeroExt R M
⊢ x ∈ kerIdeal R M ↔ ∃ m, x = inr m
Tactic:
rw [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
x : TrivSqZeroExt R M
⊢ x = inr x.snd ↔ ∃ m, x = inr m

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
⊢ x = inr x.snd ↔ ∃ m, x = inr m
Tactic:
exact ⟨fun h => ⟨x.snd, h⟩, fun ⟨m, hm⟩ => by rw [hm]; rfl⟩
State after:
no goals

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
x✝ : ∃ m, x = inr m
m : M
hm : x = inr m
⊢ x = inr x.snd
Tactic:
rw [hm]
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
x✝ : ∃ m, x = inr m
m : M
hm : x = inr m
⊢ inr m = inr (inr m).snd

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
x✝ : ∃ m, x = inr m
m : M
hm : x = inr m
⊢ inr m = inr (inr m).snd
Tactic:
rfl
State after:
no goals