case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ IsNontrivial (ringHomComp χ f)
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsNontrivial χ
f : R' →+* R''
hf : Function.Injective ↑f
⊢ IsNontrivial (ringHomComp χ f)
obtain ⟨a, ha⟩ := hχ
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ ↑(ringHomComp χ f) ↑a ≠ 1
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ IsNontrivial (ringHomComp χ f)
use a
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ ↑f (↑χ ↑a) ≠ ↑f 1
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ ↑(ringHomComp χ f) ↑a ≠ 1
rw [ringHomComp_apply, ← RingHom.map_one f]
no goals
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ ↑f (↑χ ↑a) ≠ ↑f 1
exact fun h => ha (hf h)