[GOAL]
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
a : ZMod n
r : (fun x => R) a
⊢ ↑a * r = r * ↑a
[PROOFSTEP]
rcases ZMod.int_cast_surjective a with ⟨k, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
k : ℤ
r : R
⊢ ↑↑k * r = r * ↑↑k
[PROOFSTEP]
show ZMod.castHom h R k * r = r * ZMod.castHom h R k
[GOAL]
case intro
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
k : ℤ
r : R
⊢ ↑(castHom h R) ↑k * r = r * ↑(castHom h R) ↑k
[PROOFSTEP]
rw [map_intCast]
[GOAL]
case intro
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
k : ℤ
r : R
⊢ ↑k * r = r * ↑k
[PROOFSTEP]
exact Commute.cast_int_left r k


[GOAL]
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ Int.gcd a ↑p ≠ 1
[PROOFSTEP]
rw [Ne, Int.gcd_comm, Int.gcd_eq_one_iff_coprime, (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd,
  Classical.not_not, int_cast_zmod_eq_zero_iff_dvd]


[GOAL]
n : ℕ
⊢ ↑n = 1 ↔ Odd n
[PROOFSTEP]
rw [← @Nat.cast_one (ZMod 2), ZMod.eq_iff_modEq_nat, Nat.odd_iff, Nat.ModEq]
[GOAL]
n : ℕ
⊢ n % 2 = 1 % 2 ↔ n % 2 = 1
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ ↑n ≠ 0 ↔ Odd n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ ↑n ≠ 0 → Odd n
[PROOFSTEP]
contrapose
[GOAL]
case mp
n : ℕ
⊢ ¬Odd n → ¬↑n ≠ 0
[PROOFSTEP]
simp [eq_zero_iff_even]
[GOAL]
case mpr
n : ℕ
⊢ Odd n → ↑n ≠ 0
[PROOFSTEP]
contrapose
[GOAL]
case mpr
n : ℕ
⊢ ¬↑n ≠ 0 → ¬Odd n
[PROOFSTEP]
simp [eq_zero_iff_even]


[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
⊢ ∀ (a b c : Σₗ' (i : ι), α i), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨a₃, b₃⟩ ⟨h₁r⟩ ⟨h₂r⟩
[GOAL]
case mk.mk.mk.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₃, snd := b₃ }
[PROOFSTEP]
left
[GOAL]
case mk.mk.mk.left.left.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < a₃
[PROOFSTEP]
apply lt_trans
[GOAL]
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < ?mk.mk.mk.left.left.a.b
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ?mk.mk.mk.left.left.a.b < a₃
case mk.mk.mk.left.left.a.b
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ι
[PROOFSTEP]
repeat' assumption
[GOAL]
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < ?mk.mk.mk.left.left.a.b
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₂ < a₃
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₂, snd := b₂✝ }
[PROOFSTEP]
left
[GOAL]
case mk.mk.mk.left.right.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₃, snd := b₃ }
[PROOFSTEP]
left
[GOAL]
case mk.mk.mk.right.left.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ a₁ < a₃
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₁, snd := b₂✝ }
[PROOFSTEP]
right
[GOAL]
case mk.mk.mk.right.right.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ b₂✝
[PROOFSTEP]
apply le_trans
[GOAL]
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ ?mk.mk.mk.right.right.a.b
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ ?mk.mk.mk.right.right.a.b ≤ b₂✝
case mk.mk.mk.right.right.a.b
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ (fun i => α i) a₁
[PROOFSTEP]
repeat' assumption
[GOAL]
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ ?mk.mk.mk.right.right.a.b
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₂✝¹ ≤ b₂✝
[PROOFSTEP]
assumption
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
refine' fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, _⟩, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a b : Σₗ' (i : ι), α i
hab : a < b
⊢ ¬b ≤ a
[PROOFSTEP]
rintro (⟨i, a, hji⟩ | ⟨i, hba⟩)
[GOAL]
case refine'_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hab : { fst := a₂✝, snd := a } < { fst := a₁✝, snd := i }
⊢ False
[PROOFSTEP]
obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
[GOAL]
case refine'_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : { fst := i, snd := b₂✝ } < { fst := i, snd := b₁✝ }
⊢ False
[PROOFSTEP]
obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
[GOAL]
case refine'_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hij : a₂✝ < a₁✝
⊢ False
[PROOFSTEP]
exact hij.not_lt hji
[GOAL]
case refine'_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
i a : α a₁✝
hji : a₁✝ < a₁✝
hab : a < i
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hji
[GOAL]
case refine'_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hij : i < i
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hij
[GOAL]
case refine'_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False
[PROOFSTEP]
exact hab.not_le hba
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a b : Σₗ' (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b
[PROOFSTEP]
rintro ⟨⟨j, b, hij⟩ | ⟨i, hab⟩, hba⟩
[GOAL]
case refine'_2.intro.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
j : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : a₁✝ < a₂✝
hba : ¬{ fst := a₂✝, snd := b } ≤ { fst := a₁✝, snd := j }
⊢ { fst := a₁✝, snd := j } < { fst := a₂✝, snd := b }
[PROOFSTEP]
exact Lex.left _ _ hij
[GOAL]
case refine'_2.intro.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hab : b₁✝ ≤ b₂✝
hba : ¬{ fst := i, snd := b₂✝ } ≤ { fst := i, snd := b₁✝ }
⊢ { fst := i, snd := b₁✝ } < { fst := i, snd := b₂✝ }
[PROOFSTEP]
exact Lex.right _ (hab.lt_of_not_le fun h => hba <| Lex.right _ h)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨_, _, hlt₁⟩ | ⟨_, hlt₁⟩) (⟨_, _, hlt₂⟩ | ⟨_, hlt₂⟩)
[GOAL]
case mk.mk.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
hlt₁ : a₁ < a₂
hlt₂ : a₂ < a₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
[PROOFSTEP]
exact (lt_irrefl a₁ <| hlt₁.trans hlt₂).elim
[GOAL]
case mk.mk.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
[PROOFSTEP]
exact (lt_irrefl a₁ hlt₁).elim
[GOAL]
case mk.mk.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂✝ }
[PROOFSTEP]
exact (lt_irrefl a₁ hlt₂).elim
[GOAL]
case mk.mk.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂✝ }
[PROOFSTEP]
rw [hlt₁.antisymm hlt₂]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b ∨ b ≤ a
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a : α i
j : ι
b : α j
⊢ { fst := i, snd := a } ≤ { fst := j, snd := b } ∨ { fst := j, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
obtain hij | rfl | hji := lt_trichotomy i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a : α i
j : ι
b : α j
hij : i < j
⊢ { fst := i, snd := a } ≤ { fst := j, snd := b } ∨ { fst := j, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.left _ _ hij)
[GOAL]
case mk.mk.inr.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a b : α i
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b } ∨ { fst := i, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
obtain hab | hba := le_total a b
[GOAL]
case mk.mk.inr.inl.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a b : α i
hab : a ≤ b
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b } ∨ { fst := i, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.right _ hab)
[GOAL]
case mk.mk.inr.inl.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a b : α i
hba : b ≤ a
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b } ∨ { fst := i, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.right _ hba)
[GOAL]
case mk.mk.inr.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a : α i
j : ι
b : α j
hji : j < i
⊢ { fst := i, snd := a } ≤ { fst := j, snd := b } ∨ { fst := j, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.left _ _ hji)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ ⊥ ≤ { fst := a, snd := b }
[PROOFSTEP]
obtain rfl | ha := eq_bot_or_bot_lt a
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
b : α ⊥
⊢ ⊥ ≤ { fst := ⊥, snd := b }
[PROOFSTEP]
exact Lex.right _ bot_le
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ ⊥ ≤ { fst := a, snd := b }
[PROOFSTEP]
exact Lex.left _ _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ { fst := a, snd := b } ≤ ⊤
[PROOFSTEP]
obtain rfl | ha := eq_top_or_lt_top a
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
b : α ⊤
⊢ { fst := ⊤, snd := b } ≤ ⊤
[PROOFSTEP]
exact Lex.right _ le_top
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ { fst := a, snd := b } ≤ ⊤
[PROOFSTEP]
exact Lex.left _ _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨k, hi, hj⟩ := exists_between h
[GOAL]
case mk.mk.left.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c⟩ : Nonempty (α k) := inferInstance
[GOAL]
case mk.mk.left.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
c : α k
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c, ha⟩ := exists_gt a
[GOAL]
case mk.mk.left.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α i
ha : a < c
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, left _ _ h⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c, hb⟩ := exists_lt b
[GOAL]
case mk.mk.left.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α j
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨j, c⟩, left _ _ h, right _ hb⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, a < b
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨j, h⟩ := exists_gt i
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨b⟩ : Nonempty (α j) := inferInstance
[GOAL]
case mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
exact ⟨⟨j, b⟩, left _ _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, b < a
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨j, h⟩ := exists_lt i
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨b⟩ : Nonempty (α j) := inferInstance
[GOAL]
case mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
exact ⟨⟨j, b⟩, left _ _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, a < b
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨b, h⟩ := exists_gt a
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
exact ⟨⟨i, b⟩, right _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, b < a
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨b, h⟩ := exists_lt a
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : b < a
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
exact ⟨⟨i, b⟩, right _ h⟩


[GOAL]
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : FunLike F α β
f g : F
h : f = g
⊢ ↑f = ↑g
[PROOFSTEP]
cases h
[GOAL]
case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : FunLike F α β
f : F
⊢ ↑f = ↑f
[PROOFSTEP]
rfl


[GOAL]
n : ℕ
src✝ : Mul (Fin n) := inferInstanceAs (Mul (Fin n))
x✝² x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
⊢ a * b * c ≡ a * (b * c) [MOD n]
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
n : ℕ
x✝² x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
⊢ a * (b + c) ≡ a * b + a * c [MOD n]
[PROOFSTEP]
rw [mul_add]
[GOAL]
n : ℕ
src✝¹ : AddCommSemigroup (Fin n) := addCommSemigroup n
src✝ : CommSemigroup (Fin n) := instCommSemigroup n
a b c : Fin n
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]
[GOAL]
⊢ Repr (ZMod 0)
[PROOFSTEP]
dsimp [ZMod]
[GOAL]
⊢ Repr ℤ
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ Repr (ZMod (n + 1))
[PROOFSTEP]
dsimp [ZMod]
[GOAL]
n : ℕ
⊢ Repr (Fin (n + 1))
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n
[PROOFSTEP]
cases n with
| zero => exact (not_finite (ZMod 0)).elim
| succ n => convert Fintype.card_fin (n + 1) using 2
[GOAL]
n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n
[PROOFSTEP]
cases n with
| zero => exact (not_finite (ZMod 0)).elim
| succ n => convert Fintype.card_fin (n + 1) using 2
[GOAL]
case zero
inst✝ : Fintype (ZMod Nat.zero)
⊢ Fintype.card (ZMod Nat.zero) = Nat.zero
[PROOFSTEP]

| zero => exact (not_finite (ZMod 0)).elim
[GOAL]
case zero
inst✝ : Fintype (ZMod Nat.zero)
⊢ Fintype.card (ZMod Nat.zero) = Nat.zero
[PROOFSTEP]
exact (not_finite (ZMod 0)).elim
[GOAL]
case succ
n : ℕ
inst✝ : Fintype (ZMod (Nat.succ n))
⊢ Fintype.card (ZMod (Nat.succ n)) = Nat.succ n
[PROOFSTEP]

| succ n => convert Fintype.card_fin (n + 1) using 2
[GOAL]
case succ
n : ℕ
inst✝ : Fintype (ZMod (Nat.succ n))
⊢ Fintype.card (ZMod (Nat.succ n)) = Nat.succ n
[PROOFSTEP]
convert Fintype.card_fin (n + 1) using 2