Theorem: triv_is_subgroup (src/Group.lean)

State before:
α : Type u_1
G : group α
⊢ subgroup G (trivial_subgroup G)
Tactic:
let H := trivial_subgroup G
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)
Tactic:
have hH : H = trivial_subgroup G := by simp
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)
Tactic:
rw [← hH]
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G H
Tactic:
have hmul_mem : ∀ a b : α, a ∈ H → b ∈ H → a * b ∈ H := by
  intros a b ha hb
  rw [Membership.mem, instMembershipSet] at ha
  simp at ha
  rw [Set.isMember, trivial_subgroup] at ha
  simp at ha
  rw [Membership.mem, instMembershipSet] at hb
  simp at hb
  rw [Set.isMember, trivial_subgroup] at hb
  simp at hb
  rw [ha, hb]
  rw [G.mul_one]
  simp
  rw [trivial_subgroup, Membership.mem, instMembershipSet]
  simp
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ subgroup G H

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

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

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
hinv_mem : ∀ (a : α), a ∈ H → group.inv a ∈ H
⊢ subgroup G H
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 α
H : Set α := trivial_subgroup G
⊢ H = trivial_subgroup G
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
Tactic:
intros a b ha hb
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a ∈ H
hb : b ∈ H
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a ∈ H
hb : b ∈ H
⊢ a * b ∈ H
Tactic:
rw [Membership.mem, instMembershipSet] at ha
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : { mem := fun x s => Set.isMember x }.1 a H
hb : b ∈ H
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : { mem := fun x s => Set.isMember x }.1 a H
hb : b ∈ H
⊢ a * b ∈ H
Tactic:
simp at ha
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : Set.isMember a
hb : b ∈ H
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : Set.isMember a
hb : b ∈ H
⊢ a * b ∈ H
Tactic:
rw [Set.isMember, trivial_subgroup] at ha
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : { isMember := fun x => x = has_one.one }.1 a
hb : b ∈ H
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : { isMember := fun x => x = has_one.one }.1 a
hb : b ∈ H
⊢ a * b ∈ H
Tactic:
simp at ha
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b ∈ H
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b ∈ H
⊢ a * b ∈ H
Tactic:
rw [Membership.mem, instMembershipSet] at hb
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : { mem := fun x s => Set.isMember x }.1 b H
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : { mem := fun x s => Set.isMember x }.1 b H
⊢ a * b ∈ H
Tactic:
simp at hb
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : Set.isMember b
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : Set.isMember b
⊢ a * b ∈ H
Tactic:
rw [Set.isMember, trivial_subgroup] at hb
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : { isMember := fun x => x = has_one.one }.1 b
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : { isMember := fun x => x = has_one.one }.1 b
⊢ a * b ∈ H
Tactic:
simp at hb
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ a * b ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ a * b ∈ H
Tactic:
rw [ha, hb]
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one * has_one.one ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one * has_one.one ∈ H
Tactic:
rw [G.mul_one]
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ H
Tactic:
simp
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ trivial_subgroup G

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ trivial_subgroup G
Tactic:
rw [trivial_subgroup, Membership.mem, instMembershipSet]
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun x => x = has_one.one }

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun x => x = has_one.one }
Tactic:
simp
State after:
no goals

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

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

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ Set.isMember has_one.one
Tactic:
rw [Set.isMember, trivial_subgroup]
State after:
no goals

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
⊢ ∀ (a : α), a ∈ H → group.inv a ∈ H
Tactic:
intros a ha
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a ∈ H
⊢ group.inv a ∈ H

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

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

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

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

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a = has_one.one
⊢ group.inv a ∈ H
Tactic:
rw [ha]
State after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a = has_one.one
⊢ group.inv has_one.one ∈ H

State before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a = has_one.one
⊢ group.inv has_one.one ∈ H
Tactic:
apply inv_one_eq_one
State after:
no goals