internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = a.args.length
Tactic:
trans List.length xs
Proof state after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = xs.length

D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = a.args.length
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = xs.length
Tactic:
simp only [eq_comm]
Proof state after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = E1_hd.args.length
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = E1_hd.args.length
Tactic:
exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = a.args.length
Tactic:
exact h2_1_right_right
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1 : ¬(X = E1_hd.name ∧ xs.length = E1_hd.args.length)
⊢ Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
exact E1_ih h3_right
Proof state after:
no goals
Theorem: Function.left_id_left_inverse
Proof state before:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
⊢ LeftInverse g f
Tactic:
simp only [Function.LeftInverse]
Proof state after:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
⊢ ∀ (x : α), g (f x) = x
Theorem: Function.left_id_left_inverse
Proof state before:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
⊢ ∀ (x : α), g (f x) = x
Tactic:
intro x
Proof state after:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
x : α
⊢ g (f x) = x
Theorem: Function.left_id_left_inverse
Proof state before:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
x : α
⊢ g (f x) = x
Tactic:
exact congrFun h1 x
Proof state after:
no goals
Theorem: Function.right_id_right_inverse
Proof state before:
α β : Type
f : α → β
g : β → α
h1 : f ∘ g = id
⊢ RightInverse g f
Tactic:
simp only [Function.RightInverse]
Proof state after:
α β : Type
f : α → β
g : β → α
h1 : f ∘ g = id
⊢ LeftInverse f g
Theorem: Function.right_id_right_inverse
Proof state before:
α β : Type
f : α → β
g : β → α
h1 : f ∘ g = id
⊢ LeftInverse f g
Tactic:
exact Function.left_id_left_inverse g f h1
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
⊢ updateITE f a b = Function.updateITE' f a b
Tactic:
funext x
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ updateITE f a b x = Function.updateITE' f a b x
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ updateITE f a b x = Function.updateITE' f a b x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ (if x = a then b else f x) = Function.updateITE' f a b x
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ (if x = a then b else f x) = Function.updateITE' f a b x
Tactic:
simp only [Function.updateITE']
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ (if x = a then b else f x) = if a = x then b else f x
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ (if x = a then b else f x) = if a = x then b else f x
Tactic:
split_ifs
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : x = a
h✝ : a = x
⊢ b = b

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : x = a
h✝ : ¬a = x
⊢ b = f x

case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : ¬x = a
h✝ : a = x
⊢ f x = b

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : ¬x = a
h✝ : ¬a = x
⊢ f x = f x
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : a = x
⊢ b = b
Tactic:
case _ c1 c2 =>
  rfl
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : ¬a = x
⊢ b = f x
Tactic:
case _ c1 c2 =>
  subst c1
  contradiction
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : a = x
⊢ f x = b
Tactic:
case _ c1 c2 =>
  subst c2
  contradiction
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : ¬a = x
⊢ f x = f x
Tactic:
case _ c1 c2 =>
  rfl
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : a = x
⊢ b = b
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : ¬a = x
⊢ b = f x
Tactic:
subst c1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
b : β
x : α
c2 : ¬x = x
⊢ b = f x
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
b : β
x : α
c2 : ¬x = x
⊢ b = f x
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : a = x
⊢ f x = b
Tactic:
subst c2
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
c1 : ¬a = a
⊢ f a = b
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
c1 : ¬a = a
⊢ f a = b
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateITE_eq_Function.updateITE'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : ¬a = x
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_comp_left
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
⊢ f ∘ updateITE g a b = updateITE (f ∘ g) a (f b)
Tactic:
funext x
Proof state after:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ (f ∘ updateITE g a b) x = updateITE (f ∘ g) a (f b) x
Theorem: Function.updateITE_comp_left
Proof state before:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ (f ∘ updateITE g a b) x = updateITE (f ∘ g) a (f b) x
Tactic:
simp
Proof state after:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ f (updateITE g a b x) = updateITE (f ∘ g) a (f b) x
Theorem: Function.updateITE_comp_left
Proof state before:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ f (updateITE g a b x) = updateITE (f ∘ g) a (f b) x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ f (if x = a then b else g x) = if x = a then f b else (f ∘ g) x
Theorem: Function.updateITE_comp_left
Proof state before:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ f (if x = a then b else g x) = if x = a then f b else (f ∘ g) x
Tactic:
split_ifs
Proof state after:
case pos
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
h✝ : x = a
⊢ f b = f b

case neg
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
h✝ : ¬x = a
⊢ f (g x) = (f ∘ g) x
Theorem: Function.updateITE_comp_left
Proof state before:
case pos
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
h✝ : x = a
⊢ f b = f b
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_comp_left
Proof state before:
case neg
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
h✝ : ¬x = a
⊢ f (g x) = (f ∘ g) x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_comp_right
Proof state before:
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
⊢ updateITE g a b ∘ f = updateITE (g ∘ f) (finv a) b
Tactic:
funext x
Proof state after:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ (updateITE g a b ∘ f) x = updateITE (g ∘ f) (finv a) b x
Theorem: Function.updateITE_comp_right
Proof state before:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ (updateITE g a b ∘ f) x = updateITE (g ∘ f) (finv a) b x
Tactic:
simp
Proof state after:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ updateITE g a b (f x) = updateITE (g ∘ f) (finv a) b x
Theorem: Function.updateITE_comp_right
Proof state before:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ updateITE g a b (f x) = updateITE (g ∘ f) (finv a) b x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ (if f x = a then b else g (f x)) = if x = finv a then b else (g ∘ f) x
Theorem: Function.updateITE_comp_right
Proof state before:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ (if f x = a then b else g (f x)) = if x = finv a then b else (g ∘ f) x
Tactic:
congr!
Proof state after:
case h.h₁.a
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ f x = a ↔ x = finv a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ f x = a ↔ x = finv a
Tactic:
constructor
Proof state after:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ f x = a → x = finv a

case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ x = finv a → f x = a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ f x = a → x = finv a
Tactic:
intro a1
Proof state after:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
⊢ x = finv a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
⊢ x = finv a
Tactic:
simp only [← a1]
Proof state after:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
⊢ x = finv (f x)
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
⊢ x = finv (f x)
Tactic:
obtain s1 := Function.left_id_left_inverse f finv h1
Proof state after:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
s1 : LeftInverse finv f
⊢ x = finv (f x)
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
s1 : LeftInverse finv f
⊢ x = finv (f x)
Tactic:
simp only [Function.LeftInverse] at s1
Proof state after:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
s1 : ∀ (x : α), finv (f x) = x
⊢ x = finv (f x)
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : f x = a
s1 : ∀ (x : α), finv (f x) = x
⊢ x = finv (f x)
Tactic:
simp only [s1 x]
Proof state after:
no goals
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ x = finv a → f x = a
Tactic:
intro a1
Proof state after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
⊢ f x = a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
⊢ f x = a
Tactic:
simp only [a1]
Proof state after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
⊢ f (finv a) = a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
⊢ f (finv a) = a
Tactic:
obtain s1 := Function.right_id_right_inverse f finv h2
Proof state after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
s1 : RightInverse finv f
⊢ f (finv a) = a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
s1 : RightInverse finv f
⊢ f (finv a) = a
Tactic:
simp only [Function.RightInverse] at s1
Proof state after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
s1 : LeftInverse f finv
⊢ f (finv a) = a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
s1 : LeftInverse f finv
⊢ f (finv a) = a
Tactic:
simp only [Function.LeftInverse] at s1
Proof state after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
s1 : ∀ (x : β), f (finv x) = x
⊢ f (finv a) = a
Theorem: Function.updateITE_comp_right
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
s1 : ∀ (x : β), f (finv x) = x
⊢ f (finv a) = a
Tactic:
exact s1 a
Proof state after:
no goals
Theorem: Function.updateITE_comp_right_injective
Proof state before:
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : Injective f
⊢ updateITE g (f a) b ∘ f = updateITE (g ∘ f) a b
Tactic:
simp only [Function.Injective] at h1
Proof state after:
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
⊢ updateITE g (f a) b ∘ f = updateITE (g ∘ f) a b
Theorem: Function.updateITE_comp_right_injective
Proof state before:
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
⊢ updateITE g (f a) b ∘ f = updateITE (g ∘ f) a b
Tactic:
funext x
Proof state after:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ (updateITE g (f a) b ∘ f) x = updateITE (g ∘ f) a b x
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ (updateITE g (f a) b ∘ f) x = updateITE (g ∘ f) a b x
Tactic:
simp
Proof state after:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ updateITE g (f a) b (f x) = updateITE (g ∘ f) a b x
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ updateITE g (f a) b (f x) = updateITE (g ∘ f) a b x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ (if f x = f a then b else g (f x)) = if x = a then b else (g ∘ f) x
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ (if f x = f a then b else g (f x)) = if x = a then b else (g ∘ f) x
Tactic:
congr!
Proof state after:
case h.h₁.a
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f a ↔ x = a