internlm/Lean-Github huggingface dataset:
Theorem: liftedCIA.GSN_IA'_correct
Proof state before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict (R | ρ) (D | ρ)) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)
Tactic:
simp [←restrict_correct]
Proof state after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict' R D | ρ) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)
Theorem: liftedCIA.GSN_IA'_correct
Proof state before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict' R D | ρ) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)
Tactic:
simp [Delta_Variational, indexDelta, index_union, ←sliceSys_correct]
Proof state after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys' S (D.delete ∪ D.modify) | ρ) ∪
            trace (restrict' R D | ρ) (sliceSys' S' (D.add ∪ D.modify) | ρ) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D.delete | ρ))))
      (trace (R | ρ) (D.delete | ρ))
Theorem: liftedCIA.GSN_IA'_correct
Proof state before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys' S (D.delete ∪ D.modify) | ρ) ∪
            trace (restrict' R D | ρ) (sliceSys' S' (D.add ∪ D.modify) | ρ) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D.delete | ρ))))
      (trace (R | ρ) (D.delete | ρ))
Tactic:
simp [←trace_correct]
Proof state after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (((trace' R (sliceSys' S (D.delete ∪ D.modify)) | ρ) ∪
            trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) | ρ) ∪
          sliceGSN_V (A | ρ) (trace' R D.delete | ρ)))
      (trace' R D.delete | ρ)
Theorem: liftedCIA.GSN_IA'_correct
Proof state before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (((trace' R (sliceSys' S (D.delete ∪ D.modify)) | ρ) ∪
            trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) | ρ) ∪
          sliceGSN_V (A | ρ) (trace' R D.delete | ρ)))
      (trace' R D.delete | ρ)
Tactic:
simp [←sliceGSNV_correct, index_union]
Proof state after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        ((trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)) |
          ρ))
      (trace' R D.delete | ρ)
Theorem: liftedCIA.GSN_IA'_correct
Proof state before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        ((trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)) |
          ρ))
      (trace' R D.delete | ρ)
Tactic:
simp [←sliceGSNR_correct, ←createAnnotation_correct]
Proof state after:
no goals
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
⊢ ∀ (a : α), group.inv (group.inv a) = a
Tactic:
intro a
Proof state after:
α : Type u_1
g : group α
a : α
⊢ group.inv (group.inv a) = a
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
⊢ group.inv (group.inv a) = a
Tactic:
have h := (g.mul_left_inv (g.inv a))
Proof state after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ group.inv (group.inv a) = a
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ group.inv (group.inv a) = a
Tactic:
have h2 : g.inv (g.inv a) * (g.inv a) * a = a := by {
  rw[h]
  apply g.one_mul
}
Proof state after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * group.inv a * a = a
⊢ group.inv (group.inv a) = a
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * group.inv a * a = a
⊢ group.inv (group.inv a) = a
Tactic:
rw [g.mul_assoc] at h2
Proof state after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * (group.inv a * a) = a
⊢ group.inv (group.inv a) = a
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * (group.inv a * a) = a
⊢ group.inv (group.inv a) = a
Tactic:
rw [g.mul_left_inv a] at h2
Proof state after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * has_one.one = a
⊢ group.inv (group.inv a) = a
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * has_one.one = a
⊢ group.inv (group.inv a) = a
Tactic:
rw [g.mul_one] at h2
Proof state after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) = a
⊢ group.inv (group.inv a) = a
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) = a
⊢ group.inv (group.inv a) = a
Tactic:
exact h2
Proof state after:
no goals
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ group.inv (group.inv a) * group.inv a * a = a
Tactic:
rw[h]
Proof state after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ has_one.one * a = a
Theorem: inv_invo
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ has_one.one * a = a
Tactic:
apply g.one_mul
Proof state after:
no goals
Theorem: inv_one_eq_one
Proof state before:
α : Type u_1
g : group α
⊢ group.inv has_one.one = has_one.one
Tactic:
have h : (g.inv g.one) * g.one = g.one := g.mul_left_inv g.one
Proof state after:
α : Type u_1
g : group α
h : group.inv has_one.one * has_one.one = has_one.one
⊢ group.inv has_one.one = has_one.one
Theorem: inv_one_eq_one
Proof state before:
α : Type u_1
g : group α
h : group.inv has_one.one * has_one.one = has_one.one
⊢ group.inv has_one.one = has_one.one
Tactic:
have k := g.mul_one (g.inv g.one)
Proof state after:
α : Type u_1
g : group α
h : group.inv has_one.one * has_one.one = has_one.one
k : group.inv has_one.one * has_one.one = group.inv has_one.one
⊢ group.inv has_one.one = has_one.one
Theorem: inv_one_eq_one
Proof state before:
α : Type u_1
g : group α
h : group.inv has_one.one * has_one.one = has_one.one
k : group.inv has_one.one * has_one.one = group.inv has_one.one
⊢ group.inv has_one.one = has_one.one
Tactic:
rw [k] at h
Proof state after:
α : Type u_1
g : group α
h : group.inv has_one.one = has_one.one
k : group.inv has_one.one * has_one.one = group.inv has_one.one
⊢ group.inv has_one.one = has_one.one
Theorem: inv_one_eq_one
Proof state before:
α : Type u_1
g : group α
h : group.inv has_one.one = has_one.one
k : group.inv has_one.one * has_one.one = group.inv has_one.one
⊢ group.inv has_one.one = has_one.one
Tactic:
exact h
Proof state after:
no goals
Theorem: mul_right_inv
Proof state before:
α : Type u_1
g : group α
⊢ ∀ (a : α), a * group.inv a = has_one.one
Tactic:
intro a
Proof state after:
α : Type u_1
g : group α
a : α
⊢ a * group.inv a = has_one.one
Theorem: mul_right_inv
Proof state before:
α : Type u_1
g : group α
a : α
⊢ a * group.inv a = has_one.one
Tactic:
have h := g.mul_left_inv (group.inv a)
Proof state after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one
Theorem: mul_right_inv
Proof state before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one
Tactic:
rw [inv_invo] at h
Proof state after:
α : Type u_1
g : group α
a : α
h : a * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one
Theorem: mul_right_inv
Proof state before:
α : Type u_1
g : group α
a : α
h : a * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one
Tactic:
exact h
Proof state after:
no goals
Theorem: self_is_subgroup
Proof 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
Proof 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
Theorem: self_is_subgroup
Proof 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
Proof 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
Theorem: self_is_subgroup
Proof 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
Proof 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
Theorem: self_is_subgroup
Proof 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
}
Proof state after:
no goals
Theorem: self_is_subgroup
Proof state before:
α : Type u_1
G : group α
⊢ ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
Tactic:
rw [whole_group]
Proof 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 }
Theorem: self_is_subgroup
Proof 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 _ _
Proof 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 }
Theorem: self_is_subgroup
Proof 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]
Proof 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 }
Theorem: self_is_subgroup
Proof 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
Proof state after:
no goals
Theorem: self_is_subgroup
Proof 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]
Proof 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
Theorem: self_is_subgroup
Proof 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
Proof 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
Theorem: self_is_subgroup
Proof 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]
Proof 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
Theorem: self_is_subgroup
Proof 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
Proof state after:
no goals
Theorem: self_is_subgroup
Proof 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 _
Proof 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
Theorem: self_is_subgroup
Proof 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]
Proof 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
Theorem: self_is_subgroup
Proof 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
Proof 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)
Theorem: self_is_subgroup
Proof 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]
Proof 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)
Theorem: self_is_subgroup
Proof 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
Proof state after:
no goals
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
⊢ subgroup G (trivial_subgroup G)
Tactic:
let H := trivial_subgroup G
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)
Theorem: triv_is_subgroup
Proof 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
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)
Theorem: triv_is_subgroup
Proof 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]
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G H
Theorem: triv_is_subgroup
Proof 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
Proof 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
Theorem: triv_is_subgroup
Proof 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]
Proof 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
Theorem: triv_is_subgroup
Proof 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
Proof 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
Theorem: triv_is_subgroup
Proof 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
}
Proof state after:
no goals
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
⊢ H = trivial_subgroup G
Tactic:
simp
Proof state after:
no goals
Theorem: triv_is_subgroup
Proof 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
Proof 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
Theorem: triv_is_subgroup
Proof 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
Proof 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
Theorem: triv_is_subgroup
Proof 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
Proof 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
Theorem: triv_is_subgroup
Proof 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
Proof 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
Theorem: triv_is_subgroup
Proof 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
Proof 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
Theorem: triv_is_subgroup
Proof 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
Proof 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