[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
[PROOFSTEP]
trans x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (p ^ n).choose k
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k)
[PROOFSTEP]
simp_rw [h.add_pow, ← Nat.Ico_zero_eq_range, Nat.Ico_succ_right, Icc_eq_cons_Ico (zero_le _), Finset.sum_cons,
  Ico_eq_cons_Ioo (pow_pos hp.pos _), Finset.sum_cons, tsub_self, tsub_zero, pow_zero, Nat.choose_zero_right,
  Nat.choose_self, Nat.cast_one, mul_one, one_mul, ← add_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
[PROOFSTEP]
simp_rw [Finset.mul_sum, Nat.cast_comm, mul_assoc _ _ (p : R), ← Nat.cast_mul]
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ∑ x_1 in Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑(Nat.choose (p ^ n) x_1 / p * p)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i hi => _
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : i ∈ Ioo 0 (p ^ n)
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
[PROOFSTEP]
rw [mem_Ioo] at hi
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : 0 < i ∧ i < p ^ n
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
[PROOFSTEP]
rw [Nat.div_mul_cancel (hp.dvd_choose_pow hi.1.ne' hi.2.ne)]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k in Ioo 0 p, x ^ k * y ^ (p - k) * ↑(Nat.choose p k / p)
[PROOFSTEP]
simpa using h.add_pow_prime_pow_eq hp 1
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ ↑(Fintype.card R) = 0
[PROOFSTEP]
rw [← nsmul_one, card_nsmul_eq_zero]
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : ℕ
⊢ ↑n = 0 ↔ addOrderOf 1 ∣ n
[PROOFSTEP]
rw [← Nat.smul_one_eq_coe, addOrderOf_dvd_iff_nsmul_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
⊢ ↑a = 0 ↔ ↑p ∣ a
[PROOFSTEP]
rcases lt_trichotomy a 0 with (h | rfl | h)
[GOAL]
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑a = 0 ↔ ↑p ∣ a
[PROOFSTEP]
rw [← neg_eq_zero, ← Int.cast_neg, ← dvd_neg]
[GOAL]
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑(-a) = 0 ↔ ↑p ∣ -a
[PROOFSTEP]
lift -a to ℕ using neg_nonneg.mpr (le_of_lt h) with b
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
b : ℕ
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b
[PROOFSTEP]
rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0
[PROOFSTEP]
simp only [Int.cast_zero, eq_self_iff_true, dvd_zero]
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a
[PROOFSTEP]
lift a to ℕ using le_of_lt h with b
[GOAL]
case inr.inr.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
b : ℕ
h✝ h : 0 < ↑b
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b
[PROOFSTEP]
rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]
[PROOFSTEP]
rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]
[PROOFSTEP]
rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
⊢ ↑↑a = ↑↑b ↔ a ≡ b [MOD p]
[PROOFSTEP]
exact (CharP.intCast_eq_intCast _ _).trans Int.coe_nat_modEq_iff
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x
[PROOFSTEP]
rw [zero_dvd_iff, ← Nat.cast_zero, Nat.cast_inj]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x
[PROOFSTEP]
rw [zero_dvd_iff]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
exact ⟨H x, by rintro rfl; simp⟩
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ x = 0 → ↑x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑x = 0
H2 : ¬x % Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0)) = 0
⊢ ↑(x % Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0))) = 0
[PROOFSTEP]
rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add, Nat.cast_mul,
  of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)), zero_mul, add_zero] at H1
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0)) ∣ x
⊢ ↑x = 0
[PROOFSTEP]
rw [← Nat.mul_div_cancel' H1, Nat.cast_mul, of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)), zero_mul]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
[PROOFSTEP]
letI : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).1
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
[PROOFSTEP]
exact CharP.cast_eq_zero_iff R (ringChar R)
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ↑(ringChar R) = 0
[PROOFSTEP]
rw [ringChar.spec]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p
[PROOFSTEP]
let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hp.out
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
r : R
hr : (x + y) ^ p = x ^ p + y ^ p + ↑p * r
⊢ (x + y) ^ p = x ^ p + y ^ p
[PROOFSTEP]
simp [hr]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
[PROOFSTEP]
let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hp.out n
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
[PROOFSTEP]
simp [hr]
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p
[PROOFSTEP]
rw [eq_sub_iff_add_eq, ← add_pow_char_of_commute _ _ _ (Commute.sub_left h rfl)]
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y + y) ^ p = x ^ p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
n : ℕ
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih =>
  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
  apply sub_pow_char_of_commute; apply Commute.pow_pow h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
n : ℕ
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih =>
  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
  apply sub_pow_char_of_commute; apply Commute.pow_pow h
[GOAL]
case zero
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ Nat.zero = x ^ p ^ Nat.zero - y ^ p ^ Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ Nat.zero = x ^ p ^ Nat.zero - y ^ p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ (x - y) ^ p ^ Nat.succ n = x ^ p ^ Nat.succ n - y ^ p ^ Nat.succ n
[PROOFSTEP]

| succ n n_ih =>
  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
  apply sub_pow_char_of_commute; apply Commute.pow_pow h
[GOAL]
case succ
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ (x - y) ^ p ^ Nat.succ n = x ^ p ^ Nat.succ n - y ^ p ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
[GOAL]
case succ
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ (x ^ p ^ n - y ^ p ^ n) ^ p = (x ^ p ^ n) ^ p - (y ^ p ^ n) ^ p
[PROOFSTEP]
apply sub_pow_char_of_commute
[GOAL]
case succ.h
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ Commute (x ^ p ^ n) (y ^ p ^ n)
[PROOFSTEP]
apply Commute.pow_pow h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ -1 ≠ 1
[PROOFSTEP]
suffices (2 : R) ≠ 0 by
  intro h
  symm at h
  rw [← sub_eq_zero, sub_neg_eq_add] at h
  norm_num at h
  exact this h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
⊢ -1 ≠ 1
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h : -1 = 1
⊢ False
[PROOFSTEP]
symm at h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h : 1 = -1
⊢ False
[PROOFSTEP]
rw [← sub_eq_zero, sub_neg_eq_add] at h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h✝ : 1 = -1
h : 1 + 1 = 0
⊢ False
[PROOFSTEP]
norm_num at h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h✝ : 1 = -1
h : 2 = 0
⊢ False
[PROOFSTEP]
exact this h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ 2 ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : 2 = 0
⊢ False
[PROOFSTEP]
rw [show (2 : R) = (2 : ℕ) by norm_cast] at h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : 2 = 0
⊢ 2 = ↑2
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
⊢ False
[PROOFSTEP]
have := (CharP.cast_eq_zero_iff R p 2).mp h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
this : p ∣ 2
⊢ False
[PROOFSTEP]
have := Nat.le_of_dvd (by decide) this
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
this : p ∣ 2
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
this✝ : p ∣ 2
this : p ≤ 2
⊢ False
[PROOFSTEP]
rw [fact_iff] at *
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : 2 < p
h : ↑2 = 0
this✝ : p ∣ 2
this : p ≤ 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p = -1
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p + 1 = 0
[PROOFSTEP]
nth_rw 2 [← one_pow p]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p + 1 ^ p = 0
[PROOFSTEP]
rw [← add_pow_char, add_left_neg, zero_pow (Fact.out (p := Nat.Prime p)).pos]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n = -1
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 = 0
[PROOFSTEP]
nth_rw 2 [← one_pow (p ^ n)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0
[PROOFSTEP]
rw [← add_pow_char_pow, add_left_neg, zero_pow (pow_pos (Fact.out (p := Nat.Prime p)).pos _)]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Semiring L
inst✝ : Nontrivial L
f : K →+* L
p : ℕ
⊢ CharP K p ↔ CharP L p
[PROOFSTEP]
simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, f.map_zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
⊢ (↑(frobenius R p))^[n] x = x ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih => rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
⊢ (↑(frobenius R p))^[n] x = x ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih => rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
⊢ (↑(frobenius R p))^[Nat.zero] x = x ^ p ^ Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
⊢ (↑(frobenius R p))^[Nat.zero] x = x ^ p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
n_ih : (↑(frobenius R p))^[n] x = x ^ p ^ n
⊢ (↑(frobenius R p))^[Nat.succ n] x = x ^ p ^ Nat.succ n
[PROOFSTEP]

| succ n n_ih => rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
n_ih : (↑(frobenius R p))^[n] x = x ^ p ^ n
⊢ (↑(frobenius R p))^[Nat.succ n] x = x ^ p ^ Nat.succ n
[PROOFSTEP]
rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H : ↑(frobenius R p) x = ↑(frobenius R p) h
⊢ x = h
[PROOFSTEP]
rw [← sub_eq_zero] at H ⊢
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) x - ↑(frobenius R p) h = 0
⊢ x - h = 0
[PROOFSTEP]
rw [← frobenius_sub] at H
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) (x - h) = 0
⊢ x - h = 0
[PROOFSTEP]
exact IsReduced.eq_zero _ ⟨_, H⟩
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
⊢ IsSquare a
[PROOFSTEP]
cases nonempty_fintype R
[GOAL]
case intro
R✝ : Type u_1
R : Type u_2
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
val✝ : Fintype R
⊢ IsSquare a
[PROOFSTEP]
exact
  Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
    (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑k = ↑(k % p + p * (k / p))
[PROOFSTEP]
rw [Nat.mod_add_div]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑(k % p + p * (k / p)) = ↑(k % p)
[PROOFSTEP]
simp [cast_eq_zero]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Finite R
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False
[PROOFSTEP]
haveI : CharZero R := charP_to_charZero R
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False
[PROOFSTEP]
cases nonempty_fintype R
[GOAL]
case intro
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
val✝ : Fintype R
⊢ False
[PROOFSTEP]
exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))
[GOAL]
R : Type u_1
inst✝¹ inst✝ : NonAssocRing R
⊢ ringChar R = 0 ↔ CharZero R
[PROOFSTEP]
rw [ringChar.eq_iff, charP_zero_iff_charZero]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p k m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
⊢ x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
⊢ x ^ (p ^ Nat.zero * m) = 1 ↔ x ^ m = 1
[PROOFSTEP]
rw [pow_zero, one_mul]
[GOAL]
case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
⊢ x ^ (p ^ Nat.succ k * m) = 1 ↔ x ^ m = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case succ.refine'_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
h : x ^ (p ^ Nat.succ k * m) = 1
⊢ x ^ m = 1
[PROOFSTEP]
rw [pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at h
[GOAL]
case succ.refine'_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
h✝ : ↑(frobenius R p) (x ^ (p ^ k * m)) = 1
h : ↑(frobenius R p) (x ^ (p ^ k * m)) = ↑(frobenius R p) 1
⊢ x ^ m = 1
[PROOFSTEP]
exact hk.1 (frobenius_inj R p h)
[GOAL]
case succ.refine'_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
h : x ^ m = 1
⊢ x ^ (p ^ Nat.succ k * m) = 1
[PROOFSTEP]
rw [pow_mul', h, one_pow]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hc : CharP R p
hp : p = 1
⊢ 1 = 0
[PROOFSTEP]
simpa using (cast_eq_zero_iff R p 1).mpr (hp ▸ dvd_refl p)
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : NoZeroDivisors R
p : ℕ
hc : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * e
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p
[PROOFSTEP]
rw [‹e = p›] at hmul
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : NoZeroDivisors R
p : ℕ
hc : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p
[PROOFSTEP]
rw [one_mul]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : NoZeroDivisors R
p : ℕ
hc : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = p
[PROOFSTEP]
exact Eq.symm hmul
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ r = 1 * r
[PROOFSTEP]
rw [one_mul]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ 1 * r = ↑1 * r
[PROOFSTEP]
rw [Nat.cast_one]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ ↑1 * r = 0 * r
[PROOFSTEP]
rw [CharP.cast_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ 0 * r = 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
this : ∀ (r : R), r = 0
a b : R
⊢ a = b
[PROOFSTEP]
rw [this a, this b]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
⊢ ringChar R ≠ 1
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ False
[PROOFSTEP]
apply zero_ne_one' R
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 0 = 1
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 1 = 0
[PROOFSTEP]
rw [← Nat.cast_one, ringChar.spec, h]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : ↑1 = 0
⊢ v = 1
[PROOFSTEP]
rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 ≠ 0
[PROOFSTEP]
rw [Ne.def, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 = ↑2
[PROOFSTEP]
norm_cast
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)
[PROOFSTEP]
exact mt (or_iff_left hR).mp CharP.ringChar_ne_one
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
[PROOFSTEP]
have H : (n : R) = 0 := by rw [← hn, CharP.cast_card_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
⊢ ↑n = 0
[PROOFSTEP]
rw [← hn, CharP.cast_card_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
[PROOFSTEP]
intro k
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 ↔ n ∣ k
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 → n ∣ k
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑k = 0
⊢ n ∣ k
[PROOFSTEP]
rw [← Nat.mod_add_div k n, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n ∣ k
[PROOFSTEP]
rw [Nat.dvd_iff_mod_eq_zero]
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ k % n = 0
[PROOFSTEP]
apply hR _ (Nat.mod_lt _ _) h
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n > 0
[PROOFSTEP]
rw [← hn, gt_iff_lt, Fintype.card_pos_iff]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ Nonempty R
[PROOFSTEP]
exact ⟨0⟩
[GOAL]
case mpr
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ n ∣ k → ↑k = 0
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑(n * k) = 0
[PROOFSTEP]
rw [Nat.cast_mul, H, zero_mul]
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
⊢ CharP R (p ^ n)
[PROOFSTEP]
obtain ⟨c, hc⟩ := CharP.exists R
[GOAL]
case intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)
[PROOFSTEP]
have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, CharP.cast_card_eq_zero]
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ c ∣ p ^ n
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff R c, ← hn, CharP.cast_card_eq_zero]
[GOAL]
case intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ CharP R (p ^ n)
[PROOFSTEP]
obtain ⟨i, hi, hc⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ ∃ i, i ≤ n ∧ c = p ^ i
[PROOFSTEP]
rwa [Nat.dvd_prime_pow hp.1] at hcpn
[GOAL]
case intro.intro.intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ CharP R (p ^ n)
[PROOFSTEP]
obtain rfl : i = n := by
  apply hR i hi
  rw [← Nat.cast_pow, ← hc, CharP.cast_eq_zero]
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ i = n
[PROOFSTEP]
apply hR i hi
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ ↑p ^ i = 0
[PROOFSTEP]
rw [← Nat.cast_pow, ← hc, CharP.cast_eq_zero]
[GOAL]
case intro.intro.intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc✝ : CharP R c
i : ℕ
hc : c = p ^ i
hn : Fintype.card R = p ^ i
hR : ∀ (i_1 : ℕ), i_1 ≤ i → ↑p ^ i_1 = 0 → i_1 = i
hcpn : c ∣ p ^ i
hi : i ≤ i
⊢ CharP R (p ^ i)
[PROOFSTEP]
rwa [← hc]
[GOAL]
R : Type u_1
S : Type v
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S q
⊢ ∀ (x : ℕ), ↑x = 0 ↔ lcm p q ∣ x
[PROOFSTEP]
simp [Prod.ext_iff, CharP.cast_eq_zero_iff R p, CharP.cast_eq_zero_iff S q, Nat.lcm_dvd_iff]
[GOAL]
R : Type u_1
S : Type v
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S p
⊢ CharP (R × S) p
[PROOFSTEP]
convert Nat.lcm.charP R S p p
[GOAL]
case h.e'_3
R : Type u_1
S : Type v
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S p
⊢ p = Nat.lcm p p
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ Set.InjOn Int.cast {0, 1, -1}
[PROOFSTEP]
rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h
[GOAL]
case inl.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑0
⊢ 0 = 0
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inl.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑1
⊢ 0 = 1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inl.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑(-1)
⊢ 0 = -1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑0
⊢ 1 = 0
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑1
⊢ 1 = 1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑(-1)
⊢ 1 = -1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑0
⊢ -1 = 0
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inr.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑1
⊢ -1 = 1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inr.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑(-1)
⊢ -1 = -1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ False
[PROOFSTEP]
exact (Ring.neg_one_ne_one_of_char_ne_two hR).symm h
[GOAL]
case inr.inr.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ False
[PROOFSTEP]
exact (Ring.neg_one_ne_one_of_char_ne_two hR) h
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
r : R
n p✝ : ℕ
a : ℕ+
p : ℕ
inst✝ : CharP R p
k : ℕ
h : NeZero ↑k
⊢ ¬p ∣ k
[PROOFSTEP]
rwa [← CharP.cast_eq_zero_iff R p k, ← Ne.def, ← neZero_iff]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
[PROOFSTEP]
refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : CharZero R
p : ℕ
hp : Nat.Prime p
⊢ ↑p ≠ 0
[PROOFSTEP]
simp [hp.ne_zero]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
⊢ CharZero R
[PROOFSTEP]
let p := ringChar R
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
⊢ CharZero R
[PROOFSTEP]
cases CharP.char_is_prime_or_zero R p with
| inl hp => simpa using h p hp
| inr h =>
  haveI : CharP R 0 := h ▸ inferInstance
  exact CharP.charP_to_charZero R
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
x✝ : Nat.Prime p ∨ p = 0
⊢ CharZero R
[PROOFSTEP]
cases CharP.char_is_prime_or_zero R p with
| inl hp => simpa using h p hp
| inr h =>
  haveI : CharP R 0 := h ▸ inferInstance
  exact CharP.charP_to_charZero R
[GOAL]
case inl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R
[PROOFSTEP]

| inl hp => simpa using h p hp
[GOAL]
case inl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R
[PROOFSTEP]
simpa using h p hp
[GOAL]
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
⊢ CharZero R
[PROOFSTEP]

| inr h =>
  haveI : CharP R 0 := h ▸ inferInstance
  exact CharP.charP_to_charZero R
[GOAL]
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
⊢ CharZero R
[PROOFSTEP]
haveI : CharP R 0 := h ▸ inferInstance
[GOAL]
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
this : CharP R 0
⊢ CharZero R
[PROOFSTEP]
exact CharP.charP_to_charZero R


[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n✝ : ℤ
a : α
n : ℤ
⊢ (-a) ^ bit1 n = -a ^ bit1 n
[PROOFSTEP]
rw [zpow_bit1', zpow_bit1', neg_mul_neg, neg_mul_eq_mul_neg]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := h.exists_bit1
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionRing α
a : α
k : ℤ
h : Odd (bit1 k)
⊢ (-a) ^ bit1 k = -a ^ bit1 k
[PROOFSTEP]
exact zpow_bit1_neg _ _
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
⊢ (-1) ^ n = -1
[PROOFSTEP]
rw [h.neg_zpow, one_zpow]


[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Semigroup (f i)
⊢ ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Semigroup (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Semigroup (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝ * c✝) x✝ = (a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
exact mul_assoc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → CommSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
⊢ ∀ (a b : (i : I) → f i), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → CommSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ : (i : I) → f i
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → CommSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝) x✝ = (b✝ * a✝) x✝
[PROOFSTEP]
exact mul_comm _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (1 * a✝) x✝ = a✝ x✝
[PROOFSTEP]
exact one_mul _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * 1) x✝ = a✝ x✝
[PROOFSTEP]
exact mul_one _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvOneClass (f i)
⊢ 1⁻¹ = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvOneClass (f i)
⊢ 1⁻¹ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvOneClass (f i)
x✝ : I
⊢ 1⁻¹ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact inv_one
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
⊢ ∀ (x : (i : I) → f i), (fun n x i => x i ^ n) 0 x = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
x✝ : (i : I) → f i
⊢ (fun n x i => x i ^ n) 0 x✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
x✝¹ : (i : I) → f i
x✝ : I
⊢ (fun n x i => x i ^ n) 0 x✝¹ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact Monoid.npow_zero _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
⊢ ∀ (n : ℕ) (x : (i : I) → f i), (fun n x i => x i ^ n) (n + 1) x = x * (fun n x i => x i ^ n) n x
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
n✝ : ℕ
x✝ : (i : I) → f i
⊢ (fun n x i => x i ^ n) (n✝ + 1) x✝ = x✝ * (fun n x i => x i ^ n) n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
n✝ : ℕ
x✝¹ : (i : I) → f i
x✝ : I
⊢ (fun n x i => x i ^ n) (n✝ + 1) x✝¹ x✝ = (x✝¹ * (fun n x i => x i ^ n) n✝ x✝¹) x✝
[PROOFSTEP]
exact Monoid.npow_succ _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (a b : (i : I) → f i), a / b = a * b⁻¹
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ b✝ : (i : I) → f i
⊢ a✝ / b✝ = a✝ * b✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ b✝ : (i : I) → f i
x✝ : I
⊢ (a✝ / b✝) x✝ = (a✝ * b✝⁻¹) x✝
[PROOFSTEP]
exact div_eq_mul_inv _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (a : (i : I) → f i), (fun z x i => x i ^ z) 0 a = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ : (i : I) → f i
⊢ (fun z x i => x i ^ z) 0 a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ : (i : I) → f i
x✝ : I
⊢ (fun z x i => x i ^ z) 0 a✝ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact DivInvMonoid.zpow_zero' _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (n : ℕ) (a : (i : I) → f i),
    (fun z x i => x i ^ z) (Int.ofNat (Nat.succ n)) a = a * (fun z x i => x i ^ z) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
⊢ (fun z x i => x i ^ z) (Int.ofNat (Nat.succ n✝)) a✝ = a✝ * (fun z x i => x i ^ z) (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
x✝ : I
⊢ (fun z x i => x i ^ z) (Int.ofNat (Nat.succ n✝)) a✝ x✝ = (a✝ * (fun z x i => x i ^ z) (Int.ofNat n✝) a✝) x✝
[PROOFSTEP]
exact DivInvMonoid.zpow_succ' _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (n : ℕ) (a : (i : I) → f i), (fun z x i => x i ^ z) (Int.negSucc n) a = ((fun z x i => x i ^ z) (↑(Nat.succ n)) a)⁻¹
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
⊢ (fun z x i => x i ^ z) (Int.negSucc n✝) a✝ = ((fun z x i => x i ^ z) (↑(Nat.succ n✝)) a✝)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
x✝ : I
⊢ (fun z x i => x i ^ z) (Int.negSucc n✝) a✝ x✝ = ((fun z x i => x i ^ z) (↑(Nat.succ n✝)) a✝)⁻¹ x✝
[PROOFSTEP]
exact DivInvMonoid.zpow_neg' _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvOneMonoid (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
⊢ 1⁻¹ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvOneMonoid (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
x✝ : I
⊢ 1⁻¹ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact inv_one
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvolutiveInv (f i)
⊢ ∀ (x : (i : I) → f i), x⁻¹⁻¹ = x
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvolutiveInv (f i)
x✝ : (i : I) → f i
⊢ x✝⁻¹⁻¹ = x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvolutiveInv (f i)
x✝¹ : (i : I) → f i
x✝ : I
⊢ x✝¹⁻¹⁻¹ x✝ = x✝¹ x✝
[PROOFSTEP]
exact inv_inv _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
⊢ ∀ (a b : (i : I) → f i), (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
⊢ (a✝ * b✝)⁻¹ = b✝⁻¹ * a✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝)⁻¹ x✝ = (b✝⁻¹ * a✝⁻¹) x✝
[PROOFSTEP]
exact mul_inv_rev _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
⊢ ∀ (a b : (i : I) → f i), a * b = 1 → a⁻¹ = b
[PROOFSTEP]
intros _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
h : a✝ * b✝ = 1
⊢ a✝⁻¹ = b✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
h : a✝ * b✝ = 1
x✝ : I
⊢ a✝⁻¹ x✝ = b✝ x✝
[PROOFSTEP]
exact DivisionMonoid.inv_eq_of_mul _ _ (congrFun h _)
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Group (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
⊢ ∀ (a : (i : I) → f i), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Group (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
a✝ : (i : I) → f i
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Group (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝⁻¹ * a✝) x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact mul_left_inv _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → LeftCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
⊢ ∀ (a b c : (i : I) → f i), a * b = a * c → b = c
[PROOFSTEP]
intros _ _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → LeftCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = a✝ * c✝
⊢ b✝ = c✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → LeftCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = a✝ * c✝
x✝ : I
⊢ b✝ x✝ = c✝ x✝
[PROOFSTEP]
exact LeftCancelSemigroup.mul_left_cancel _ _ _ (congr_fun h _)
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → RightCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
⊢ ∀ (a b c : (i : I) → f i), a * b = c * b → a = c
[PROOFSTEP]
intros _ _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → RightCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = c✝ * b✝
⊢ a✝ = c✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → RightCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = c✝ * b✝
x✝ : I
⊢ a✝ x✝ = c✝ x✝
[PROOFSTEP]
exact RightCancelSemigroup.mul_right_cancel _ _ _ (congr_fun h _)
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
⊢ ∀ (a : (i : I) → f i), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
⊢ 0 * a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (0 * a✝) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
exact zero_mul _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
⊢ ∀ (a : (i : I) → f i), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
⊢ a✝ * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * 0) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
exact mul_zero _
[GOAL]
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_5
x✝¹ x✝ : I → α
⊢ (fun h => ↑f ∘ h) (x✝¹ * x✝) = (fun h => ↑f ∘ h) x✝¹ * (fun h => ↑f ∘ h) x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_5
x✝² x✝¹ : I → α
x✝ : I
⊢ (fun h => ↑f ∘ h) (x✝² * x✝¹) x✝ = ((fun h => ↑f ∘ h) x✝² * (fun h => ↑f ∘ h) x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
⊢ (fun h => ↑f ∘ h) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝ : I
⊢ (fun h => ↑f ∘ h) 1 x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝ : I
⊢ ↑f 1 = 1
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝¹ x✝ : I → α
⊢ OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } (x✝¹ * x✝) =
    OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝¹ *
      OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝² x✝¹ : I → α
x✝ : I
⊢ OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } (x✝² * x✝¹) x✝ =
    (OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝² *
        OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝¹)
      x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
⊢ Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)
[PROOFSTEP]
intro i j hij x y
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle i x) (mulSingle j y)
[PROOFSTEP]
ext k
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
by_cases h1 : i = k
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
subst h1
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ (mulSingle i x * mulSingle j y) i = (mulSingle j y * mulSingle i x) i
[PROOFSTEP]
simp [hij]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : ¬i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
by_cases h2 : j = k
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : ¬i = k
h2 : j = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
subst h2
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
h1 : ¬i = j
⊢ (mulSingle i x * mulSingle j y) j = (mulSingle j y * mulSingle i x) j
[PROOFSTEP]
simp [hij]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : ¬i = k
h2 : ¬j = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
simp [h1, h2]
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))
[PROOFSTEP]
obtain rfl | hij := Decidable.eq_or_ne i j
[GOAL]
case inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i✝ j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))
[PROOFSTEP]
exact Pi.mulSingle_commute hij _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x = g / mulSingle i (g i) * mulSingle i x
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
[PROOFSTEP]
rcases eq_or_ne i j with (rfl | h)
[GOAL]
case h.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i
[PROOFSTEP]
simp
[GOAL]
case h.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
[PROOFSTEP]
simp [Function.update_noteq h.symm, h]
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hk := congr_fun h k
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hl := congr_fun h l
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hm := (congr_fun h m).symm
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle m u * mulSingle n v) m = (mulSingle k u * mulSingle l v) m
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hn := (congr_fun h n).symm
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle m u * mulSingle n v) m = (mulSingle k u * mulSingle l v) m
hn : (mulSingle m u * mulSingle n v) n = (mulSingle k u * mulSingle l v) n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
simp only [mul_apply, mulSingle_apply, if_pos rfl] at hk hl hm hn
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if m = n then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
rcases eq_or_ne k m with (rfl | hkm)
[GOAL]
case refine'_1.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
⊢ k = k ∧ l = n ∨ u = v ∧ k = n ∧ l = k ∨ u * v = 1 ∧ k = l ∧ k = n
[PROOFSTEP]
refine' Or.inl ⟨rfl, not_ne_iff.mp fun hln => (hv _).elim⟩
[GOAL]
case refine'_1.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hln : l ≠ n
⊢ v = 1
[PROOFSTEP]
rcases eq_or_ne k l with (rfl | hkl)
[GOAL]
case refine'_1.inl.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle k v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = k then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = k then v else 1
hln : k ≠ n
⊢ v = 1
[PROOFSTEP]
rwa [if_neg hln.symm, if_neg hln.symm, one_mul, one_mul] at hn
[GOAL]
case refine'_1.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hln : l ≠ n
hkl : k ≠ l
⊢ v = 1
[PROOFSTEP]
rwa [if_neg hkl.symm, if_neg hln, one_mul, one_mul] at hl
[GOAL]
case refine'_1.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if m = n then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hkm : k ≠ m
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
rcases eq_or_ne m n with (rfl | hmn)
[GOAL]
case refine'_1.inr.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
rcases eq_or_ne k l with (rfl | hkl)
[GOAL]
case refine'_1.inr.inl.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = k then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = k then v else 1
⊢ k = m ∧ k = m ∨ u = v ∧ k = m ∧ k = m ∨ u * v = 1 ∧ k = k ∧ m = m
[PROOFSTEP]
rw [if_neg hkm.symm, if_neg hkm.symm, one_mul, if_pos rfl] at hm
[GOAL]
case refine'_1.inr.inl.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hm : (if True then u else 1) * v = 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = k then v else 1
⊢ k = m ∧ k = m ∨ u = v ∧ k = m ∧ k = m ∨ u * v = 1 ∧ k = k ∧ m = m
[PROOFSTEP]
exact Or.inr (Or.inr ⟨hm, rfl, rfl⟩)
[GOAL]
case refine'_1.inr.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hkl : k ≠ l
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
simp only [if_neg hkm, if_neg hkl, mul_one] at hk
[GOAL]
case refine'_1.inr.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hkl : k ≠ l
hk : (if True then u else 1) = 1
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
dsimp at hk
[GOAL]
case refine'_1.inr.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hkl : k ≠ l
hk : u = 1
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
contradiction
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if m = n then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hkm : k ≠ m
hmn : m ≠ n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
rw [if_neg hkm.symm, if_neg hmn, one_mul, mul_one] at hm
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : (if True then u else 1) = if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hkm : k ≠ m
hmn : m ≠ n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hm.symm hu)).1
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
hmn : m ≠ n
h : mulSingle k u * mulSingle m v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = m then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if m = k then u else 1) * if True then v else 1) = (if m = m then u else 1) * if m = n then v else 1
hm : (if True then u else 1) = if m = m then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = m then v else 1
⊢ k = m ∧ m = n ∨ u = v ∧ k = n ∧ m = m ∨ u * v = 1 ∧ k = m ∧ m = n
[PROOFSTEP]
rw [if_neg hkm, if_neg hkm, one_mul, mul_one] at hk
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
hmn : m ≠ n
h : mulSingle k u * mulSingle m v = mulSingle m u * mulSingle n v
hk : (if True then u else 1) = if k = n then v else 1
hl : ((if m = k then u else 1) * if True then v else 1) = (if m = m then u else 1) * if m = n then v else 1
hm : (if True then u else 1) = if m = m then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = m then v else 1
⊢ k = m ∧ m = n ∨ u = v ∧ k = n ∧ m = m ∨ u * v = 1 ∧ k = m ∧ m = n
[PROOFSTEP]
obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hk.symm hu)).1
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
hm : (if True then u else 1) = if m = m then v else 1
hmn : m ≠ k
h : mulSingle k u * mulSingle m v = mulSingle m u * mulSingle k v
hk : (if True then u else 1) = if k = k then v else 1
hl : ((if m = k then u else 1) * if True then v else 1) = (if m = m then u else 1) * if m = k then v else 1
hn : ((if k = m then u else 1) * if True then v else 1) = (if k = k then u else 1) * if k = m then v else 1
⊢ k = m ∧ m = k ∨ u = v ∧ k = k ∧ m = m ∨ u * v = 1 ∧ k = m ∧ m = k
[PROOFSTEP]
exact Or.inr (Or.inl ⟨hk.trans (if_pos rfl), rfl, rfl⟩)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ | ⟨h, rfl, rfl⟩)
[GOAL]
case refine'_2.inl.intro
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ mulSingle k u * mulSingle l v = mulSingle k u * mulSingle l v
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr.inl.intro.intro
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l : I
u : M
hu hv : u ≠ 1
⊢ mulSingle k u * mulSingle l u = mulSingle l u * mulSingle k u
[PROOFSTEP]
apply mul_comm
[GOAL]
case refine'_2.inr.inr.intro.intro
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : u * v = 1
⊢ mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v
[PROOFSTEP]
simp_rw [← Pi.mulSingle_mul, h, mulSingle_one]
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f✝ : I → Type v
x y : (i : I) → f✝ i
i j : I
η : Type v
R : Type w
s : ι → η
inst✝ : MulOneClass R
f g : ι → R
⊢ OneHom.toFun { toFun := fun f => extend s f 1, map_one' := (_ : extend s 1 1 = 1) } (f * g) =
    OneHom.toFun { toFun := fun f => extend s f 1, map_one' := (_ : extend s 1 1 = 1) } f *
      OneHom.toFun { toFun := fun f => extend s f 1, map_one' := (_ : extend s 1 1 = 1) } g
[PROOFSTEP]
simpa using Function.extend_mul s f g 1 1


[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
a b : R
⊢ OneHom.toFun
      { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
        map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
      (a * b) =
    OneHom.toFun
        { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
          map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
        a *
      OneHom.toFun
        { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
          map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
        b
[PROOFSTEP]
simp only [AddMonoidHom.comp_apply]
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
a b : R
⊢ ↑(of A 0) (↑GAlgebra.toFun (a * b)) = ↑(of A 0) (↑GAlgebra.toFun a) * ↑(of A 0) (↑GAlgebra.toFun b)
[PROOFSTEP]
rw [of_mul_of]
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
a b : R
⊢ ↑(of A 0) (↑GAlgebra.toFun (a * b)) = ↑(of A (0 + 0)) (GradedMonoid.GMul.mul (↑GAlgebra.toFun a) (↑GAlgebra.toFun b))
[PROOFSTEP]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.map_mul a b)
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                    map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) },
                map_mul' :=
                  (_ :
                    ∀ (a b : R),
                      OneHom.toFun
                          { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                            map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            a *
                          OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            b) },
            map_zero' := (_ : ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) 0 = 0),
            map_add' :=
              (_ :
                ∀ (a b : R),
                  ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) (a + b) =
                    ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) a + ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) b) }
        r *
      x =
    x *
      ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                    map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) },
                map_mul' :=
                  (_ :
                    ∀ (a b : R),
                      OneHom.toFun
                          { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                            map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            a *
                          OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            b) },
            map_zero' := (_ : ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) 0 = 0),
            map_add' :=
              (_ :
                ∀ (a b : R),
                  ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) (a + b) =
                    ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) a + ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) b) }
        r
[PROOFSTEP]
change AddMonoidHom.mul (DirectSum.of _ _ _) x = AddMonoidHom.mul.flip (DirectSum.of _ _ _) x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑(↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) x =
    ↑(↑(AddMonoidHom.flip AddMonoidHom.mul) (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) x
[PROOFSTEP]
apply FunLike.congr_fun _ x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r)) =
    ↑(AddMonoidHom.flip AddMonoidHom.mul) (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))
[PROOFSTEP]
ext i xi : 2
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(AddMonoidHom.comp (↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) (of (fun i => A i) i)) xi =
    ↑(AddMonoidHom.comp (↑(AddMonoidHom.flip AddMonoidHom.mul) (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r)))
          (of (fun i => A i) i))
      xi
[PROOFSTEP]
dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.mul_apply, AddMonoidHom.flip_apply]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(of (fun i => A i) 0) (↑GAlgebra.toFun r) * ↑(of (fun i => A i) i) xi =
    ↑(of (fun i => A i) i) xi * ↑(of (fun i => A i) 0) (↑GAlgebra.toFun r)
[PROOFSTEP]
rw [of_mul_of, of_mul_of]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(of (fun i => A i) (0 + i)) (GradedMonoid.GMul.mul (↑GAlgebra.toFun r) xi) =
    ↑(of (fun i => A i) (i + 0)) (GradedMonoid.GMul.mul xi (↑GAlgebra.toFun r))
[PROOFSTEP]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.commutes r ⟨i, xi⟩)
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ r • x =
    ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                    map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) },
                map_mul' :=
                  (_ :
                    ∀ (a b : R),
                      OneHom.toFun
                          { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                            map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            a *
                          OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            b) },
            map_zero' := (_ : ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) 0 = 0),
            map_add' :=
              (_ :
                ∀ (a b : R),
                  ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) (a + b) =
                    ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) a + ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) b) }
        r *
      x
[PROOFSTEP]
change DistribMulAction.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑(DistribMulAction.toAddMonoidHom ((fun x => ⨁ (i : ι), A i) r) r) x =
    ↑(↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) x
[PROOFSTEP]
apply FunLike.congr_fun _ x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ DistribMulAction.toAddMonoidHom ((fun x => ⨁ (i : ι), A i) r) r =
    ↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))
[PROOFSTEP]
ext i xi : 2
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(AddMonoidHom.comp (DistribMulAction.toAddMonoidHom ((fun x => ⨁ (i : ι), A i) r) r) (of (fun i => A i) i)) xi =
    ↑(AddMonoidHom.comp (↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) (of (fun i => A i) i)) xi
[PROOFSTEP]
dsimp only [AddMonoidHom.comp_apply, DistribMulAction.toAddMonoidHom_apply, AddMonoidHom.mul_apply]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ r • ↑(of (fun i => A i) i) xi = ↑(of (fun i => A i) 0) (↑GAlgebra.toFun r) * ↑(of (fun i => A i) i) xi
[PROOFSTEP]
rw [DirectSum.of_mul_of, ← of_smul]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(of (fun i => A i) i) (r • xi) = ↑(of (fun i => A i) (0 + i)) (GradedMonoid.GMul.mul (↑GAlgebra.toFun r) xi)
[PROOFSTEP]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.smul_def r ⟨i, xi⟩)


[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ c (f ^ 0) = (c f)^[0]
[PROOFSTEP]
rw [pow_zero, h1]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ (n + 1)) = (c f)^[n + 1]
[PROOFSTEP]
rw [pow_succ, iterate_succ', hmul, hom_coe_pow c h1 hmul f n]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
a : G
n : ℕ
inst✝ : MulAction G H
b : H
⊢ (fun x => a • x)^[Nat.zero] b = a ^ Nat.zero • b
[PROOFSTEP]
rw [iterate_zero, id.def, pow_zero, one_smul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
a : G
n✝ : ℕ
inst✝ : MulAction G H
b : H
n : ℕ
ih : (fun x => a • x)^[n] b = a ^ n • b
⊢ (fun x => a • x)^[Nat.succ n] b = a ^ Nat.succ n • b
[PROOFSTEP]
rw [iterate_succ', comp_apply, ih, pow_succ, mul_smul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
inst✝ : Monoid G
a : G
n : ℕ
⊢ (fun x => x * a)^[n] 1 = a ^ n
[PROOFSTEP]
simp [mul_right_iterate]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x => a * x) ((fun x => b * x) j) = (fun x => c * x) ((fun x => a * x) j)
[PROOFSTEP]
dsimp only
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ a * (b * j) = c * (a * j)
[PROOFSTEP]
rw [← mul_assoc, h.eq, mul_assoc]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x => x * a) ((fun x => x * c) j) = (fun x => x * b) ((fun x => x * a) j)
[PROOFSTEP]
simp_rw [mul_assoc, ← h.eq]