ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
⊢ map f l = map g l → ∀ (x : α), x ∈ l → f x = g x
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
⊢ map f l = map g l ↔ ∀ (x : α), x ∈ l → f x = g x
refine' ⟨_, map_congr⟩
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
x : α
hx : x ∈ l
⊢ f x = g x
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
⊢ map f l = map g l → ∀ (x : α), x ∈ l → f x = g x
intro h x hx
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
x : α
hx : ∃ n, get l n = x
⊢ f x = g x
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
x : α
hx : x ∈ l
⊢ f x = g x
rw [mem_iff_get] at hx
case intro.refl
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
n : Fin (length l)
⊢ f (get l n) = g (get l n)
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
x : α
hx : ∃ n, get l n = x
⊢ f x = g x
rcases hx with ⟨n, hn, rfl⟩
case intro.refl
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
n : Fin (length l)
⊢ get (map f l) { val := ↑n, isLt := (_ : ↑n < length (map f l)) } =
    get (map g l) { val := ↑n, isLt := (_ : ↑n < length (map g l)) }
case intro.refl
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
n : Fin (length l)
⊢ f (get l n) = g (get l n)
rw [get_map_rev f, get_map_rev g]
no goals
case intro.refl
ι : Type ?u.130847
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β
l : List α
h : map f l = map g l
n : Fin (length l)
⊢ get (map f l) { val := ↑n, isLt := (_ : ↑n < length (map f l)) } =
    get (map g l) { val := ↑n, isLt := (_ : ↑n < length (map g l)) }
congr!