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

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

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

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

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

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

State before:
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
Tactic:
constructor
State after:
case h.h₁.a.mp
α β γ : 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

case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ x = a → f x = f a

State before:
case h.h₁.a.mp
α β γ : 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
Tactic:
apply h1
State after:
no goals

State before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ x = a → f x = f a
Tactic:
intro a1
State after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
a1 : x = a
⊢ f x = f a

State before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
a1 : x = a
⊢ f x = f a
Tactic:
subst a1
State after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f x

State before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f x
Tactic:
rfl
State after:
no goals