internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
let f : s →ₑ[φ] s :=
  { toFun := id
    map_smul' := fun ⟨⟨m, hm'⟩, hm⟩ ⟨a, ha⟩ => rfl }
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
have hf : Function.Surjective f := Function.surjective_id
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
apply isPreprimitive_of_surjective_map hf
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Tactic:
apply stabilizer.isPreprimitive
Proof state after:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ Set.Nontrivial sᶜ
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ Set.Nontrivial sᶜ
Tactic:
exact hsc
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↥(stabilizer (↥G) s)
Tactic:
use! (g : alternatingGroup α)
Proof state after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ G

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ?property } ∈ stabilizer (↥G) s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ G

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ?property } ∈ stabilizer (↥G) s
Tactic:
apply hG
Proof state after:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Tactic:
rw [Subgroup.mem_inf]
Proof state after:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ∧ ↑↑g ∈ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ∧ ↑↑g ∈ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Tactic:
constructor
Proof state after:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s

case property.a.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Tactic:
exact g.prop
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s
Tactic:
let h := g.prop
Proof state after:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g ∈ stabilizer (↥(alternatingGroup α)) s := Subtype.prop g
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g ∈ stabilizer (↥(alternatingGroup α)) s := Subtype.prop g
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s
Tactic:
rw [mem_stabilizer_iff] at h ⊢
Proof state after:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g • s = s
⊢ ↑↑g • s = s
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g • s = s
⊢ ↑↑g • s = s
Tactic:
exact h
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive'
Proof state before:
case property.a.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ alternatingGroup α
Tactic:
exact SetLike.coe_mem _
Proof state after:
no goals
Theorem: Set.one_lt_encard_iff_nontrivial
Proof state before:
α : Type u_1
s : Set α
⊢ 1 < encard s ↔ Set.Nontrivial s
Tactic:
unfold Set.Nontrivial
Proof state after:
α : Type u_1
s : Set α
⊢ 1 < encard s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
Theorem: Set.one_lt_encard_iff_nontrivial
Proof state before:
α : Type u_1
s : Set α
⊢ 1 < encard s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
Tactic:
rw [Set.one_lt_encard_iff]
Proof state after:
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
Theorem: Set.one_lt_encard_iff_nontrivial
Proof state before:
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) → ∃ x ∈ s, ∃ y ∈ s, x ≠ y

case mpr
α : Type u_1
s : Set α
⊢ (∃ x ∈ s, ∃ y ∈ s, x ≠ y) → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Theorem: Set.one_lt_encard_iff_nontrivial
Proof state before:
case mp
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) → ∃ x ∈ s, ∃ y ∈ s, x ≠ y

case mpr
α : Type u_1
s : Set α
⊢ (∃ x ∈ s, ∃ y ∈ s, x ≠ y) → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic:
all_goals {
  rintro ⟨a, b, c, d, e⟩
  exact ⟨a, c, b, d, e⟩ }
Proof state after:
no goals
Theorem: Set.one_lt_encard_iff_nontrivial
Proof state before:
case mpr
α : Type u_1
s : Set α
⊢ (∃ x ∈ s, ∃ y ∈ s, x ≠ y) → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic:
rintro ⟨a, b, c, d, e⟩
Proof state after:
case mpr.intro.intro.intro.intro
α : Type u_1
s : Set α
a : α
b : a ∈ s
c : α
d : c ∈ s
e : a ≠ c
⊢ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Theorem: Set.one_lt_encard_iff_nontrivial
Proof state before:
case mpr.intro.intro.intro.intro
α : Type u_1
s : Set α
a : α
b : a ∈ s
c : α
d : c ∈ s
e : a ≠ c
⊢ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic:
exact ⟨a, c, b, d, e⟩
Proof state after:
no goals
Theorem: Set.one_lt_ncard_iff_nontrivial
Proof state before:
α : Type u_1
s : Set α
inst✝ : Finite ↑s
⊢ 1 < ncard s ↔ Set.Nontrivial s
Tactic:
rw [← Set.one_lt_encard_iff_nontrivial, ← Set.Finite.cast_ncard_eq (toFinite s),
  Nat.one_lt_cast]
Proof state after:
no goals
Theorem: Set.subsingleton_iff_encard_le_one
Proof state before:
α✝ : Type u_1
α : Type u_2
B : Set α
⊢ Set.Subsingleton B ↔ encard B ≤ 1
Tactic:
rw [← Set.not_nontrivial_iff, not_iff_comm, not_le, Set.one_lt_encard_iff_nontrivial]
Proof state after:
no goals
Theorem: Set.subsingleton_iff_ncard_le_one
Proof state before:
α✝ : Type u_1
α : Type u_2
inst✝ : Finite α
B : Set α
⊢ Set.Subsingleton B ↔ ncard B ≤ 1
Tactic:
rw [← Set.not_nontrivial_iff, not_iff_comm, not_le, ← Set.one_lt_ncard_iff_nontrivial]
Proof state after:
no goals
Theorem: Set.eq_top_iff_ncard
Proof state before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ B = ⊤ ↔ ncard B = Fintype.card α
Tactic:
rw [top_eq_univ, ← Set.compl_empty_iff, ← Set.ncard_eq_zero]
Proof state after:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Fintype.card α
Theorem: Set.eq_top_iff_ncard
Proof state before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Fintype.card α
Tactic:
rw [← Nat.card_eq_fintype_card]
Proof state after:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Nat.card α
Theorem: Set.eq_top_iff_ncard
Proof state before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Nat.card α
Tactic:
rw [← Set.ncard_add_ncard_compl B]
Proof state after:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = ncard B + ncard Bᶜ
Theorem: Set.eq_top_iff_ncard
Proof state before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = ncard B + ncard Bᶜ
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 → ncard B = ncard B + ncard Bᶜ

case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard B = ncard B + ncard Bᶜ → ncard Bᶜ = 0
Theorem: Set.eq_top_iff_ncard
Proof state before:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 → ncard B = ncard B + ncard Bᶜ
Tactic:
intro H
Proof state after:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard Bᶜ = 0
⊢ ncard B = ncard B + ncard Bᶜ
Theorem: Set.eq_top_iff_ncard
Proof state before:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard Bᶜ = 0
⊢ ncard B = ncard B + ncard Bᶜ
Tactic:
rw [H, add_zero]
Proof state after:
no goals
Theorem: Set.eq_top_iff_ncard
Proof state before:
case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard B = ncard B + ncard Bᶜ → ncard Bᶜ = 0
Tactic:
intro H
Proof state after:
case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard B = ncard B + ncard Bᶜ
⊢ ncard Bᶜ = 0
Theorem: Set.eq_top_iff_ncard
Proof state before:
case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard B = ncard B + ncard Bᶜ
⊢ ncard Bᶜ = 0
Tactic:
exact Nat.add_left_cancel H.symm
Proof state after:
no goals
Theorem: WithTop.add_eq_add_iff
Proof state before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ c + ↑m = ↑n + ↑m ↔ c = ↑n
Tactic:
rw [WithTop.add_right_cancel_iff]
Proof state after:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤
Theorem: WithTop.add_eq_add_iff
Proof state before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤
Tactic:
exact WithTop.coe_ne_top
Proof state after:
no goals
Theorem: WithTop.add_one_eq_coe_succ_iff
Proof state before:
α : Type u_1
c : ℕ∞
n : ℕ
⊢ c + 1 = ↑(Nat.succ n) ↔ c = ↑n
Tactic:
rw [← Nat.cast_one, Nat.succ_eq_add_one, Nat.cast_add, WithTop.add_eq_add_iff]
Proof state after:
no goals
Theorem: WithTop.add_coe_lt_add_iff
Proof state before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ c + ↑m < ↑n + ↑m ↔ c < ↑n
Tactic:
rw [WithTop.add_lt_add_iff_right]
Proof state after:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤
Theorem: WithTop.add_coe_lt_add_iff
Proof state before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤
Tactic:
exact WithTop.coe_ne_top
Proof state after:
no goals
Theorem: WithTop.add_one_lt_coe_succ_iff
Proof state before:
α : Type u_1
c : ℕ∞
n : ℕ
⊢ c + 1 < ↑(Nat.succ n) ↔ c < ↑n
Tactic:
rw [← Nat.cast_one, Nat.succ_eq_add_one, Nat.cast_add, WithTop.add_coe_lt_add_iff]
Proof state after:
no goals
Theorem: WithTop.add_coe_le_add_iff
Proof state before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤
Tactic:
exact WithTop.coe_ne_top
Proof state after:
no goals
Theorem: WithTop.add_one_le_coe_succ_iff
Proof state before:
α : Type u_1
c : ℕ∞
n : ℕ
⊢ c + 1 ≤ ↑(Nat.succ n) ↔ c ≤ ↑n
Tactic:
rw [← Nat.cast_one, Nat.succ_eq_add_one, Nat.cast_add, WithTop.add_coe_le_add_iff]
Proof state after:
no goals
Theorem: WithTop.coe_lt_iff_succ_le
Proof state before:
α : Type u_1
n : ℕ
c : ℕ∞
⊢ ↑n < c ↔ ↑(Nat.succ n) ≤ c
Tactic:
induction c using WithTop.recTopCoe with
| top =>
  simp only [Nat.cast_succ, le_top, iff_true]
  apply WithTop.coe_lt_top
| coe m =>
  simp only [ENat.some_eq_coe, Nat.cast_lt, Nat.cast_le]
  exact Nat.lt_iff_add_one_le
Proof state after:
no goals
Theorem: WithTop.coe_lt_iff_succ_le
Proof state before:
case top
α : Type u_1
n : ℕ
⊢ ↑n < ⊤ ↔ ↑(Nat.succ n) ≤ ⊤
Tactic:
simp only [Nat.cast_succ, le_top, iff_true]
Proof state after:
case top
α : Type u_1
n : ℕ
⊢ ↑n < ⊤
Theorem: WithTop.coe_lt_iff_succ_le
Proof state before:
case top
α : Type u_1
n : ℕ
⊢ ↑n < ⊤
Tactic:
apply WithTop.coe_lt_top
Proof state after:
no goals
Theorem: WithTop.coe_lt_iff_succ_le
Proof state before:
case coe
α : Type u_1
n m : ℕ
⊢ ↑n < ↑m ↔ ↑(Nat.succ n) ≤ ↑m
Tactic:
simp only [ENat.some_eq_coe, Nat.cast_lt, Nat.cast_le]
Proof state after:
case coe
α : Type u_1
n m : ℕ
⊢ n < m ↔ Nat.succ n ≤ m
Theorem: WithTop.coe_lt_iff_succ_le
Proof state before:
case coe
α : Type u_1
n m : ℕ
⊢ n < m ↔ Nat.succ n ≤ m
Tactic:
exact Nat.lt_iff_add_one_le
Proof state after:
no goals
Theorem: Function.Injective.image_iInter_eq
Proof state before:
α✝ : Type u_1
α : Type u_3
β : Type u_4
G : Type ?u.14473
X : Type ?u.14476
ι : Sort u_2
κ : ι → Sort ?u.14484
inst✝ : Nonempty ι
f : α → β
hf : Injective f
s : ι → Set α
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i
Tactic:
rw [Set.InjOn.image_iInter_eq (Set.injOn_of_injective hf _)]
Proof state after:
no goals
Theorem: Set.subset_of_eq
Proof state before:
α✝¹ : Type u_1
α✝ : Type ?u.14727
β : Type ?u.14730
G : Type ?u.14733
X : Type ?u.14736
ι : Sort ?u.14739
κ : ι → Sort ?u.14744
α : Type u_2
s t : Set α
h : s = t
⊢ s ⊆ t
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MulAction.smul_set_iInter
Proof state before:
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
⊢ a • ⋂ i, s i = ⋂ i, a • s i
Tactic:
obtain _ | _ := isEmpty_or_nonempty ι
Proof state after:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i

case inr
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : Nonempty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i
Theorem: MulAction.smul_set_iInter
Proof state before:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i
Tactic:
refine' Eq.trans _ (Set.iInter_of_empty _).symm
Proof state after:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = Set.univ
Theorem: MulAction.smul_set_iInter
Proof state before:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = Set.univ
Tactic:
rw [Set.iInter_of_empty]
Proof state after:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • Set.univ = Set.univ
Theorem: MulAction.smul_set_iInter
Proof state before:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • Set.univ = Set.univ
Tactic:
exact Set.smul_set_univ
Proof state after:
no goals
Theorem: MulAction.smul_set_iInter
Proof state before:
case inr
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : Nonempty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i
Tactic:
exact (MulAction.injective _).image_iInter_eq _
Proof state after:
no goals
Theorem: MulAction.smul_set_iInter₂
Proof state before:
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.20290
X : Type ?u.20293
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : (i : ι) → κ i → Set β
⊢ a • ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, a • s i j
Tactic:
simp_rw [smul_set_iInter]
Proof state after:
no goals
Theorem: Subgroup.isMaximal_iff
Proof state before:
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ IsMaximal K ↔ K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
constructor
Proof state after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ IsMaximal K → K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤

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
Theorem: Subgroup.isMaximal_iff
Proof state before:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ IsMaximal K → K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
intro hK
Proof state after:
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 = ⊤