α : Type u_1
β : Type ?u.15921
L L' : List (List α)
⊢ join L = join L' ∧ map length L = map length L' → L = L'
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
⊢ L = L' ↔ join L = join L' ∧ map length L = map length L'
refine' ⟨fun H => by simp [H], _⟩
case intro
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ L = L'
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
⊢ join L = join L' ∧ map length L = map length L' → L = L'
rintro ⟨join_eq, length_eq⟩
case intro.hl
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ length L = length L'

case intro.h
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ ∀ (n : ℕ) (h₁ : n < length L) (h₂ : n < length L'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
case intro
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ L = L'
apply ext_get
no goals
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
H : L = L'
⊢ join L = join L' ∧ map length L = map length L'
simp [H]
case intro.hl
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
this : length (map length L) = length (map length L')
⊢ length L = length L'
case intro.hl
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ length L = length L'
have : length (map length L) = length (map length L') := by rw [length_eq]
no goals
case intro.hl
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
this : length (map length L) = length (map length L')
⊢ length L = length L'
simpa using this
no goals
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ length (map length L) = length (map length L')
rw [length_eq]
case intro.h
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
n : ℕ
h₁ : n < length L
h₂ : n < length L'
⊢ get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
case intro.h
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ ∀ (n : ℕ) (h₁ : n < length L) (h₂ : n < length L'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
intro n h₁ h₂
no goals
case intro.h
α : Type u_1
β : Type ?u.15921
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
n : ℕ
h₁ : n < length L
h₂ : n < length L'
⊢ get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
rw [← drop_take_succ_join_eq_get, ← drop_take_succ_join_eq_get, join_eq, length_eq]