-- Mathlib/Analysis/Normed/Algebra/Unitization.lean
theorem splitMul_injective_of_clm_mul_injective
    (h : Function.Injective (mul 𝕜 A)) :
    Function.Injective (splitMul 𝕜 A)

Proof state:
case inl_add_inr.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (mul 𝕜 A) a✝ = (mul 𝕜 A) 0
⊢ ↑a✝ = 0

Tactic:
rw [h hx, inr_zero]

Result:
no goals

Proof state:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : r✝ = 0 ∧ (algebraMap 𝕜 (A →L[𝕜] A)) r✝ + (mul 𝕜 A) a✝ = 0
⊢ inl r✝ + ↑a✝ = 0

Tactic:
obtain ⟨rfl, hx⟩ := hx

Result:
case inl_add_inr.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (algebraMap 𝕜 (A →L[𝕜] A)) 0 + (mul 𝕜 A) a✝ = 0
⊢ inl 0 + ↑a✝ = 0

Proof state:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : (splitMul 𝕜 A) (inl r✝ + ↑a✝) = 0
⊢ inl r✝ + ↑a✝ = 0

Tactic:
rw [map_add] at hx

Result:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : (splitMul 𝕜 A) (inl r✝) + (splitMul 𝕜 A) ↑a✝ = 0
⊢ inl r✝ + ↑a✝ = 0

Proof state:
case inl_add_inr.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (mul 𝕜 A) a✝ = 0
⊢ ↑a✝ = 0

Tactic:
rw [← map_zero (mul 𝕜 A)] at hx

Result:
case inl_add_inr.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (mul 𝕜 A) a✝ = (mul 𝕜 A) 0
⊢ ↑a✝ = 0

Proof state:
case inl_add_inr.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (algebraMap 𝕜 (A →L[𝕜] A)) 0 + (mul 𝕜 A) a✝ = 0
⊢ inl 0 + ↑a✝ = 0

Tactic:
simp only [map_zero, zero_add, inl_zero] at hx ⊢

Result:
case inl_add_inr.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
a✝ : A
hx : (mul 𝕜 A) a✝ = 0
⊢ ↑a✝ = 0

Proof state:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : (splitMul 𝕜 A) (inl r✝) + (splitMul 𝕜 A) ↑a✝ = 0
⊢ inl r✝ + ↑a✝ = 0

Tactic:
simp only [splitMul_apply, fst_inl, snd_inl, map_zero, add_zero, fst_inr, snd_inr,
  zero_add, Prod.mk_add_mk, Prod.mk_eq_zero] at hx

Result:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : r✝ = 0 ∧ (algebraMap 𝕜 (A →L[𝕜] A)) r✝ + (mul 𝕜 A) a✝ = 0
⊢ inl r✝ + ↑a✝ = 0

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
⊢ ∀ (a : Unitization 𝕜 A), (splitMul 𝕜 A) a = 0 → a = 0

Tactic:
intro x hx

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
x : Unitization 𝕜 A
hx : (splitMul 𝕜 A) x = 0
⊢ x = 0

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
⊢ Function.Injective ⇑(splitMul 𝕜 A)

Tactic:
rw [injective_iff_map_eq_zero]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
⊢ ∀ (a : Unitization 𝕜 A), (splitMul 𝕜 A) a = 0 → a = 0

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
x : Unitization 𝕜 A
hx : (splitMul 𝕜 A) x = 0
⊢ x = 0

Tactic:
induction x

Result:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : (splitMul 𝕜 A) (inl r✝ + ↑a✝) = 0
⊢ inl r✝ + ↑a✝ = 0