Theorem: Option.map_inj (SInfinity/Util.lean)

State before:
A B : Type
f : A → B
inj : Injective f
x y : Option A
⊢ Option.map f x = Option.map f y → x = y
Tactic:
intros p
State after:
A B : Type
f : A → B
inj : Injective f
x y : Option A
p : Option.map f x = Option.map f y
⊢ x = y

State before:
A B : Type
f : A → B
inj : Injective f
x y : Option A
p : Option.map f x = Option.map f y
⊢ x = y
Tactic:
induction x <;> induction y <;> try trivial
State after:
case some.some
A B : Type
f : A → B
inj : Injective f
val✝¹ val✝ : A
p : Option.map f (some val✝¹) = Option.map f (some val✝)
⊢ some val✝¹ = some val✝

State before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ some v = some v'
Tactic:
case some.some v v' =>
  have obvs : ∀ a, Option.map f (some a) = some (f a) := by intros a; rfl
  rw [obvs v, obvs v'] at p
  rw [Option.some_inj] at p
  apply congrArg; apply inj; assumption
State after:
no goals

State before:
case some.none
A B : Type
f : A → B
inj : Injective f
val✝ : A
p : Option.map f (some val✝) = Option.map f none
⊢ some val✝ = none
Tactic:
trivial
State after:
no goals

State before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ some v = some v'
Tactic:
have obvs : ∀ a, Option.map f (some a) = some (f a) := by intros a; rfl
State after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'

State before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Tactic:
rw [obvs v, obvs v'] at p
State after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : some (f v) = some (f v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'

State before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : some (f v) = some (f v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Tactic:
rw [Option.some_inj] at p
State after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'

State before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Tactic:
apply congrArg
State after:
case h
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ v = v'

State before:
case h
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ v = v'
Tactic:
apply inj
State after:
case h.a
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ f v = f v'

State before:
case h.a
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ f v = f v'
Tactic:
assumption
State after:
no goals

State before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ ∀ (a : A), Option.map f (some a) = some (f a)
Tactic:
intros a
State after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
a : A
⊢ Option.map f (some a) = some (f a)

State before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
a : A
⊢ Option.map f (some a) = some (f a)
Tactic:
rfl
State after:
no goals