internlm/Lean-Github huggingface dataset:
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : group_homomorphism.fn G H has_one.one = group_homomorphism.fn G H x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
rw [←hphi] at hinj
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : φ has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : φ has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
rw [hphi, hom_preserve_one G H hom, ←hphi] at hinj
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
have hl := hinj hker.symm
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ x ∈ trivial_subgroup G
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
rw [←hl]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ has_one.one ∈ trivial_subgroup G
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ has_one.one ∈ trivial_subgroup G
Tactic:
rw [Membership.mem, instMembershipSet]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one (trivial_subgroup G)
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one (trivial_subgroup G)
Tactic:
simp
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ Set.isMember has_one.one
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ Set.isMember has_one.one
Tactic:
have hts : subgroup G (trivial_subgroup G) := triv_is_subgroup
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
hts : subgroup G (trivial_subgroup G)
⊢ Set.isMember has_one.one
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
hts : subgroup G (trivial_subgroup G)
⊢ Set.isMember has_one.one
Tactic:
apply hts.one_mem
Proof state after:
no goals
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ trivial_subgroup G → x ∈ kernel G H hom
Tactic:
intro hone
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x ∈ trivial_subgroup G
⊢ x ∈ kernel G H hom
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x ∈ trivial_subgroup G
⊢ x ∈ kernel G H hom
Tactic:
rw [trivial_subgroup, Membership.mem, instMembershipSet] at hone
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : { mem := fun x s => Set.isMember x }.1 x { isMember := fun x => x = has_one.one }
⊢ x ∈ kernel G H hom
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : { mem := fun x s => Set.isMember x }.1 x { isMember := fun x => x = has_one.one }
⊢ x ∈ kernel G H hom
Tactic:
simp at hone
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ x ∈ kernel G H hom
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ x ∈ kernel G H hom
Tactic:
rw [hone]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ has_one.one ∈ kernel G H hom
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ has_one.one ∈ kernel G H hom
Tactic:
rw [kernel, Membership.mem, instMembershipSet]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun g => group_homomorphism.fn G H g = has_one.one }
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun g => group_homomorphism.fn G H g = has_one.one }
Tactic:
simp
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ group_homomorphism.fn G H has_one.one = has_one.one
Theorem: trivial_kernel_equiv_inj
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ group_homomorphism.fn G H has_one.one = has_one.one
Tactic:
apply hom_preserve_one
Proof state after:
no goals
Theorem: Array.ext_iff
Proof state before:
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ A = B ↔ ∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ A = B → ∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]

case mpr
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ (∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]) → A = B
Theorem: Array.ext_iff
Proof state before:
case mp
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ A = B → ∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]
Tactic:
rintro rfl
Proof state after:
case mp
α : Type u_1
A : Array α
h : A.size = A.size
⊢ ∀ (i : ℕ) (h1 h2 : i < A.size), A[i] = A[i]
Theorem: Array.ext_iff
Proof state before:
case mp
α : Type u_1
A : Array α
h : A.size = A.size
⊢ ∀ (i : ℕ) (h1 h2 : i < A.size), A[i] = A[i]
Tactic:
simp
Proof state after:
no goals
Theorem: Array.ext_iff
Proof state before:
case mpr
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ (∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]) → A = B
Tactic:
apply ext _ _ h
Proof state after:
no goals
Theorem: Array.ext'_iff
Proof state before:
α : Type u_1
A B : Array α
⊢ A = B ↔ A.data = B.data
Tactic:
cases A
Proof state after:
case mk
α : Type u_1
B : Array α
data✝ : List α
⊢ { data := data✝ } = B ↔ { data := data✝ }.data = B.data
Theorem: Array.ext'_iff
Proof state before:
case mk
α : Type u_1
B : Array α
data✝ : List α
⊢ { data := data✝ } = B ↔ { data := data✝ }.data = B.data
Tactic:
cases B
Proof state after:
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
⊢ { data := data✝¹ } = { data := data✝ } ↔ { data := data✝¹ }.data = { data := data✝ }.data
Theorem: Array.ext'_iff
Proof state before:
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
⊢ { data := data✝¹ } = { data := data✝ } ↔ { data := data✝¹ }.data = { data := data✝ }.data
Tactic:
simp
Proof state after:
no goals
Theorem: List.getCons?_eq_none
Proof state before:
α : Type u_1
c : List α
⊢ c.getCons? = none ↔ c = []
Tactic:
cases c <;> simp [getCons?]
Proof state after:
no goals
Theorem: List.getCons?_eq_some
Proof state before:
α : Type u_1
x : α
xs c : List α
⊢ c.getCons? = some (x, xs) ↔ c = x :: xs
Tactic:
cases c <;> simp [getCons?]
Proof state after:
no goals
Theorem: List.getSnoc?_eq_none
Proof state before:
α : Type u_1
c : List α
⊢ c.getSnoc? = none ↔ c = []
Tactic:
induction c <;> simp_all [getSnoc?]
Proof state after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
⊢ ¬(match tail✝.getSnoc? with
      | none => some ([], head✝)
      | some (xs', x') => some (head✝ :: xs', x')) =
      none
Theorem: List.getSnoc?_eq_none
Proof state before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
⊢ ¬(match tail✝.getSnoc? with
      | none => some ([], head✝)
      | some (xs', x') => some (head✝ :: xs', x')) =
      none
Tactic:
intro h
Proof state after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
h :
  (match tail✝.getSnoc? with
    | none => some ([], head✝)
    | some (xs', x') => some (head✝ :: xs', x')) =
    none
⊢ False
Theorem: List.getSnoc?_eq_none
Proof state before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
h :
  (match tail✝.getSnoc? with
    | none => some ([], head✝)
    | some (xs', x') => some (head✝ :: xs', x')) =
    none
⊢ False
Tactic:
split at h <;> simp_all
Proof state after:
no goals
Theorem: List.getSnoc?_eq_some
Proof state before:
α : Type u_1
xs : List α
x : α
c : List α
⊢ c.getSnoc? = some (xs, x) ↔ c = xs ++ [x]
Tactic:
induction c generalizing xs x <;> simp_all [getSnoc?]
Proof state after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {xs : List α} {x : α}, tail✝.getSnoc? = some (xs, x) ↔ tail✝ = xs ++ [x]
xs : List α
x : α
⊢ (match tail✝.getSnoc? with
      | none => some ([], head✝)
      | some (xs', x') => some (head✝ :: xs', x')) =
      some (xs, x) ↔
    head✝ :: tail✝ = xs ++ [x]
Theorem: List.getSnoc?_eq_some
Proof state before:
α : Type u_1
hd : α
tl : List α
ih : ∀ {xs : List α} {x : α}, tl.getSnoc? = some (xs, x) ↔ tl = xs ++ [x]
xs : List α
x : α
⊢ (match tl.getSnoc? with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]
Tactic:
generalize ho : getSnoc? tl = o at ih
Proof state after:
α : Type u_1
hd : α
tl xs : List α
x : α
o : Option (List α × α)
ho : tl.getSnoc? = o
ih : ∀ {xs : List α} {x : α}, o = some (xs, x) ↔ tl = xs ++ [x]
⊢ (match o with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]
Theorem: List.getSnoc?_eq_some
Proof state before:
α : Type u_1
hd : α
tl xs : List α
x : α
o : Option (List α × α)
ho : tl.getSnoc? = o
ih : ∀ {xs : List α} {x : α}, o = some (xs, x) ↔ tl = xs ++ [x]
⊢ (match o with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]
Tactic:
cases o <;> simp_all
Proof state after:
case none
α : Type u_1
hd : α
tl xs : List α
x : α
ho : tl = []
⊢ [] = xs ∧ hd = x ↔ [hd] = xs ++ [x]

case some
α : Type u_1
hd : α
tl xs : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd :: val✝.1 = xs ∧ val✝.2 = x ↔ hd :: tl = xs ++ [x]
Theorem: List.getSnoc?_eq_some
Proof state before:
case none
α : Type u_1
hd : α
tl xs : List α
x : α
ho : tl = []
⊢ [] = xs ∧ hd = x ↔ [hd] = xs ++ [x]
Tactic:
cases xs <;> simp
Proof state after:
no goals
Theorem: List.getSnoc?_eq_some
Proof state before:
case some
α : Type u_1
hd : α
tl xs : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd :: val✝.1 = xs ∧ val✝.2 = x ↔ hd :: tl = xs ++ [x]
Tactic:
cases xs <;> simp_all
Proof state after:
case some.nil
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd = x → ¬tl = []

case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ tl = tail✝ ++ [x]
Theorem: List.getSnoc?_eq_some
Proof state before:
case some.nil
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd = x → ¬tl = []
Tactic:
rintro rfl rfl
Proof state after:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ [] = xs ++ [x]
⊢ False
Theorem: List.getSnoc?_eq_some
Proof state before:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ [] = xs ++ [x]
⊢ False
Tactic:
simp_all
Proof state after:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ False
Theorem: List.getSnoc?_eq_some
Proof state before:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ False
Tactic:
apply ih
Proof state after:
case some.nil.a
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ val✝ = (?some.nil.xs, ?some.nil.x)

case some.nil.xs
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ List α

case some.nil.x
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ α
Theorem: List.getSnoc?_eq_some
Proof state before:
case some.nil.a
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ val✝ = (?some.nil.xs, ?some.nil.x)

case some.nil.xs
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ List α

case some.nil.x
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ α
Tactic:
rfl
Proof state after:
no goals
Theorem: List.getSnoc?_eq_some
Proof state before:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ tl = tail✝ ++ [x]
Tactic:
rw [←ih]
Proof state after:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)
Theorem: List.getSnoc?_eq_some
Proof state before:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)
Tactic:
clear ih
Proof state after:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)
Theorem: List.getSnoc?_eq_some
Proof state before:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)
Tactic:
aesop
Proof state after:
no goals
Theorem: List.get_eq_get
Proof state before:
α : Type u_1
L1 L2 : List α
i : Fin L1.length
j : Fin L2.length
⊢ L1 = L2 → ↑i = ↑j → L1.get i = L2.get j
Tactic:
cases i
Proof state after:
case mk
α : Type u_1
L1 L2 : List α
j : Fin L2.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
⊢ L1 = L2 → ↑⟨val✝, isLt✝⟩ = ↑j → L1.get ⟨val✝, isLt✝⟩ = L2.get j
Theorem: List.get_eq_get
Proof state before:
case mk
α : Type u_1
L1 L2 : List α
j : Fin L2.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
⊢ L1 = L2 → ↑⟨val✝, isLt✝⟩ = ↑j → L1.get ⟨val✝, isLt✝⟩ = L2.get j
Tactic:
cases j
Proof state after:
case mk.mk
α : Type u_1
L1 L2 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L2.length
⊢ L1 = L2 → ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩ → L1.get ⟨val✝¹, isLt✝¹⟩ = L2.get ⟨val✝, isLt✝⟩
Theorem: List.get_eq_get
Proof state before:
case mk.mk
α : Type u_1
L1 L2 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L2.length
⊢ L1 = L2 → ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩ → L1.get ⟨val✝¹, isLt✝¹⟩ = L2.get ⟨val✝, isLt✝⟩
Tactic:
rintro rfl h
Proof state after:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Theorem: List.get_eq_get
Proof state before:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Tactic:
simp at h
Proof state after:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : val✝¹ = val✝
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Theorem: List.get_eq_get
Proof state before:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : val✝¹ = val✝
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Tactic:
cases h
Proof state after:
case mk.mk.refl
α : Type u_1
L1 : List α
val✝ : ℕ
isLt✝¹ isLt✝ : val✝ < L1.length
⊢ L1.get ⟨val✝, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Theorem: List.get_eq_get
Proof state before:
case mk.mk.refl
α : Type u_1
L1 : List α
val✝ : ℕ
isLt✝¹ isLt✝ : val✝ < L1.length
⊢ L1.get ⟨val✝, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: List.length_nonempty
Proof state before:
α : Type u_1
lst : Nonempty α
⊢ lst.toList.length > 0
Tactic:
have := lst.property
Proof state after:
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
⊢ lst.toList.length > 0
Theorem: List.length_nonempty
Proof state before:
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
⊢ lst.toList.length > 0
Tactic:
cases h : lst.val with
| nil        => contradiction
| cons hd tl => simp [Nonempty.toList, h]
Proof state after:
no goals
Theorem: List.length_nonempty
Proof state before:
case nil
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
h : ↑lst = []
⊢ lst.toList.length > 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.length_nonempty
Proof state before:
case cons
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
hd : α
tl : List α
h : ↑lst = hd :: tl
⊢ lst.toList.length > 0
Tactic:
simp [Nonempty.toList, h]
Proof state after:
no goals
Theorem: LeanColls.Seq.size_set
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
⊢ size (set cont i x) = size cont
Tactic:
simp [size_def, List.instSeqList]
Proof state after:
no goals
Theorem: LeanColls.Seq.size_update
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
⊢ size (update cont i f) = size cont
Tactic:
simp [size_def, List.instSeqList]
Proof state after:
no goals