internlm/Lean-Github huggingface dataset:
Theorem: MulAction.AlternatingGroup.isPreprimitive
Proof state before:
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Tactic:
have := alternatingGroup.isPretransitive h
Proof state after:
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Theorem: MulAction.AlternatingGroup.isPreprimitive
Proof state before:
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ ∀ {B : Set α}, IsBlock (↥(alternatingGroup α)) B → IsTrivialBlock B
Theorem: MulAction.AlternatingGroup.isPreprimitive
Proof state before:
case has_trivial_blocks'
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ ∀ {B : Set α}, IsBlock (↥(alternatingGroup α)) B → IsTrivialBlock B
Tactic:
apply alternatingGroup.has_trivial_blocks
Proof state after:
no goals
Theorem: arrowAction.mem_stabilizer_iff
Proof state before:
α : Type u_1
ι : Type u_2
p : α → ι
g : Perm α
⊢ g ∈ stabilizer (Perm α) p ↔ p ∘ ⇑g = p
Tactic:
rw [eq_comm, ← g.comp_symm_eq]
Proof state after:
α : Type u_1
ι : Type u_2
p : α → ι
g : Perm α
⊢ g ∈ stabilizer (Perm α) p ↔ p ∘ ⇑g.symm = p
Theorem: arrowAction.mem_stabilizer_iff
Proof state before:
α : Type u_1
ι : Type u_2
p : α → ι
g : Perm α
⊢ g ∈ stabilizer (Perm α) p ↔ p ∘ ⇑g.symm = p
Tactic:
rfl
Proof state after:
no goals
Theorem: φ_invFun_eq
Proof state before:
α : Type u_1
ι : Type u_2
p : α → ι
g : (i : ι) → Perm ↑{a | p a = i}
a : α
i : ι
h : p a = i
⊢ φ_invFun g a = ↑((g i) { val := a, property := h })
Tactic:
subst h
Proof state after:
α : Type u_1
ι : Type u_2
p : α → ι
g : (i : ι) → Perm ↑{a | p a = i}
a : α
⊢ φ_invFun g a = ↑((g (p a)) { val := a, property := ⋯ })
Theorem: φ_invFun_eq
Proof state before:
α : Type u_1
ι : Type u_2
p : α → ι
g : (i : ι) → Perm ↑{a | p a = i}
a : α
⊢ φ_invFun g a = ↑((g (p a)) { val := a, property := ⋯ })
Tactic:
rfl
Proof state after:
no goals
Theorem: MonoidHom.range_isCommutative
Proof state before:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ Subgroup.IsCommutative (range f)
Tactic:
apply Subgroup.IsCommutative.mk
Proof state after:
case is_comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ Std.Commutative fun x x_1 => x * x_1
Theorem: MonoidHom.range_isCommutative
Proof state before:
case is_comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
constructor
Proof state after:
case is_comm.comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ ∀ (a b : ↥(range f)), a * b = b * a
Theorem: MonoidHom.range_isCommutative
Proof state before:
case is_comm.comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ ∀ (a b : ↥(range f)), a * b = b * a
Tactic:
rintro ⟨_, a, rfl⟩ ⟨_, b, rfl⟩
Proof state after:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ { val := f a, property := ⋯ } * { val := f b, property := ⋯ } =
    { val := f b, property := ⋯ } * { val := f a, property := ⋯ }
Theorem: MonoidHom.range_isCommutative
Proof state before:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ { val := f a, property := ⋯ } * { val := f b, property := ⋯ } =
    { val := f b, property := ⋯ } * { val := f a, property := ⋯ }
Tactic:
rw [← Subtype.coe_inj]
Proof state after:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ ↑({ val := f a, property := ⋯ } * { val := f b, property := ⋯ }) =
    ↑({ val := f b, property := ⋯ } * { val := f a, property := ⋯ })
Theorem: MonoidHom.range_isCommutative
Proof state before:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ ↑({ val := f a, property := ⋯ } * { val := f b, property := ⋯ }) =
    ↑({ val := f b, property := ⋯ } * { val := f a, property := ⋯ })
Tactic:
simp only [Submonoid.coe_mul, ← map_mul, hG.comm]
Proof state after:
no goals
Theorem: Equiv.perm_is_nontrivial
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ 1 < Fintype.card α ↔ Nontrivial (Perm α)
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, Fintype.card_perm, Nat.one_lt_factorial]
Proof state after:
no goals
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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]
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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⟩
Proof state after:
no goals
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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]
Proof state after:
no goals
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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]
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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]
Proof state after:
no goals
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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]
Proof 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
Theorem: Monoid.isCommutative_of_fintype_card_le_2
Proof 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]
Proof state after:
no goals
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2
Tactic:
cases' Nat.lt_or_ge 2 (Fintype.card α) with hα hα
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2
Tactic:
rw [← not_lt]
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ ¬2 < Fintype.card α
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ ¬2 < Fintype.card α
Tactic:
simp only [hα, not_true_eq_false, iff_false]
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ ¬Std.Commutative fun x x_1 => x * x_1
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ ¬Std.Commutative fun x x_1 => x * x_1
Tactic:
intro h
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
h : Std.Commutative fun x x_1 => x * x_1
⊢ False
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
h : Std.Commutative fun x x_1 => x * x_1
⊢ False
Tactic:
rw [Fintype.two_lt_card_iff] at hα
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
h : Std.Commutative fun x x_1 => x * x_1
⊢ False
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
h : Std.Commutative fun x x_1 => x * x_1
⊢ False
Tactic:
obtain ⟨a, b, c, hab, hac, hbc⟩ := hα
Proof state after:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ False
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ False
Tactic:
apply hbc
Proof state after:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c
Tactic:
convert Equiv.ext_iff.mp (h.comm (Equiv.swap a c) (Equiv.swap a b)) a
Proof state after:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = (swap a c * swap a b) a

case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = (swap a c * swap a b) a

case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a
Tactic:
rw [coe_mul, Function.comp_apply,
  Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne hab.symm hbc]
Proof state after:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a
Tactic:
rw [coe_mul, Function.comp_apply,
  Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne hac.symm hbc.symm]
Proof state after:
no goals
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2
Tactic:
simp only [hα, iff_true]
Proof state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Std.Commutative fun x x_1 => x * x_1
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
apply Monoid.isCommutative_of_fintype_card_le_2
Proof state after:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Fintype.card (Perm α) ≤ 2
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Fintype.card (Perm α) ≤ 2
Tactic:
rw [← Nat.factorial_two, Fintype.card_perm]
Proof state after:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2
Theorem: Equiv.Perm.isCommutative_iff
Proof state before:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2
Tactic:
exact Nat.factorial_le hα
Proof state after:
no goals
Theorem: SubMulAction.image_inclusion
Proof state before:
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
⊢ Set.range ⇑(inclusion s) = s.carrier
Tactic:
ext a
Proof state after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ Set.range ⇑(inclusion s) ↔ a ∈ s.carrier
Theorem: SubMulAction.image_inclusion
Proof state before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ Set.range ⇑(inclusion s) ↔ a ∈ s.carrier
Tactic:
simp only [Set.mem_range, Subtype.exists, mem_carrier, SetLike.mem_coe]
Proof state after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) ↔ a ∈ s
Theorem: SubMulAction.image_inclusion
Proof state before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) ↔ a ∈ s
Tactic:
constructor
Proof state after:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) → a ∈ s

case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ s → ∃ a_2, ∃ (b : a_2 ∈ s), (inclusion s) { val := a_2, property := b } = a
Theorem: SubMulAction.image_inclusion
Proof state before:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) → a ∈ s
Tactic:
intro ha
Proof state after:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a
⊢ a ∈ s
Theorem: SubMulAction.image_inclusion
Proof state before:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a
⊢ a ∈ s
Tactic:
obtain ⟨a, h, rfl⟩ := ha
Proof state after:
case h.mp.intro.intro
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } ∈ s
Theorem: SubMulAction.image_inclusion
Proof state before:
case h.mp.intro.intro
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: SubMulAction.image_inclusion
Proof state before:
case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ s → ∃ a_2, ∃ (b : a_2 ∈ s), (inclusion s) { val := a_2, property := b } = a
Tactic:
intro h
Proof state after:
case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a
Theorem: SubMulAction.image_inclusion
Proof state before:
case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a
Tactic:
use a
Proof state after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ (b : a ∈ s), (inclusion s) { val := a, property := b } = a
Theorem: SubMulAction.image_inclusion
Proof state before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ (b : a ∈ s), (inclusion s) { val := a, property := b } = a
Tactic:
use h
Proof state after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } = a
Theorem: SubMulAction.image_inclusion
Proof state before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } = a
Tactic:
rfl
Proof state after:
no goals
Theorem: SubMulAction.inclusion_injective
Proof state before:
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
⊢ Function.Injective ⇑(inclusion s)
Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩ h
Proof state after:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ { val := a, property := ha } = { val := b, property := hb }
Theorem: SubMulAction.inclusion_injective
Proof state before:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ { val := a, property := ha } = { val := b, property := hb }
Tactic:
simp only [Subtype.mk.injEq]
Proof state after:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ a = b
Theorem: SubMulAction.inclusion_injective
Proof state before:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ a = b
Tactic:
exact h
Proof state after:
no goals