Theorem: Partial.map_inj (ReactorModel/Extensions.lean)

State before:
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
⊢ f₁ = f₂
Tactic:
funext a
State after:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
a : α
⊢ f₁ a = f₂ a

State before:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
a : α
⊢ f₁ a = f₂ a
Tactic:
replace h : f₁.map g a = f₂.map g a := by simp [h]
State after:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
a : α
h : map g f₁ a = map g f₂ a
⊢ f₁ a = f₂ a

State before:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
a : α
h : map g f₁ a = map g f₂ a
⊢ f₁ a = f₂ a
Tactic:
exact Option.map_injective hi h
State after:
no goals

State before:
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
a : α
⊢ map g f₁ a = map g f₂ a
Tactic:
simp [h]
State after:
no goals