Theorem: Monoid.isCommutative_of_fintype_card_le_2 (Jordan/Mathlib/GroupTheory/Subgroup/Basic.lean)

State before:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
⊢ ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
Tactic:
by_contra h
State after:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
h : ¬∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
⊢ False

State before:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
h : ¬∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
⊢ False
Tactic:
apply not_lt.mpr hG
State after:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
h : ¬∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
⊢ 2 < Fintype.card G

State before:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
h : ¬∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
⊢ 2 < Fintype.card G
Tactic:
push_neg at h
State after:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
h : ∃ a b, a ≠ 1 ∧ b ≠ 1 ∧ a ≠ b
⊢ 2 < Fintype.card G

State before:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
h : ∃ a b, a ≠ 1 ∧ b ≠ 1 ∧ a ≠ b
⊢ 2 < Fintype.card G
Tactic:
obtain ⟨a, b, ha1, hb1, hab⟩ := h
State after:
case intro.intro.intro.intro
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
a b : G
ha1 : a ≠ 1
hb1 : b ≠ 1
hab : a ≠ b
⊢ 2 < Fintype.card G

State before:
case intro.intro.intro.intro
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
a b : G
ha1 : a ≠ 1
hb1 : b ≠ 1
hab : a ≠ b
⊢ 2 < Fintype.card G
Tactic:
rw [Fintype.two_lt_card_iff]
State after:
case intro.intro.intro.intro
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
a b : G
ha1 : a ≠ 1
hb1 : b ≠ 1
hab : a ≠ b
⊢ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

State before:
case intro.intro.intro.intro
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
a b : G
ha1 : a ≠ 1
hb1 : b ≠ 1
hab : a ≠ b
⊢ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic:
exact ⟨a, b, 1, hab, ha1, hb1⟩
State after:
no goals

State before:
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
constructor
State after:
case comm
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
⊢ ∀ (a b : G), a * b = b * a

State before:
case comm
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
⊢ ∀ (a b : G), a * b = b * a
Tactic:
intro a b
State after:
case comm
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
⊢ a * b = b * a

State before:
case comm
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
⊢ a * b = b * a
Tactic:
cases' dec_em (a = 1) with ha ha
State after:
case comm.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : a = 1
⊢ a * b = b * a

case comm.inr
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
⊢ a * b = b * a

State before:
case comm.inr
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
⊢ a * b = b * a
Tactic:
cases' dec_em (b = 1) with hb hb
State after:
case comm.inr.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
hb : b = 1
⊢ a * b = b * a

case comm.inr.inr
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
hb : ¬b = 1
⊢ a * b = b * a

State before:
case comm.inr.inr
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
hb : ¬b = 1
⊢ a * b = b * a
Tactic:
rw [this a b ha hb]
State after:
no goals

State before:
case comm.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : a = 1
⊢ a * b = b * a
Tactic:
rw [ha]
State after:
case comm.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : a = 1
⊢ 1 * b = b * 1

State before:
case comm.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : a = 1
⊢ 1 * b = b * 1
Tactic:
simp only [one_mul, mul_one]
State after:
no goals

State before:
case comm.inr.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
hb : b = 1
⊢ a * b = b * a
Tactic:
rw [hb]
State after:
case comm.inr.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
hb : b = 1
⊢ a * 1 = 1 * a

State before:
case comm.inr.inl
G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Fintype G
inst✝ : Monoid G
hG : Fintype.card G ≤ 2
this : ∀ (a b : G), a ≠ 1 → b ≠ 1 → a = b
a b : G
ha : ¬a = 1
hb : b = 1
⊢ a * 1 = 1 * a
Tactic:
simp only [one_mul, mul_one]
State after:
no goals