Theorem: self_is_subgroup (src/Group.lean)

State before:
α : Type u_1
G : group α
⊢ subgroup G whole_group
Tactic:
have hmul_mem : ∀ a b : α, a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group := by
  rw [whole_group]
  intros a b _ _
  rw [Membership.mem, instMembershipSet]
  simp
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ subgroup G whole_group

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ subgroup G whole_group
Tactic:
have hone_mem : G.one ∈ whole_group := by
  rw [Membership.mem, instMembershipSet]
  simp
  rw [Set.isMember, whole_group]
  simp
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
⊢ subgroup G whole_group

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
⊢ subgroup G whole_group
Tactic:
have hinv_mem : ∀ a : α, a ∈ whole_group → G.inv a ∈ whole_group := by
  intros a _
  rw [Membership.mem, instMembershipSet]
  simp
  rw [Set.isMember, whole_group]
  simp
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
hinv_mem : ∀ (a : α), a ∈ whole_group → group.inv a ∈ whole_group
⊢ subgroup G whole_group

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
hinv_mem : ∀ (a : α), a ∈ whole_group → group.inv a ∈ whole_group
⊢ subgroup G whole_group
Tactic:
exact {
  mul_mem := hmul_mem
  one_mem := hone_mem
  inv_mem := hinv_mem
}
State after:
no goals

State before:
α : Type u_1
G : group α
⊢ ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
Tactic:
rw [whole_group]
State after:
α : Type u_1
G : group α
⊢ ∀ (a b : α),
    a ∈ { isMember := fun x => True } → b ∈ { isMember := fun x => True } → a * b ∈ { isMember := fun x => True }

State before:
α : Type u_1
G : group α
⊢ ∀ (a b : α),
    a ∈ { isMember := fun x => True } → b ∈ { isMember := fun x => True } → a * b ∈ { isMember := fun x => True }
Tactic:
intros a b _ _
State after:
α : Type u_1
G : group α
a b : α
a✝¹ : a ∈ { isMember := fun x => True }
a✝ : b ∈ { isMember := fun x => True }
⊢ a * b ∈ { isMember := fun x => True }

State before:
α : Type u_1
G : group α
a b : α
a✝¹ : a ∈ { isMember := fun x => True }
a✝ : b ∈ { isMember := fun x => True }
⊢ a * b ∈ { isMember := fun x => True }
Tactic:
rw [Membership.mem, instMembershipSet]
State after:
α : Type u_1
G : group α
a b : α
a✝¹ : a ∈ { isMember := fun x => True }
a✝ : b ∈ { isMember := fun x => True }
⊢ { mem := fun x s => Set.isMember x }.1 (a * b) { isMember := fun x => True }

State before:
α : Type u_1
G : group α
a b : α
a✝¹ : a ∈ { isMember := fun x => True }
a✝ : b ∈ { isMember := fun x => True }
⊢ { mem := fun x s => Set.isMember x }.1 (a * b) { isMember := fun x => True }
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ has_one.one ∈ whole_group
Tactic:
rw [Membership.mem, instMembershipSet]
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one whole_group

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one whole_group
Tactic:
simp
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ Set.isMember has_one.one

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ Set.isMember has_one.one
Tactic:
rw [Set.isMember, whole_group]
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ { isMember := fun x => True }.1 has_one.one

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
⊢ { isMember := fun x => True }.1 has_one.one
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
⊢ ∀ (a : α), a ∈ whole_group → group.inv a ∈ whole_group
Tactic:
intros a _
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ group.inv a ∈ whole_group

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ group.inv a ∈ whole_group
Tactic:
rw [Membership.mem, instMembershipSet]
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ { mem := fun x s => Set.isMember x }.1 (group.inv a) whole_group

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ { mem := fun x s => Set.isMember x }.1 (group.inv a) whole_group
Tactic:
simp
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ Set.isMember (group.inv a)

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ Set.isMember (group.inv a)
Tactic:
rw [Set.isMember, whole_group]
State after:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ { isMember := fun x => True }.1 (group.inv a)

State before:
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
a : α
a✝ : a ∈ whole_group
⊢ { isMember := fun x => True }.1 (group.inv a)
Tactic:
simp
State after:
no goals