internlm/Lean-Github huggingface dataset:
Theorem: Fin.snoc_five_apply
Proof state before:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
⊢ snoc (snoc (snoc (snoc (snoc l x) y) z) w) u { val := n, isLt := (_ : n < n + (4 + 1)) } = x
Tactic:
simp only [snoc]
Proof state after:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Theorem: Fin.snoc_five_apply
Proof state before:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Tactic:
have : n < n + 1 + 1 := Nat.lt_add _
Proof state after:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
this : n < n + 1 + 1
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Theorem: Fin.snoc_five_apply
Proof state before:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
this : n < n + 1 + 1
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Tactic:
have : n < n + 1 + 1 + 1 := Nat.lt_add _
Proof state after:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
this✝ : n < n + 1 + 1
this : n < n + 1 + 1 + 1
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Theorem: Fin.snoc_five_apply
Proof state before:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
this✝ : n < n + 1 + 1
this : n < n + 1 + 1 + 1
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Tactic:
have : n < n + 1 + 1 + 1 + 1 := Nat.lt_add _
Proof state after:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
this✝¹ : n < n + 1 + 1
this✝ : n < n + 1 + 1 + 1
this : n < n + 1 + 1 + 1 + 1
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Theorem: Fin.snoc_five_apply
Proof state before:
V : Type ?u.14957
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z w u : α
this✝¹ : n < n + 1 + 1
this✝ : n < n + 1 + 1 + 1
this : n < n + 1 + 1 + 1 + 1
⊢ (if h : n < n + 1 + 1 + 1 + 1 then
      if h_1 : n < n + 1 + 1 + 1 then
        if h_2 : n < n + 1 + 1 then
          if h_3 : n < n + 1 then
            if h_4 : n < n then
              l
                { val := n,
                  isLt :=
                    (_ :
                      { val := n,
                            isLt :=
                              (_ :
                                { val := n,
                                      isLt :=
                                        (_ :
                                          { val := n,
                                                isLt :=
                                                  (_ :
                                                    { val := n,
                                                          isLt :=
                                                            (_ :
                                                              { val := n, isLt := (_ : n < n + (4 + 1)) }.val <
                                                                n + 1 + 1 + 1 + 1) }.val <
                                                      n + 1 + 1 + 1) }.val <
                                            n + 1 + 1) }.val <
                                  n + 1) }.val <
                        n) }
            else x
          else y
        else z
      else w
    else u) =
    x
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_snoc_termSucc
Proof state before:
V : Type u_2
inst✝ : SetTheory V
α✝ : Type u_1
v : α✝ → V
n✝ : Nat
l : Fin n✝ → V
y : V
x : α✝ ⊕ Fin n✝
⊢ interpretTerm V v (Fin.snoc l y) (termSucc x) = interpretTerm V v l x
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_termSum_elim
Proof state before:
V : Type u_3
inst✝ : SetTheory V
α : Type u_1
n : Nat
vα : α → V
β✝ : Type u_2
vβ : β✝ → V
l : Fin n → V
p : α ⊕ Fin n
⊢ interpretTerm V (Sum.elim vα vβ) l (termSum p) = interpretTerm V vα l p
Tactic:
cases p <;> rfl
Proof state after:
no goals
Theorem: SetTheory.interpret_sum_elim
Proof state before:
V : Type u_1
inst✝ : SetTheory V
β α✝ : Type
a✝ : Nat
p : BoundedFormula α✝ a✝
vα : α✝ → V
vβ : β → V
l : Fin a✝ → V
⊢ Interpret V (sum β p) (Sum.elim vα vβ) l ↔ Interpret V p vα l
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_or
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.or p q) v l ↔ Interpret V p v l ∨ Interpret V q v l
Tactic:
rw [or_iff]
Proof state after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.or p q) v l ↔ ¬Interpret V p v l → Interpret V q v l
Theorem: SetTheory.interpret_or
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.or p q) v l ↔ ¬Interpret V p v l → Interpret V q v l
Tactic:
rfl
Proof state after:
no goals
Theorem: SetTheory.interpret_and
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and p q) v l ↔ Interpret V p v l ∧ Interpret V q v l
Tactic:
rw [and_iff]
Proof state after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and p q) v l ↔ ¬(Interpret V p v l → ¬Interpret V q v l)
Theorem: SetTheory.interpret_and
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and p q) v l ↔ ¬(Interpret V p v l → ¬Interpret V q v l)
Tactic:
rfl
Proof state after:
no goals
Theorem: SetTheory.interpret_iff
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.iff p q) v l ↔ (Interpret V p v l ↔ Interpret V q v l)
Tactic:
unfold BoundedFormula.iff
Proof state after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and (BoundedFormula.imp p q) (BoundedFormula.imp q p)) v l ↔
    (Interpret V p v l ↔ Interpret V q v l)
Theorem: SetTheory.interpret_iff
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and (BoundedFormula.imp p q) (BoundedFormula.imp q p)) v l ↔
    (Interpret V p v l ↔ Interpret V q v l)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_subset
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
n✝ : Nat
x y : α✝ ⊕ Fin n✝
v : α✝ → V
l : Fin n✝ → V
⊢ Interpret V (BoundedFormula.subset x y) v l ↔ interpretTerm V v l x ⊆ interpretTerm V v l y
Tactic:
unfold BoundedFormula.subset
Proof state after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
n✝ : Nat
x y : α✝ ⊕ Fin n✝
v : α✝ → V
l : Fin n✝ → V
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc x))
          (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc y))))
      v l ↔
    interpretTerm V v l x ⊆ interpretTerm V v l y
Theorem: SetTheory.interpret_subset
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
n✝ : Nat
x y : α✝ ⊕ Fin n✝
v : α✝ → V
l : Fin n✝ → V
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc x))
          (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc y))))
      v l ↔
    interpretTerm V v l x ⊆ interpretTerm V v l y
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_exists
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p : BoundedFormula α✝ (a✝ + 1)
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.exists p) v l ↔ ∃ x, Interpret V p v (Fin.snoc l x)
Tactic:
unfold BoundedFormula.exists
Proof state after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p : BoundedFormula α✝ (a✝ + 1)
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.not (BoundedFormula.all (BoundedFormula.not p))) v l ↔ ∃ x, Interpret V p v (Fin.snoc l x)
Theorem: SetTheory.interpret_exists
Proof state before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p : BoundedFormula α✝ (a✝ + 1)
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.not (BoundedFormula.all (BoundedFormula.not p))) v l ↔ ∃ x, Interpret V p v (Fin.snoc l x)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.ext_iff
Proof state before:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
inst✝ : Extensionality V
x y : V
⊢ x = y → ∀ (z : V), z ∈ x ↔ z ∈ y
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_singleton_iff
Proof state before:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
y x : V
inst✝ : Pairing V
⊢ y ∈ {x} ↔ y = x
Tactic:
show y ∈ pair x x ↔ y = x
Proof state after:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
y x : V
inst✝ : Pairing V
⊢ y ∈ pair x x ↔ y = x
Theorem: SetTheory.mem_singleton_iff
Proof state before:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
y x : V
inst✝ : Pairing V
⊢ y ∈ pair x x ↔ y = x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.mem_union_iff
Proof state before:
V : Type u_1
inst✝³ inst✝² : SetTheory V
inst✝¹ : Union V
inst✝ : Pairing V
x y z : V
⊢ z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y
Tactic:
show z ∈ ⋃ pair x y ↔ z ∈ x ∨ z ∈ y
Proof state after:
V : Type u_1
inst✝³ inst✝² : SetTheory V
inst✝¹ : Union V
inst✝ : Pairing V
x y z : V
⊢ z ∈ ⋃ pair x y ↔ z ∈ x ∨ z ∈ y
Theorem: SetTheory.mem_union_iff
Proof state before:
V : Type u_1
inst✝³ inst✝² : SetTheory V
inst✝¹ : Union V
inst✝ : Pairing V
x y z : V
⊢ z ∈ ⋃ pair x y ↔ z ∈ x ∨ z ∈ y
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.mop_injective'
Proof state before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q ↔ p = q
Tactic:
constructor
Proof state after:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q → p = q

case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Theorem: LO.UnaryModalOperator.mop_injective'
Proof state before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q → p = q

case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Tactic:
. intro h; exact mop_injective h;
Proof state after:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Theorem: LO.UnaryModalOperator.mop_injective'
Proof state before:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Tactic:
. simp_all;
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.mop_injective'
Proof state before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q → p = q
Tactic:
intro h
Proof state after:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
h : mop i p = mop i q
⊢ p = q
Theorem: LO.UnaryModalOperator.mop_injective'
Proof state before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
h : mop i p = mop i q
⊢ p = q
Tactic:
exact mop_injective h
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.mop_injective'
Proof state before:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.multimop_succ
Proof state before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ (mop i)^[n + 1] p = mop i ((mop i)^[n] p)
Tactic:
apply iterate_succ_apply'
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.multimop_injective
Proof state before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ Injective (mop i)^[n]
Tactic:
apply Function.Injective.iterate (by simp)
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.multimop_injective
Proof state before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ Injective (mop i)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.multimop_injective'
Proof state before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ (mop i)^[n] p = (mop i)^[n] q ↔ p = q
Tactic:
constructor
Proof state after:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ (mop i)^[n] p = (mop i)^[n] q → p = q

case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ p = q → (mop i)^[n] p = (mop i)^[n] q
Theorem: LO.UnaryModalOperator.multimop_injective'
Proof state before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ (mop i)^[n] p = (mop i)^[n] q → p = q

case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ p = q → (mop i)^[n] p = (mop i)^[n] q
Tactic:
. intro h; exact multimop_injective h;
Proof state after:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ p = q → (mop i)^[n] p = (mop i)^[n] q
Theorem: LO.UnaryModalOperator.multimop_injective'
Proof state before:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ p = q → (mop i)^[n] p = (mop i)^[n] q
Tactic:
. simp_all;
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.multimop_injective'
Proof state before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ (mop i)^[n] p = (mop i)^[n] q → p = q
Tactic:
intro h
Proof state after:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
h : (mop i)^[n] p = (mop i)^[n] q
⊢ p = q
Theorem: LO.UnaryModalOperator.multimop_injective'
Proof state before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
h : (mop i)^[n] p = (mop i)^[n] q
⊢ p = q
Tactic:
exact multimop_injective h
Proof state after:
no goals
Theorem: LO.UnaryModalOperator.multimop_injective'
Proof state before:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ p = q → (mop i)^[n] p = (mop i)^[n] q
Tactic:
simp_all
Proof state after:
no goals
Theorem: Set.mop_iff_multimop_one
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Set F
⊢ Set.mop i s = Set.multimop i 1 s
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.premop_iff_premultimop_one
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Set F
⊢ Set.premop i s = Set.premultimop i 1 s
Tactic:
rfl
Proof state after:
no goals