Theorem: map_two (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ f 2 = 2
Tactic:
rw [← one_add_one_eq_two, map_add, map_one]
State after:
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ 1 + 1 = 2

State before:
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ 1 + 1 = 2
Tactic:
exact one_add_one_eq_two
State after:
no goals