case h.e'_3.h
α : Type ?u.317239
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
x✝ : ℕ
⊢ (natAbs ∘ (fun x x_1 => x ^ x_1) x) x✝ = natAbs x ^ x✝
α : Type ?u.317239
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
⊢ Function.Injective (natAbs ∘ (fun x x_1 => x ^ x_1) x)
convert Nat.pow_right_injective h using 2
no goals
case h.e'_3.h
α : Type ?u.317239
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
x✝ : ℕ
⊢ (natAbs ∘ (fun x x_1 => x ^ x_1) x) x✝ = natAbs x ^ x✝
rw [Function.comp_apply, natAbs_pow]
no goals
α : Type ?u.317239
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
this : Function.Injective (natAbs ∘ (fun x x_1 => x ^ x_1) x)
⊢ Function.Injective ((fun x x_1 => x ^ x_1) x)
exact Function.Injective.of_comp this