Theorem: Function.updateITE_comp_right (FOL/FunctionUpdateITE.lean)

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
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

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
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

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]
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

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!
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

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
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

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
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

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]
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)

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
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)

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
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)

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]
State after:
no goals

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
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

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]
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

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
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

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
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

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
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

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
State after:
no goals