-- Mathlib/RingTheory/Fintype.lean
lemma Finset.univ_of_card_le_three (h : Fintype.card R ≤ 3) :
    (univ : Finset R) = {0, 1, -1}

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ 1 < Fintype.card R

Tactic:
rw [h]

Result:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ 1 < 3

Proof state:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ #univ ≤ #{0, 1, -1}

Tactic:
apply card_le_card

Result:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ univ ⊆ {0, 1, -1}

Proof state:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
a : R
ha : a ∈ {0, 1}
⊢ a ∈ {0, 1, -1}

Tactic:
simp only [mem_insert, mem_singleton] at ha

Result:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
a : R
ha : a = 0 ∨ a = 1
⊢ a ∈ {0, 1, -1}

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 1 = -1
⊢ False

Tactic:
rw [← add_eq_zero_iff_eq_neg, one_add_one_eq_two] at H

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 2 = 0
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 3
⊢ #univ ≤ #{0, 1, -1}

Tactic:
rcases lt_or_eq_of_le h with h | h

Result:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ #univ ≤ #{0, 1, -1}

case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ #univ ≤ #{0, 1, -1}

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 0 = 1 ∨ 1 = 0
⊢ False

Tactic:
rcases h with (h | h)

Result:
case inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 0 = 1
⊢ False

case inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 1 = 0
⊢ False

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : (ringEquivOfPrime R Nat.prime_three h).symm 2 = (ringEquivOfPrime R Nat.prime_three h).symm 0
⊢ False

Tactic:
simp only [map_ofNat, map_zero] at H

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 2 = 0
⊢ False

Proof state:
case inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 1 = 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ #univ ≤ #{0, 1, -1}

Tactic:
rw [card_univ, h, card_insert_of_not_mem, card_insert_of_not_mem, card_singleton]

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 1 ∉ {-1}

case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 0 ∉ {1, -1}

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 3 ∣ 2
⊢ False

Tactic:
norm_num at H

Result:
no goals

Proof state:
case inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 0 = 1
⊢ False

Tactic:
exact zero_ne_one h

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ #univ ≤ #{0, 1, -1}

Tactic:
have : Nontrivial R := by
  refine Fintype.one_lt_card_iff_nontrivial.1 ?_
  rw [h]
  norm_num

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ #univ ≤ #{0, 1, -1}

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ 1 < 3

Tactic:
norm_num

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 0 ∉ {1, -1}

Tactic:
intro h

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 0 ∈ {1, -1}
⊢ False

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 1 ∉ {-1}

Tactic:
rw [mem_singleton]

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ ¬1 = -1

Proof state:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ univ ⊆ {0, 1, -1}

Tactic:
rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]

Result:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ {0, 1} ⊆ {0, 1, -1}

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : ↑2 = 0
⊢ False

Tactic:
rw [natCast_zmod_eq_zero_iff_dvd] at H

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 3 ∣ 2
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 3
⊢ univ = {0, 1, -1}

Tactic:
refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm

Result:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 3
⊢ #univ ≤ #{0, 1, -1}

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ ¬1 = -1

Tactic:
intro H

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 1 = -1
⊢ False

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 2 = 0
⊢ False

Tactic:
apply_fun (ringEquivOfPrime R Nat.prime_three h).symm at H

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : (ringEquivOfPrime R Nat.prime_three h).symm 2 = (ringEquivOfPrime R Nat.prime_three h).symm 0
⊢ False

Proof state:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
a : R
ha : a = 0 ∨ a = 1
⊢ a ∈ {0, 1, -1}

Tactic:
rcases ha with rfl | rfl <;> simp

Result:
no goals