internlm/Lean-Github huggingface dataset:
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
constructor
Proof state after:
case mp.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ K ≠ ⊤

case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ K ≠ ⊤
Tactic:
exact hK.ne_top
Proof state after:
no goals
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
intro H g hKH hgK hgH
Proof state after:
case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ H = ⊤
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ H = ⊤
Tactic:
apply (isMaximal_def.1 hK).2
Proof state after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K < H
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K < H
Tactic:
rw [← Ne.le_iff_lt]
Proof state after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≤ H

case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≤ H

case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H
Tactic:
exact hKH
Proof state after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H
Tactic:
rw [Ne.def]
Proof state after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ ¬K = H
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ ¬K = H
Tactic:
intro z
Proof state after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
z : K = H
⊢ False
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
z : K = H
⊢ False
Tactic:
rw [z] at hgK
Proof state after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ H
hgH : g ∈ H
z : K = H
⊢ False
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ H
hgH : g ∈ H
z : K = H
⊢ False
Tactic:
exact hgK hgH
Proof state after:
no goals
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ (K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤) → IsMaximal K
Tactic:
rintro ⟨hG, hmax⟩
Proof state after:
case mpr.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsMaximal K
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mpr.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsMaximal K
Tactic:
constructor
Proof state after:
case mpr.intro.out
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mpr.intro.out
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K
Tactic:
constructor
Proof state after:
case mpr.intro.out.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ K ≠ ⊤

case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ ∀ (b : Subgroup G), K < b → b = ⊤
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mpr.intro.out.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ K ≠ ⊤
Tactic:
assumption
Proof state after:
no goals
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ ∀ (b : Subgroup G), K < b → b = ⊤
Tactic:
intro H hKH
Proof state after:
case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
⊢ H = ⊤
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
⊢ H = ⊤
Tactic:
obtain ⟨g, hgH, hgK⟩ := Set.exists_of_ssubset hKH
Proof state after:
case mpr.intro.out.right.intro.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
g : G
hgH : g ∈ ↑H
hgK : g ∉ ↑K
⊢ H = ⊤
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mpr.intro.out.right.intro.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
g : G
hgH : g ∈ ↑H
hgK : g ∉ ↑K
⊢ H = ⊤
Tactic:
exact hmax H g (le_of_lt hKH) hgK hgH
Proof state after:
no goals
Theorem: Nat.Combination.mem_iff
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
⊢ s ∈ Combination α n ↔ s.card = n
Tactic:
unfold Combination
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
⊢ s ∈ {s | s.card = n} ↔ s.card = n
Theorem: Nat.Combination.mem_iff
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
⊢ s ∈ {s | s.card = n} ↔ s.card = n
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
no goals
Theorem: Nat.Combination.eq_iff_finset_subset
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ s = t ↔ ↑s ⊆ ↑t
Tactic:
constructor
Proof state after:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ s = t → ↑s ⊆ ↑t

case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ ↑s ⊆ ↑t → s = t
Theorem: Nat.Combination.eq_iff_finset_subset
Proof state before:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ s = t → ↑s ⊆ ↑t
Tactic:
intro h
Proof state after:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : s = t
⊢ ↑s ⊆ ↑t
Theorem: Nat.Combination.eq_iff_finset_subset
Proof state before:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : s = t
⊢ ↑s ⊆ ↑t
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Nat.Combination.eq_iff_finset_subset
Proof state before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ ↑s ⊆ ↑t → s = t
Tactic:
intro h
Proof state after:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ s = t
Theorem: Nat.Combination.eq_iff_finset_subset
Proof state before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ s = t
Tactic:
rw [← Subtype.coe_inj]
Proof state after:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ ↑s = ↑t
Theorem: Nat.Combination.eq_iff_finset_subset
Proof state before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ ↑s = ↑t
Tactic:
apply Finset.eq_of_subset_of_card_le h
Proof state after:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ (↑t).card ≤ (↑s).card
Theorem: Nat.Combination.eq_iff_finset_subset
Proof state before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ (↑t).card ≤ (↑s).card
Tactic:
rw [s.prop, t.prop]
Proof state after:
no goals
Theorem: Nat.combination_mulAction_apply
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n✝ n : ℕ
g : G
s : Finset α
hs : s ∈ Combination α n
⊢ g • s = g • ↑{ val := s, property := hs }
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s ≠ t ↔ ∃ a ∈ ↑s, a ∉ g⁻¹ • ↑t
Tactic:
simp only [ne_eq, exists_prop]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ∃ a ∈ ↑s, a ∉ g⁻¹ • ↑t
Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ∃ a ∈ ↑s, a ∉ g⁻¹ • ↑t
Tactic:
rw [← Finset.not_subset]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ¬↑s ⊆ g⁻¹ • ↑t
Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ¬↑s ⊆ g⁻¹ • ↑t
Tactic:
rw [not_iff_not]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ g⁻¹ • ↑t
Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ g⁻¹ • ↑t
Tactic:
rw [← Nat.combination_mulAction.coe_apply']
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ ↑(g⁻¹ • t)
Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ ↑(g⁻¹ • t)
Tactic:
rw [Nat.Combination.eq_iff_finset_subset]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ↑(g • s) ⊆ ↑t ↔ ↑s ⊆ ↑(g⁻¹ • t)
Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ↑(g • s) ⊆ ↑t ↔ ↑s ⊆ ↑(g⁻¹ • t)
Tactic:
simp only [Nat.combination_mulAction.coe_apply', Finset.le_eq_subset]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • ↑s ⊆ ↑t ↔ ↑s ⊆ g⁻¹ • ↑t
Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • ↑s ⊆ ↑t ↔ ↑s ⊆ g⁻¹ • ↑t
Tactic:
exact Finset.smul_finset_subset_iff
Proof state after:
no goals
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
⊢ ∃ s, g • s ≠ s
Tactic:
have zob : ∃ (a : α), (g • a : α) ≠ a := by
  by_contra h
  push_neg at h
  apply hg
  ext a
  simpa only using h a
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
zob : ∃ a, g • a ≠ a
⊢ ∃ s, g • s ≠ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
zob : ∃ a, g • a ≠ a
⊢ ∃ s, g • s ≠ s
Tactic:
obtain ⟨a, ha⟩ := zob
Proof state after:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ∃ s, g • s ≠ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
have : ({a} : Set α) ⊆ {g • a}ᶜ := by
  simp only [Set.subset_compl_singleton_iff, Set.mem_singleton_iff]
  exact ha
Proof state after:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
have hα' : n ≤ Set.encard ({g • a}ᶜ) := by
  rw [← not_lt, ← WithTop.add_one_lt_coe_succ_iff, not_lt, add_comm,
    ← Set.encard_singleton (g • a), Set.encard_add_encard_compl, Set.encard_univ]
  rw [← PartENat.withTopEquiv_natCast, PartENat.withTopEquiv_le]
  exact hα
Proof state after:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
obtain ⟨s, has, has', hs⟩ := Set.exists_superset_subset_encard_eq this (by
  rw [Set.encard_singleton, ← Nat.cast_one, Nat.cast_le]
  exact hn) hα'
Proof state after:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
use s
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
constructor
Proof state after:
case h.left
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n

case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ a ∈ s ∧ g • a ∉ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
⊢ ∃ a, g • a ≠ a
Tactic:
by_contra h
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ¬∃ a, g • a ≠ a
⊢ False
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ¬∃ a, g • a ≠ a
⊢ False
Tactic:
push_neg at h
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ False
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ False
Tactic:
apply hg
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ toPerm g = 1
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ toPerm g = 1
Tactic:
ext a
Proof state after:
case H
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
a : α
⊢ (toPerm g) a = 1 a
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case H
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
a : α
⊢ (toPerm g) a = 1 a
Tactic:
simpa only using h a
Proof state after:
no goals
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
⊢ ∃ s, g • s ≠ s
Tactic:
obtain ⟨s, hs, has, has'⟩ := this
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ ∃ s, g • s ≠ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ ∃ s, g • s ≠ s
Tactic:
have : Set.Finite s := Set.finite_of_encard_eq_coe hs
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
⊢ ∃ s, g • s ≠ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
⊢ ∃ s, g • s ≠ s
Tactic:
rw [Set.Finite.encard_eq_coe_toFinset_card this, cast_inj] at hs
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ∃ s, g • s ≠ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ∃ s, g • s ≠ s
Tactic:
use ⟨Set.Finite.toFinset this, hs⟩
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ g • { val := Set.Finite.toFinset this, property := hs } ≠ { val := Set.Finite.toFinset this, property := hs }