[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ n : R
⊢ (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ n : R
⊢ (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ n : R
⊢ a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ n : R
⊢ a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ n : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
        (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
      (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ n : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) *
      (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 +
                  (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 +
                (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 +
              (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 +
            (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 +
          (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 +
        (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 +
      (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2
[PROOFSTEP]
ring


[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff R p x]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑x = 0 ↔ ↑x = 0
[PROOFSTEP]
change algebraMap ℕ A x = 0 ↔ algebraMap ℕ R x = 0
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑(algebraMap ℕ A) x = 0 ↔ ↑(algebraMap ℕ R) x = 0
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply ℕ R A x]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = 0 ↔ ↑(algebraMap ℕ R) x = 0
[PROOFSTEP]
refine' Iff.trans _ h.eq_iff
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = 0 ↔ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap R A) 0
[PROOFSTEP]
rw [RingHom.map_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑x = ↑y
⊢ x = y
[PROOFSTEP]
change algebraMap ℕ A x = algebraMap ℕ A y at hxy
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap ℕ A) x = ↑(algebraMap ℕ A) y
⊢ x = y
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply ℕ R A x] at hxy
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap ℕ A) y
⊢ x = y
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply ℕ R A y] at hxy
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap R A) (↑(algebraMap ℕ R) y)
⊢ x = y
[PROOFSTEP]
exact CharZero.cast_injective (h hxy)
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ ringChar K = ringChar L
[PROOFSTEP]
rw [ringChar.eq_iff, Algebra.charP_iff K L]
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ CharP L (ringChar L)
[PROOFSTEP]
apply ringChar.charP


[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
⊢ q = 0 ∨ IsPrimePow q
[PROOFSTEP]
apply or_iff_not_imp_left.2
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
⊢ ¬q = 0 → IsPrimePow q
[PROOFSTEP]
intro q_pos
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
⊢ IsPrimePow q
[PROOFSTEP]
let K := LocalRing.ResidueField R
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
⊢ IsPrimePow q
[PROOFSTEP]
haveI RM_char := ringChar.charP K
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
⊢ IsPrimePow q
[PROOFSTEP]
let r := ringChar K
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
⊢ IsPrimePow q
[PROOFSTEP]
let n := q.factorization r
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
⊢ IsPrimePow q
[PROOFSTEP]
cases' CharP.char_is_prime_or_zero K r with r_prime r_zero
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
⊢ IsPrimePow q
[PROOFSTEP]
let a := q / r ^ n
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
⊢ IsPrimePow q
[PROOFSTEP]
have q_eq_a_mul_rn : q = r ^ n * a := by rw [Nat.mul_div_cancel' (Nat.ord_proj_dvd q r)]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
⊢ q = r ^ n * a
[PROOFSTEP]
rw [Nat.mul_div_cancel' (Nat.ord_proj_dvd q r)]
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
⊢ IsPrimePow q
[PROOFSTEP]
have r_ne_dvd_a := Nat.not_dvd_ord_compl r_prime q_pos
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
⊢ IsPrimePow q
[PROOFSTEP]
have rn_dvd_q : r ^ n ∣ q := ⟨a, q_eq_a_mul_rn⟩
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
⊢ IsPrimePow q
[PROOFSTEP]
rw [mul_comm] at q_eq_a_mul_rn
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
⊢ IsPrimePow q
[PROOFSTEP]
have a_unit : IsUnit (a : R) := by
  by_contra g
  rw [← mem_nonunits_iff] at g
  rw [← LocalRing.mem_maximalIdeal] at g
  have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
  rw [map_natCast] at a_cast_zero
  have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
  exact absurd r_dvd_a r_ne_dvd_a
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
⊢ IsUnit ↑a
[PROOFSTEP]
by_contra g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g : ¬IsUnit ↑a
⊢ False
[PROOFSTEP]
rw [← mem_nonunits_iff] at g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ nonunits R
⊢ False
[PROOFSTEP]
rw [← LocalRing.mem_maximalIdeal] at g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
⊢ False
[PROOFSTEP]
have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
a_cast_zero : ↑(Ideal.Quotient.mk (LocalRing.maximalIdeal R)) ↑a = 0
⊢ False
[PROOFSTEP]
rw [map_natCast] at a_cast_zero
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
⊢ False
[PROOFSTEP]
have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
r_dvd_a : ringChar K ∣ a
⊢ False
[PROOFSTEP]
exact absurd r_dvd_a r_ne_dvd_a
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
⊢ IsPrimePow q
[PROOFSTEP]
cases' a_unit.exists_left_inv with a_inv h_inv_mul_a
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
⊢ IsPrimePow q
[PROOFSTEP]
have rn_cast_zero : ↑(r ^ n) = (0 : R) :=
  by
  rw [← @mul_one R _ (r ^ n), mul_comm, ← Classical.choose_spec a_unit.exists_left_inv, mul_assoc, ← Nat.cast_mul, ←
    q_eq_a_mul_rn, CharP.cast_eq_zero R q]
  simp
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
⊢ ↑(r ^ n) = 0
[PROOFSTEP]
rw [← @mul_one R _ (r ^ n), mul_comm, ← Classical.choose_spec a_unit.exists_left_inv, mul_assoc, ← Nat.cast_mul, ←
  q_eq_a_mul_rn, CharP.cast_eq_zero R q]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
⊢ Classical.choose (_ : ∃ b, b * ↑a = 1) * 0 = 0
[PROOFSTEP]
simp
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
⊢ IsPrimePow q
[PROOFSTEP]
have q_eq_rn := Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero) rn_dvd_q
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
⊢ IsPrimePow q
[PROOFSTEP]
have n_pos : n ≠ 0 := fun n_zero =>
  absurd (by simpa [n_zero] using q_eq_rn)
    (CharP.char_ne_one R q)
      -- Definition of prime power: `∃ r n, Prime r ∧ 0 < n ∧ r ^ n = q`.
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_zero : n = 0
⊢ q = 1
[PROOFSTEP]
simpa [n_zero] using q_eq_rn
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_pos : n ≠ 0
⊢ IsPrimePow q
[PROOFSTEP]
exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
⊢ IsPrimePow q
[PROOFSTEP]
haveI K_char_p_0 := ringChar.of_eq r_zero
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
⊢ IsPrimePow q
[PROOFSTEP]
haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
⊢ IsPrimePow q
[PROOFSTEP]
haveI R_char_zero :=
  RingHom.charZero
    (LocalRing.residue R)
      -- Finally, `r = 0` would lead to a contradiction:
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
⊢ IsPrimePow q
[PROOFSTEP]
have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
q_zero : q = 0
⊢ IsPrimePow q
[PROOFSTEP]
exact absurd q_zero q_pos


[GOAL]
R : Type u
inst✝ : Semiring R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
⊢ q = 1
[PROOFSTEP]
cases' hq with q hq_one hq_prime hq_hchar
[GOAL]
case zero
R : Type u
inst✝ : Semiring R
hp : CharP R 0
q : CharZero R
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case prime
R : Type u
inst✝ : Semiring R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hq_hchar : CharP R q
⊢ q = 1
[PROOFSTEP]
exact False.elim (lt_irrefl _ ((hp.eq R hq_hchar).symm ▸ hq_prime : (0 : ℕ).Prime).pos)
[GOAL]
R : Type u
inst✝ : Semiring R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
⊢ p = q ↔ Nat.Prime p
[PROOFSTEP]
cases' hq with q hq_one hq_prime hq_hchar
[GOAL]
case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ p = 1 ↔ Nat.Prime p
[PROOFSTEP]
rw [(CharP.eq R hp inferInstance : p = 0)]
[GOAL]
case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ 0 = 1 ↔ Nat.Prime 0
[PROOFSTEP]
decide
[GOAL]
case prime
R : Type u
inst✝ : Semiring R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hq_hchar : CharP R q
⊢ p = q ↔ Nat.Prime p
[PROOFSTEP]
exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp hq_hchar⟩
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hq : ExpChar R 1
⊢ p = 0
[PROOFSTEP]
cases hq
[GOAL]
case zero
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0
[PROOFSTEP]
exact CharP.eq R hp inferInstance
[GOAL]
case prime
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0
[PROOFSTEP]
exact False.elim (CharP.char_ne_one R 1 rfl)
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hq : ExpChar R 1
⊢ CharZero R
[PROOFSTEP]
cases hq
[GOAL]
case zero
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R
[PROOFSTEP]
assumption
[GOAL]
case prime
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R
[PROOFSTEP]
exact False.elim (CharP.char_ne_one R 1 rfl)
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 ↔ p = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 → p = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R 1
⊢ p = 0
[PROOFSTEP]
exact char_zero_of_expChar_one R p
[GOAL]
case mpr
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
q : ℕ
inst✝¹ : ExpChar R q
inst✝ : CharP R 0
⊢ q = 1
[PROOFSTEP]
exact expChar_one_of_char_zero R q
[GOAL]
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
⊢ Nat.Prime p
[PROOFSTEP]
cases' CharP.char_is_prime_or_zero R p with h h
[GOAL]
case inl
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
h : Nat.Prime p
⊢ Nat.Prime p
[PROOFSTEP]
exact h
[GOAL]
case inr
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
h : p = 0
⊢ Nat.Prime p
[PROOFSTEP]
contradiction
[GOAL]
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hq : ExpChar R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
cases hq
[GOAL]
case zero
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1
case prime
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hprime✝ : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
case zero => exact .inr rfl
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1
[PROOFSTEP]
case zero => exact .inr rfl
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1
[PROOFSTEP]
exact .inr rfl
[GOAL]
case prime
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hprime✝ : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
case prime hp _ => exact .inl hp
[GOAL]
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hp : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
case prime hp _ => exact .inl hp
[GOAL]
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hp : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
exact .inl hp


[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
q : Submodule R M
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h : (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ } = (fun s => s.carrier) q
⊢ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
toAddSubmonoid✝¹ : AddSubmonoid M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
⊢ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAddSubmonoid
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
toAddSubmonoid✝¹ : AddSubmonoid M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p✝ q p : Submodule R M
s : Set M
hs : s = ↑p
⊢ 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier
[PROOFSTEP]
simpa [hs] using p.zero_mem'
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p✝ q p : Submodule R M
s : Set M
hs : s = ↑p
⊢ ∀ (c : R) {x : M},
    x ∈
        { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := s,
                        add_mem' :=
                          (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := s,
                        add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa [hs] using p.smul_mem'
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
⊢ a • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
⊢ ↑(a • 0) = ↑0
[PROOFSTEP]
simp
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x✝ y✝ : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
x y : { x // x ∈ p }
⊢ a • (x + y) = a • x + a • y
[PROOFSTEP]
ext
[GOAL]
case a
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x✝ y✝ : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
x y : { x // x ∈ p }
⊢ ↑(a • (x + y)) = ↑(a • x + a • y)
[PROOFSTEP]
simp [smul_add]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x✝ y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a b : S
x : { x // x ∈ p }
⊢ (a + b) • x = a • x + b • x
[PROOFSTEP]
ext
[GOAL]
case a
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x✝ y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a b : S
x : { x // x ∈ p }
⊢ ↑((a + b) • x) = ↑(a • x + b • x)
[PROOFSTEP]
simp [add_smul]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : { x // x ∈ p }
⊢ 0 • a = 0
[PROOFSTEP]
ext
[GOAL]
case a
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : { x // x ∈ p }
⊢ ↑(0 • a) = ↑0
[PROOFSTEP]
simp
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ { x // x ∈ p } →ₗ[R] M
[PROOFSTEP]
refine' { toFun := Subtype.val .. }
[GOAL]
case refine'_1
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (x y : { x // x ∈ p }), ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
simp [coe_smul]
[GOAL]
case refine'_2
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (r : R) (x : { x // x ∈ p }),
    AddHom.toFun { toFun := Subtype.val, map_add' := (_ : ∀ (a a_1 : { x // x ∈ p }), ↑a + ↑a_1 = ↑a + ↑a_1) } (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := Subtype.val, map_add' := (_ : ∀ (a a_1 : { x // x ∈ p }), ↑a + ↑a_1 = ↑a + ↑a_1) } x
[PROOFSTEP]
simp [coe_smul]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
module_M : Module R M
p✝ q : Submodule R M
r : R
x y : M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p : Submodule R M
⊢ Module R { x // x ∈ p }
[PROOFSTEP]
infer_instance
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
⊢ ∀ {a b : Submodule R M},
    ↑{ toFun := restrictScalars S, inj' := (_ : Injective (restrictScalars S)) } a ≤
        ↑{ toFun := restrictScalars S, inj' := (_ : Injective (restrictScalars S)) } b ↔
      a ≤ b
[PROOFSTEP]
simp [SetLike.le_def]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
r : R
x y : M
hy : y ∈ p
⊢ x - y ∈ p ↔ x ∈ p
[PROOFSTEP]
rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
r : R
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p
[PROOFSTEP]
rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : ι → M
x : M
N : Submodule R M
ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0
⊢ ¬x ∈ N
[PROOFSTEP]
intro hx
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : ι → M
x : M
N : Submodule R M
ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0
hx : x ∈ N
⊢ False
[PROOFSTEP]
simpa using ortho (-1) x hx


[GOAL]
ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
j : ι
⊢ ↑(Pi.evalRingHom (fun x => R) j) ↑x = 0
[PROOFSTEP]
rw [map_natCast, h]
[GOAL]
ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
⊢ ↑(Pi.evalRingHom (fun x => R) i) ↑x = 0
[PROOFSTEP]
rw [h, RingHom.map_zero]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
xs : List (FreeMonoid α)
⊢ ↑toList (List.prod xs) = List.join (List.map (↑toList) xs)
[PROOFSTEP]
induction xs
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
⊢ ↑toList (List.prod []) = List.join (List.map ↑toList [])
[PROOFSTEP]
simp [*, List.join]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
head✝ : FreeMonoid α
tail✝ : List (FreeMonoid α)
tail_ih✝ : ↑toList (List.prod tail✝) = List.join (List.map (↑toList) tail✝)
⊢ ↑toList (List.prod (head✝ :: tail✝)) = List.join (List.map (↑toList) (head✝ :: tail✝))
[PROOFSTEP]
simp [*, List.join]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
xs : List (List α)
⊢ ↑toList (↑ofList (List.join xs)) = ↑toList (List.prod (List.map (↑ofList) xs))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
f g : FreeMonoid α →* M
h : ∀ (x : α), ↑f (of x) = ↑g (of x)
l : FreeMonoid α
x : α
xs : FreeMonoid α
hxs : ↑f xs = ↑g xs
⊢ ↑f (of x * xs) = ↑g (of x * xs)
[PROOFSTEP]
simp only [h, hxs, MonoidHom.map_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
f : α → M
x✝¹ x✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun l => prodAux (List.map f (↑toList l)),
        map_one' :=
          (_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
      (x✝¹ * x✝) =
    OneHom.toFun
        { toFun := fun l => prodAux (List.map f (↑toList l)),
          map_one' :=
            (_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
        x✝¹ *
      OneHom.toFun
        { toFun := fun l => prodAux (List.map f (↑toList l)),
          map_one' :=
            (_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
        x✝
[PROOFSTEP]
simp only [prodAux_eq, toList_mul, List.map_append, List.prod_append]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
⊢ MonoidHom.comp g (↑lift f) = ↑lift (↑g ∘ f)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
x✝ : α
⊢ ↑(MonoidHom.comp g (↑lift f)) (of x✝) = ↑(↑lift (↑g ∘ f)) (of x✝)
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ↑(countp p) (of x) = if p x = (true = true) then 1 else 0
[PROOFSTEP]
simp [countp, List.countp, List.countp.go]
[GOAL]
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
x y : α
⊢ ↑(count x) (of y) = Pi.single x 1 y
[PROOFSTEP]
simp [Pi.single, Function.update, count, countp, List.countp, List.countp.go, Bool.beq_eq_decide_eq]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ↑(countp p) (of x) = if p x then ↑Multiplicative.ofAdd 1 else ↑Multiplicative.ofAdd 0
[PROOFSTEP]
erw [FreeAddMonoid.countp_of]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if p x = (true = true) then 1 else 0) = if p x then ↑Multiplicative.ofAdd 1 else ↑Multiplicative.ofAdd 0
[PROOFSTEP]
simp only [eq_iff_iff, iff_true, ofAdd_zero]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if p x then 1 else 0) = if p x then ↑Multiplicative.ofAdd 1 else 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ↑(countp p) (of x) = if p x then ↑Multiplicative.ofAdd 1 else 1
[PROOFSTEP]
rw [countp_of', ofAdd_zero]
[GOAL]
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
x y : α
⊢ ↑(count x) (of y) = Pi.mulSingle x (↑Multiplicative.ofAdd 1) y
[PROOFSTEP]
simp [count, countp_of, Pi.mulSingle_apply, eq_comm, Bool.beq_eq_decide_eq]


[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : M
hab : a ≤ b
⊢ a ^ 0 ≤ b ^ 0
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ (k + 1) ≤ b ^ (k + 1)
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : M
hab : a ≤ b
k : ℕ
⊢ a * a ^ k ≤ b * b ^ k
[PROOFSTEP]
exact mul_le_mul' hab (pow_le_pow_of_le_left' hab k)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
H : 1 ≤ a
⊢ 1 ≤ a ^ 0
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
H : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
H : 1 ≤ a
k : ℕ
⊢ 1 ≤ a * a ^ k
[PROOFSTEP]
exact one_le_mul H (one_le_pow_of_one_le' H k)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
n m : ℕ
ha : 1 ≤ a
h : n ≤ m
k : ℕ
hk : n + k = m
⊢ a ^ n * a ^ k = a ^ m
[PROOFSTEP]
rw [← hk, pow_add]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
k : ℕ
hk : k ≠ 0
⊢ 1 < a ^ k
[PROOFSTEP]
rcases Nat.exists_eq_succ_of_ne_zero hk with ⟨l, rfl⟩
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
hk : Nat.succ l ≠ 0
⊢ 1 < a ^ Nat.succ l
[PROOFSTEP]
clear hk
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
⊢ 1 < a ^ Nat.succ l
[PROOFSTEP]
induction' l with l IH
[GOAL]
case intro.zero
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
⊢ 1 < a ^ Nat.succ Nat.zero
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case intro.zero
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
⊢ 1 < a * a ^ Nat.zero
[PROOFSTEP]
simpa using ha
[GOAL]
case intro.succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
IH : 1 < a ^ Nat.succ l
⊢ 1 < a ^ Nat.succ (Nat.succ l)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case intro.succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
IH : 1 < a ^ Nat.succ l
⊢ 1 < a * a ^ (l + 1)
[PROOFSTEP]
exact one_lt_mul'' ha IH
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n m : ℕ
ha : 1 < a
h : n < m
⊢ a ^ n < a ^ m
[PROOFSTEP]
rcases Nat.le.dest h with ⟨k, rfl⟩
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
h : n < Nat.succ n + k
⊢ a ^ n < a ^ (Nat.succ n + k)
[PROOFSTEP]
clear h
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
⊢ a ^ n < a ^ (Nat.succ n + k)
[PROOFSTEP]
rw [pow_add, pow_succ', mul_assoc, ← pow_succ]
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
⊢ a ^ n < a ^ n * a ^ (k + 1)
[PROOFSTEP]
exact lt_mul_of_one_lt_right' _ (one_lt_pow' ha k.succ_ne_zero)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x * x ^ n
[PROOFSTEP]
exact Left.one_le_mul hx <| Left.one_le_pow_of_le hx
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : x ≤ 1
n : ℕ
⊢ x ^ (n + 1) ≤ 1
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : x ≤ 1
n : ℕ
⊢ x * x ^ n ≤ 1
[PROOFSTEP]
exact Left.mul_le_one hx <| Left.pow_le_one_of_le hx
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x * x ^ n
[PROOFSTEP]
exact Right.one_le_mul hx <| Right.one_le_pow_of_le hx
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : x ≤ 1
n : ℕ
⊢ x ^ (n + 1) ≤ 1
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : x ≤ 1
n : ℕ
⊢ x * x ^ n ≤ 1
[PROOFSTEP]
exact Right.mul_le_one hx <| Right.pow_le_one_of_le hx
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
f : β → M
hf : StrictMono f
x✝ : 1 ≠ 0
⊢ StrictMono fun a => f a ^ 1
[PROOFSTEP]
simpa
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
f : β → M
hf : StrictMono f
n : ℕ
x✝ : Nat.succ (Nat.succ n) ≠ 0
⊢ StrictMono fun a => f a ^ Nat.succ (Nat.succ n)
[PROOFSTEP]
simp_rw [pow_succ _ (n + 1)]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
f : β → M
hf : StrictMono f
n : ℕ
x✝ : Nat.succ (Nat.succ n) ≠ 0
⊢ StrictMono fun a => f a * f a ^ (n + 1)
[PROOFSTEP]
exact hf.mul' (StrictMono.pow_right' hf n.succ_ne_zero)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : β → M
hf : Monotone f
⊢ Monotone fun a => f a ^ 0
[PROOFSTEP]
simpa using monotone_const
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a ^ (n + 1)
[PROOFSTEP]
simp_rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a * f a ^ n
[PROOFSTEP]
exact hf.mul' (Monotone.pow_right hf _)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
n✝ : ℕ
x : M
hn : 0 < n✝
h : x < 1
n : ℕ
x✝ : Nat.succ 0 ≤ n
ih : x ^ n < 1
⊢ x ^ (n + 1) < 1
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
n✝ : ℕ
x : M
hn : 0 < n✝
h : x < 1
n : ℕ
x✝ : Nat.succ 0 ≤ n
ih : x ^ n < 1
⊢ x * x ^ n < 1
[PROOFSTEP]
exact mul_lt_one h ih
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
n✝ : ℕ
x : M
hn : 0 < n✝
h : x < 1
n : ℕ
x✝ : Nat.succ 0 ≤ n
ih : x ^ n < 1
⊢ x ^ (n + 1) < 1
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
n✝ : ℕ
x : M
hn : 0 < n✝
h : x < 1
n : ℕ
x✝ : Nat.succ 0 ≤ n
ih : x ^ n < 1
⊢ x * x ^ n < 1
[PROOFSTEP]
exact Right.mul_lt_one h ih
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n = 1 ↔ x = 1
[PROOFSTEP]
simp only [le_antisymm_iff]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n ≤ 1 ∧ 1 ≤ x ^ n ↔ x ≤ 1 ∧ 1 ≤ x
[PROOFSTEP]
rw [pow_le_one_iff hn, one_le_pow_iff hn]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : M
h : a * b < c * d
⊢ min a b ^ 2 < max c d ^ 2
[PROOFSTEP]
simp_rw [pow_two]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : M
h : a * b < c * d
⊢ min a b * min a b < max c d * max c d
[PROOFSTEP]
exact (mul_le_mul' inf_le_left inf_le_right).trans_lt (h.trans_le <| mul_le_mul' le_sup_left le_sup_right)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : M
h : a * b < c ^ 2
⊢ min a b < c
[PROOFSTEP]
simpa using min_lt_max_of_mul_lt_mul (h.trans_eq <| pow_two _)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : M
h : a ^ 2 < b * c
⊢ a < max b c
[PROOFSTEP]
simpa using min_lt_max_of_mul_lt_mul ((pow_two _).symm.trans_lt h)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : M
h : a * b ≤ c ^ 2
⊢ min a b ≤ c
[PROOFSTEP]
simpa using min_le_max_of_mul_le_mul (h.trans_eq <| pow_two _)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : M
h : a ^ 2 ≤ b * c
⊢ a ≤ max b c
[PROOFSTEP]
simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : G
H : 1 ≤ x
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ x ^ n
[PROOFSTEP]
lift n to ℕ using hn
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n
[PROOFSTEP]
apply one_le_pow_of_one_le' H
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m n : ℕ
⊢ 0 ^ (n + 1) ≤ 1
[PROOFSTEP]
rw [zero_pow n.succ_pos]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m n : ℕ
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
hn : n ≠ 0
⊢ x ^ n + y ^ n ≤ (x + y) ^ n
[PROOFSTEP]
rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
[GOAL]
case intro
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn : Nat.succ k ≠ 0
⊢ x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case intro.zero
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
⊢ x ^ Nat.succ Nat.zero + y ^ Nat.succ Nat.zero ≤ (x + y) ^ Nat.succ Nat.zero
[PROOFSTEP]
have eqn : Nat.succ Nat.zero = 1 := rfl
[GOAL]
case intro.zero
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
eqn : Nat.succ Nat.zero = 1
⊢ x ^ Nat.succ Nat.zero + y ^ Nat.succ Nat.zero ≤ (x + y) ^ Nat.succ Nat.zero
[PROOFSTEP]
rw [eqn]
[GOAL]
case intro.zero
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
eqn : Nat.succ Nat.zero = 1
⊢ x ^ 1 + y ^ 1 ≤ (x + y) ^ 1
[PROOFSTEP]
simp only [pow_one, le_refl]
[GOAL]
case intro.succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
[PROOFSTEP]
let n := k.succ
[GOAL]
case intro.succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
[PROOFSTEP]
have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
[GOAL]
case intro.succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
[PROOFSTEP]
have h2 := add_nonneg hx hy
[GOAL]
case intro.succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
[PROOFSTEP]
calc
  x ^ n.succ + y ^ n.succ ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) :=
    by
    rw [pow_succ _ n, pow_succ _ n]
    exact le_add_of_nonneg_right h1
  _ = (x + y) * (x ^ n + y ^ n) := by
    rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc, add_assoc (x * x ^ n) (x * y ^ n),
      add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
  _ ≤ (x + y) ^ n.succ := by
    rw [pow_succ _ n]
    exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ Nat.succ n + y ^ Nat.succ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
[PROOFSTEP]
rw [pow_succ _ n, pow_succ _ n]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
[PROOFSTEP]
exact le_add_of_nonneg_right h1
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
[PROOFSTEP]
rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc, add_assoc (x * x ^ n) (x * y ^ n),
  add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ _ n]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ^ (n + 1) < 1
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1
[PROOFSTEP]
exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one _ h₀ h₁.le)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n m : ℕ
H : 1 ≤ a
⊢ 1 ≤ a ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
H : 1 ≤ a
n : ℕ
⊢ 1 ≤ a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
H : 1 ≤ a
n : ℕ
⊢ 1 ≤ a * a ^ n
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le H n) zero_le_one (le_trans zero_le_one H)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a * a ^ n
[PROOFSTEP]
exact le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
⊢ ∀ (i : ℕ), a ^ i ≤ b ^ i
[PROOFSTEP]
intro i
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
i : ℕ
⊢ a ^ i ≤ b ^ i
[PROOFSTEP]
induction i with
| zero => simp
| succ k ih =>
  rw [pow_succ, pow_succ]
  apply mul_le_mul hab
  apply ih
  apply pow_nonneg ha
  apply le_trans ha hab
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
i : ℕ
⊢ a ^ i ≤ b ^ i
[PROOFSTEP]
induction i with
| zero => simp
| succ k ih =>
  rw [pow_succ, pow_succ]
  apply mul_le_mul hab
  apply ih
  apply pow_nonneg ha
  apply le_trans ha hab
[GOAL]
case zero
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
⊢ a ^ Nat.zero ≤ b ^ Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
⊢ a ^ Nat.zero ≤ b ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a ^ Nat.succ k ≤ b ^ Nat.succ k
[PROOFSTEP]

| succ k ih =>
  rw [pow_succ, pow_succ]
  apply mul_le_mul hab
  apply ih
  apply pow_nonneg ha
  apply le_trans ha hab
[GOAL]
case succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a ^ Nat.succ k ≤ b ^ Nat.succ k
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
case succ
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a * a ^ k ≤ b * b ^ k
[PROOFSTEP]
apply mul_le_mul hab
[GOAL]
case succ.h₂
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a ^ k ≤ b ^ k
case succ.c0
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ a ^ k
case succ.b0
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
[PROOFSTEP]
apply ih
[GOAL]
case succ.c0
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ a ^ k
case succ.b0
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
[PROOFSTEP]
apply pow_nonneg ha
[GOAL]
case succ.b0
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
[PROOFSTEP]
apply le_trans ha hab
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n
[PROOFSTEP]
exact one_lt_mul_of_lt_of_le ha (one_le_pow_of_one_le ha.le _)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedSemiring R
a x y : R
n m : ℕ
h : x < y
hx : 0 ≤ x
hn : 0 < 0
⊢ x ^ 0 < y ^ 0
[PROOFSTEP]
contradiction
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedSemiring R
a x y : R
n✝ m : ℕ
h : x < y
hx : 0 ≤ x
n : ℕ
x✝ : 0 < n + 1
⊢ x ^ (n + 1) < y ^ (n + 1)
[PROOFSTEP]
simpa only [pow_succ'] using mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedSemiring R
a x y : R
n✝ m : ℕ
h : 1 < a
this : 0 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)
[PROOFSTEP]
simpa only [one_mul, pow_succ] using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedSemiring R
a x y : R
n✝ m : ℕ
h₀ : 0 < a
h₁ : a < 1
n : ℕ
⊢ a ^ (n + 1) < a ^ n
[PROOFSTEP]
simpa only [pow_succ, one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedSemiring R
a x y : R
n m : ℕ
ha : 0 < a
⊢ 0 < a ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedSemiring R
a x y : R
n m : ℕ
ha : 0 < a
⊢ 0 < a * a
[PROOFSTEP]
exact mul_pos ha ha
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
n : ℕ
⊢ 0 < a ^ bit0 n
[PROOFSTEP]
rw [pow_bit0']
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
n : ℕ
⊢ 0 < (a * a) ^ n
[PROOFSTEP]
exact pow_pos (mul_pos_of_neg_of_neg ha ha) _
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
n : ℕ
⊢ a ^ bit1 n < 0
[PROOFSTEP]
rw [bit1, pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
n : ℕ
⊢ a * a ^ bit0 n < 0
[PROOFSTEP]
exact mul_neg_of_neg_of_pos ha (pow_bit0_pos_of_neg ha n)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1
[PROOFSTEP]
refine' ⟨_, pow_le_one n ha⟩
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ 1 → a ≤ 1
[PROOFSTEP]
rw [← not_lt, ← not_lt]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ ¬1 < a ^ n → ¬1 < a
[PROOFSTEP]
exact mt fun h => one_lt_pow h hn
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ a ^ n ↔ 1 ≤ a
[PROOFSTEP]
refine' ⟨_, fun h => one_le_pow_of_one_le h n⟩
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ a ^ n → 1 ≤ a
[PROOFSTEP]
rw [← not_lt, ← not_lt]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ ¬a ^ n < 1 → ¬a < 1
[PROOFSTEP]
exact mt fun h => pow_lt_one ha h hn
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a✝ b✝ a b : R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a b : R
hb : 0 ≤ b
⊢ a * a < b * b → a < b
[PROOFSTEP]
simp_rw [← sq]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedSemiring R
a b : R
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2 → a < b
[PROOFSTEP]
exact lt_of_pow_lt_pow _ hb
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
n : ℕ
⊢ |(-1) ^ n| = 1
[PROOFSTEP]
rw [← pow_abs, abs_neg, abs_one, one_pow]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ |a ^ n| = 1 ↔ |a| = 1
[PROOFSTEP]
convert pow_left_inj (abs_nonneg a) zero_le_one h
[GOAL]
case h.e'_1.h.e'_2
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ |a ^ n| = |a| ^ n
case h.e'_1.h.e'_3
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ 1 = 1 ^ n
[PROOFSTEP]
exacts [(pow_abs _ _).symm, (one_pow _).symm]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ 0 ≤ a ^ bit0 n
[PROOFSTEP]
rw [pow_bit0]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ 0 ≤ a ^ n * a ^ n
[PROOFSTEP]
exact mul_self_nonneg _
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : n ≠ 0
⊢ 0 < a ^ bit0 n ↔ a ≠ 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => pow_bit0_pos h n⟩
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : n ≠ 0
h : 0 < a ^ bit0 n
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
n : ℕ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ False
[PROOFSTEP]
rw [zero_pow (Nat.zero_lt_bit0 hn)] at h
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
n : ℕ
hn : n ≠ 0
h : 0 < 0
⊢ False
[PROOFSTEP]
exact lt_irrefl _ h
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ |x| ^ 2 = x ^ 2
[PROOFSTEP]
simpa only [sq] using abs_mul_abs_self x
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ |x ^ 2| = x ^ 2
[PROOFSTEP]
simpa only [sq] using abs_mul_self x
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x y : R
⊢ x ^ 2 < y ^ 2 ↔ |x| < |y|
[PROOFSTEP]
simpa only [sq_abs] using (@strictMonoOn_pow R _ _ two_pos).lt_iff_lt (abs_nonneg x) (abs_nonneg y)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x y : R
⊢ x ^ 2 ≤ y ^ 2 ↔ |x| ≤ |y|
[PROOFSTEP]
simpa only [sq_abs] using (@strictMonoOn_pow R _ _ two_pos).le_iff_le (abs_nonneg x) (abs_nonneg y)
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x y : R
h : x ^ 2 < y ^ 2
hy : 0 ≤ y
⊢ |x| < y
[PROOFSTEP]
rwa [← abs_of_nonneg hy, ← sq_lt_sq]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x y : R
h : x ^ 2 ≤ y ^ 2
hy : 0 ≤ y
⊢ |x| ≤ y
[PROOFSTEP]
rwa [← abs_of_nonneg hy, ← sq_le_sq]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x✝ y✝ x y : R
⊢ x ^ 2 = y ^ 2 ↔ |x| = |y|
[PROOFSTEP]
simp only [le_antisymm_iff, sq_le_sq]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ x ^ 2 ≤ 1 ↔ |x| ≤ 1
[PROOFSTEP]
simpa only [one_pow, abs_one] using @sq_le_sq _ _ x 1
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ x ^ 2 < 1 ↔ |x| < 1
[PROOFSTEP]
simpa only [one_pow, abs_one] using @sq_lt_sq _ _ x 1
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ 1 ≤ x ^ 2 ↔ 1 ≤ |x|
[PROOFSTEP]
simpa only [one_pow, abs_one] using @sq_le_sq _ _ 1 x
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ 1 < x ^ 2 ↔ 1 < |x|
[PROOFSTEP]
simpa only [one_pow, abs_one] using @sq_lt_sq _ _ 1 x
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝¹ : LinearOrderedCommMonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ 0 < a ^ n ↔ 0 < a
[PROOFSTEP]
simp_rw [zero_lt_iff, pow_ne_zero_iff hn]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n : ℕ
ha : 1 < a
⊢ a ^ n < a ^ Nat.succ n
[PROOFSTEP]
rw [← one_mul (a ^ n), pow_succ]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n : ℕ
ha : 1 < a
⊢ 1 * a ^ n < a * a ^ n
[PROOFSTEP]
exact mul_lt_right₀ _ ha (pow_ne_zero _ (zero_lt_one.trans ha).ne')
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n : ℕ
ha : 1 < a
hmn : m < n
⊢ a ^ m < a ^ n
[PROOFSTEP]
induction' hmn with n _ ih
[GOAL]
case refl
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n : ℕ
ha : 1 < a
⊢ a ^ m < a ^ Nat.succ m
case step
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n✝ : ℕ
ha : 1 < a
n : ℕ
a✝ : Nat.le (Nat.succ m) n
ih : a ^ m < a ^ n
⊢ a ^ m < a ^ Nat.succ n
[PROOFSTEP]
exacts [pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Ring R
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : R →* M
⊢ ↑f (-1) ^ Nat.succ 1 = 1
[PROOFSTEP]
rw [← map_pow, neg_one_sq, map_one]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Ring R
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : R →* M
x : R
⊢ ↑f (-x) = ↑f x
[PROOFSTEP]
rw [← neg_one_mul, map_mul, map_neg_one, one_mul]
[GOAL]
β : Type u_1
A : Type u_2
G : Type u_3
M : Type u_4
R : Type u_5
inst✝³ : Ring R
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : R →* M
x y : R
⊢ ↑f (x - y) = ↑f (y - x)
[PROOFSTEP]
rw [← map_neg, neg_sub]