[GOAL]
lo hi a : ℕ
h : Nat.succ lo ≤ a ∧ a ≤ hi
⊢ Nat.succ (Nat.pred a) ≤ hi
[PROOFSTEP]
rw [Nat.succ_pred_eq_of_pos]
[GOAL]
lo hi a : ℕ
h : Nat.succ lo ≤ a ∧ a ≤ hi
⊢ a ≤ hi
lo hi a : ℕ h : Nat.succ lo ≤ a ∧ a ≤ hi ⊢ 0 < a
[PROOFSTEP]
exact h.right
[GOAL]
lo hi a : ℕ
h : Nat.succ lo ≤ a ∧ a ≤ hi
⊢ 0 < a
[PROOFSTEP]
exact lt_of_le_of_lt (Nat.zero_le lo) h.left


[GOAL]
n : ℕ
h : 0 < n
m : ℕ := n / 2
⊢ m < n
[PROOFSTEP]
apply Nat.div_lt_self h
[GOAL]
n : ℕ
h : 0 < n
m : ℕ := n / 2
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ Fin.ofNat 0 ≤ Fin.ofNat __do_lift✝
[PROOFSTEP]
simp [Fin.ofNat, LE.le]
[GOAL]
n : ℕ
⊢ 0 ≤ __do_lift✝ % (n + 1)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
⊢ 0 < List.length (String.toList " 0123abcABC:,;`\\/")
[PROOFSTEP]
decide


[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
tf : TotalFunction α β
⊢ ∀ (a : α), a ∈ zeroDefaultSupp tf ↔ apply (zeroDefault tf) a ≠ 0
[PROOFSTEP]
intro a
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
tf : TotalFunction α β
a : α
⊢ a ∈ zeroDefaultSupp tf ↔ apply (zeroDefault tf) a ≠ 0
[PROOFSTEP]
rcases tf with ⟨A, y⟩
[GOAL]
case withDefault
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ a ∈ zeroDefaultSupp (withDefault A y) ↔ apply (zeroDefault (withDefault A y)) a ≠ 0
[PROOFSTEP]
simp only [apply, zeroDefaultSupp, List.mem_map, List.mem_filter, exists_and_right, List.mem_toFinset, exists_eq_right,
  Sigma.exists, Ne.def, zeroDefault]
[GOAL]
case withDefault
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, { fst := a, snd := x } ∈ List.dedupKeys A ∧ (decide ¬x = 0) = true) ↔ ¬Option.getD (List.dlookup a A) 0 = 0
[PROOFSTEP]
constructor
[GOAL]
case withDefault.mp
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, { fst := a, snd := x } ∈ List.dedupKeys A ∧ (decide ¬x = 0) = true) → ¬Option.getD (List.dlookup a A) 0 = 0
[PROOFSTEP]
rintro ⟨od, hval, hod⟩
[GOAL]
case withDefault.mp.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : { fst := a, snd := od } ∈ List.dedupKeys A
hod : (decide ¬od = 0) = true
⊢ ¬Option.getD (List.dlookup a A) 0 = 0
[PROOFSTEP]
have := List.mem_dlookup (List.nodupKeys_dedupKeys A) hval
[GOAL]
case withDefault.mp.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : { fst := a, snd := od } ∈ List.dedupKeys A
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a (List.dedupKeys A)
⊢ ¬Option.getD (List.dlookup a A) 0 = 0
[PROOFSTEP]
rw [(_ : List.dlookup a A = od)]
[GOAL]
case withDefault.mp.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : { fst := a, snd := od } ∈ List.dedupKeys A
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a (List.dedupKeys A)
⊢ ¬Option.getD (some od) 0 = 0
[PROOFSTEP]
simpa using hod
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : { fst := a, snd := od } ∈ List.dedupKeys A
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a (List.dedupKeys A)
⊢ List.dlookup a A = some od
[PROOFSTEP]
simpa [List.dlookup_dedupKeys, WithTop.some_eq_coe]
[GOAL]
case withDefault.mpr
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ ¬Option.getD (List.dlookup a A) 0 = 0 → ∃ x, { fst := a, snd := x } ∈ List.dedupKeys A ∧ (decide ¬x = 0) = true
[PROOFSTEP]
intro h
[GOAL]
case withDefault.mpr
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬Option.getD (List.dlookup a A) 0 = 0
⊢ ∃ x, { fst := a, snd := x } ∈ List.dedupKeys A ∧ (decide ¬x = 0) = true
[PROOFSTEP]
use(A.dlookup a).getD (0 : β)
[GOAL]
case h
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬Option.getD (List.dlookup a A) 0 = 0
⊢ { fst := a, snd := Option.getD (List.dlookup a A) 0 } ∈ List.dedupKeys A ∧
    (decide ¬Option.getD (List.dlookup a A) 0 = 0) = true
[PROOFSTEP]
rw [← List.dlookup_dedupKeys] at h ⊢
[GOAL]
case h
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬Option.getD (List.dlookup a (List.dedupKeys A)) 0 = 0
⊢ { fst := a, snd := Option.getD (List.dlookup a (List.dedupKeys A)) 0 } ∈ List.dedupKeys A ∧
    (decide ¬Option.getD (List.dlookup a (List.dedupKeys A)) 0 = 0) = true
[PROOFSTEP]
simp only [h, ← List.mem_dlookup_iff A.nodupKeys_dedupKeys, and_true_iff, not_false_iff, Option.mem_def]
[GOAL]
case h
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬Option.getD (List.dlookup a (List.dedupKeys A)) 0 = 0
⊢ List.dlookup a (List.dedupKeys A) = some (Option.getD (List.dlookup a (List.dedupKeys A)) 0)
[PROOFSTEP]
cases haA : List.dlookup a A.dedupKeys
[GOAL]
case h.none
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬Option.getD (List.dlookup a (List.dedupKeys A)) 0 = 0
haA : List.dlookup a (List.dedupKeys A) = none
⊢ none = some (Option.getD none 0)
[PROOFSTEP]
simp [haA] at h
[GOAL]
case h.some
α : Type u
β : Type v
γ : Sort w
inst✝² : Zero β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬Option.getD (List.dlookup a (List.dedupKeys A)) 0 = 0
val✝ : β
haA : List.dlookup a (List.dedupKeys A) = some val✝
⊢ some val✝ = some (Option.getD (some val✝) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ applyId ((y, z) :: xs) x = if y = x then z else applyId xs x
[PROOFSTEP]
simp only [List.applyId, List.dlookup, eq_rec_constant, Prod.toSigma, List.map]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ Option.getD (if h : y = x then some z else List.dlookup x (List.map (fun p => { fst := p.fst, snd := p.snd }) xs)) x =
    if y = x then z else Option.getD (List.dlookup x (List.map (fun p => { fst := p.fst, snd := p.snd }) xs)) x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : y = x
⊢ Option.getD (some z) x = z
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : ¬y = x
⊢ Option.getD (List.dlookup x (List.map (fun p => { fst := p.fst, snd := p.snd }) xs)) x =
    Option.getD (List.dlookup x (List.map (fun p => { fst := p.fst, snd := p.snd }) xs)) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : List.length xs = List.length ys
x y : α
i : ℕ
h₂ : List.get? xs i = some x
⊢ applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y
[PROOFSTEP]
induction xs generalizing ys i
[GOAL]
case nil
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y : α
ys : List α
h₀ : List.Nodup []
h₁ : List.length [] = List.length ys
i : ℕ
h₂ : List.get? [] i = some x
⊢ applyId (List.zip [] ys) x = y ↔ List.get? ys i = some y
case cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {ys : List α},
    List.Nodup tail✝ →
      List.length tail✝ = List.length ys →
        ∀ (i : ℕ), List.get? tail✝ i = some x → (applyId (List.zip tail✝ ys) x = y ↔ List.get? ys i = some y)
ys : List α
h₀ : List.Nodup (head✝ :: tail✝)
h₁ : List.length (head✝ :: tail✝) = List.length ys
i : ℕ
h₂ : List.get? (head✝ :: tail✝) i = some x
⊢ applyId (List.zip (head✝ :: tail✝) ys) x = y ↔ List.get? ys i = some y
[PROOFSTEP]
case nil => cases h₂
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y : α
ys : List α
h₀ : List.Nodup []
h₁ : List.length [] = List.length ys
i : ℕ
h₂ : List.get? [] i = some x
⊢ applyId (List.zip [] ys) x = y ↔ List.get? ys i = some y
[PROOFSTEP]
case nil => cases h₂
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y : α
ys : List α
h₀ : List.Nodup []
h₁ : List.length [] = List.length ys
i : ℕ
h₂ : List.get? [] i = some x
⊢ applyId (List.zip [] ys) x = y ↔ List.get? ys i = some y
[PROOFSTEP]
cases h₂
[GOAL]
case cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {ys : List α},
    List.Nodup tail✝ →
      List.length tail✝ = List.length ys →
        ∀ (i : ℕ), List.get? tail✝ i = some x → (applyId (List.zip tail✝ ys) x = y ↔ List.get? ys i = some y)
ys : List α
h₀ : List.Nodup (head✝ :: tail✝)
h₁ : List.length (head✝ :: tail✝) = List.length ys
i : ℕ
h₂ : List.get? (head✝ :: tail✝) i = some x
⊢ applyId (List.zip (head✝ :: tail✝) ys) x = y ↔ List.get? ys i = some y
[PROOFSTEP]
case cons x' xs xs_ih =>
  cases i
  · injection h₂ with h₀; subst h₀
    cases ys
    · cases h₁
    ·
      -- porting note: `open List` no longer makes `zip_cons_cons` visiblesimp only [List.applyId, Prod.toSigma,
        Option.getD_some, List.get?, List.dlookup_cons_eq, List.zip_cons_cons, List.map, Option.some_inj]
  · cases ys
    · cases h₁
    · cases' h₀ with _ _ h₀ h₁
      simp only [List.get?, List.zip_cons_cons, List.applyId_cons] at h₂ ⊢
      rw [if_neg]
      · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
      · apply h₀; apply List.get?_mem h₂
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
ys : List α
h₀ : List.Nodup (x' :: xs)
h₁ : List.length (x' :: xs) = List.length ys
i : ℕ
h₂ : List.get? (x' :: xs) i = some x
⊢ applyId (List.zip (x' :: xs) ys) x = y ↔ List.get? ys i = some y
[PROOFSTEP]
case cons x' xs xs_ih =>
  cases i
  · injection h₂ with h₀; subst h₀
    cases ys
    · cases h₁
    ·
      -- porting note: `open List` no longer makes `zip_cons_cons` visiblesimp only [List.applyId, Prod.toSigma,
        Option.getD_some, List.get?, List.dlookup_cons_eq, List.zip_cons_cons, List.map, Option.some_inj]
  · cases ys
    · cases h₁
    · cases' h₀ with _ _ h₀ h₁
      simp only [List.get?, List.zip_cons_cons, List.applyId_cons] at h₂ ⊢
      rw [if_neg]
      · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
      · apply h₀; apply List.get?_mem h₂
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
ys : List α
h₀ : List.Nodup (x' :: xs)
h₁ : List.length (x' :: xs) = List.length ys
i : ℕ
h₂ : List.get? (x' :: xs) i = some x
⊢ applyId (List.zip (x' :: xs) ys) x = y ↔ List.get? ys i = some y
[PROOFSTEP]
cases i
[GOAL]
case zero
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
ys : List α
h₀ : List.Nodup (x' :: xs)
h₁ : List.length (x' :: xs) = List.length ys
h₂ : List.get? (x' :: xs) Nat.zero = some x
⊢ applyId (List.zip (x' :: xs) ys) x = y ↔ List.get? ys Nat.zero = some y
[PROOFSTEP]
injection h₂ with h₀
[GOAL]
case zero
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
ys : List α
h₀✝ : List.Nodup (x' :: xs)
h₁ : List.length (x' :: xs) = List.length ys
h₀ : x' = x
⊢ applyId (List.zip (x' :: xs) ys) x = y ↔ List.get? ys Nat.zero = some y
[PROOFSTEP]
subst h₀
[GOAL]
case zero
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
y x' : α
xs ys : List α
h₀ : List.Nodup (x' :: xs)
h₁ : List.length (x' :: xs) = List.length ys
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x' → (applyId (List.zip xs ys) x' = y ↔ List.get? ys i = some y)
⊢ applyId (List.zip (x' :: xs) ys) x' = y ↔ List.get? ys Nat.zero = some y
[PROOFSTEP]
cases ys
[GOAL]
case zero.nil
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : List.Nodup (x' :: xs)
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x' → (applyId (List.zip xs ys) x' = y ↔ List.get? ys i = some y)
h₁ : List.length (x' :: xs) = List.length []
⊢ applyId (List.zip (x' :: xs) []) x' = y ↔ List.get? [] Nat.zero = some y
[PROOFSTEP]
cases h₁
[GOAL]
case zero.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : List.Nodup (x' :: xs)
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x' → (applyId (List.zip xs ys) x' = y ↔ List.get? ys i = some y)
head✝ : α
tail✝ : List α
h₁ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
⊢ applyId (List.zip (x' :: xs) (head✝ :: tail✝)) x' = y ↔ List.get? (head✝ :: tail✝) Nat.zero = some y
[PROOFSTEP]
simp only [List.applyId, Prod.toSigma, Option.getD_some, List.get?, List.dlookup_cons_eq, List.zip_cons_cons, List.map,
  Option.some_inj]
[GOAL]
case succ
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
ys : List α
h₀ : List.Nodup (x' :: xs)
h₁ : List.length (x' :: xs) = List.length ys
n✝ : ℕ
h₂ : List.get? (x' :: xs) (Nat.succ n✝) = some x
⊢ applyId (List.zip (x' :: xs) ys) x = y ↔ List.get? ys (Nat.succ n✝) = some y
[PROOFSTEP]
cases ys
[GOAL]
case succ.nil
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
h₀ : List.Nodup (x' :: xs)
n✝ : ℕ
h₂ : List.get? (x' :: xs) (Nat.succ n✝) = some x
h₁ : List.length (x' :: xs) = List.length []
⊢ applyId (List.zip (x' :: xs) []) x = y ↔ List.get? [] (Nat.succ n✝) = some y
[PROOFSTEP]
cases h₁
[GOAL]
case succ.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
h₀ : List.Nodup (x' :: xs)
n✝ : ℕ
h₂ : List.get? (x' :: xs) (Nat.succ n✝) = some x
head✝ : α
tail✝ : List α
h₁ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
⊢ applyId (List.zip (x' :: xs) (head✝ :: tail✝)) x = y ↔ List.get? (head✝ :: tail✝) (Nat.succ n✝) = some y
[PROOFSTEP]
cases' h₀ with _ _ h₀ h₁
[GOAL]
case succ.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? (x' :: xs) (Nat.succ n✝) = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ applyId (List.zip (x' :: xs) (head✝ :: tail✝)) x = y ↔ List.get? (head✝ :: tail✝) (Nat.succ n✝) = some y
[PROOFSTEP]
simp only [List.get?, List.zip_cons_cons, List.applyId_cons] at h₂ ⊢
[GOAL]
case succ.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? xs n✝ = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ (if x' = x then head✝ else applyId (List.zip xs tail✝) x) = y ↔ List.get? tail✝ n✝ = some y
[PROOFSTEP]
rw [if_neg]
[GOAL]
case succ.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? xs n✝ = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ applyId (List.zip xs tail✝) x = y ↔ List.get? tail✝ n✝ = some y
[PROOFSTEP]
apply xs_ih
[GOAL]
case succ.cons.cons.h₀
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? xs n✝ = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ List.Nodup xs
[PROOFSTEP]
solve_by_elim [Nat.succ.inj]
[GOAL]
case succ.cons.cons.h₁
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? xs n✝ = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ List.length xs = List.length tail✝
[PROOFSTEP]
solve_by_elim [Nat.succ.inj]
[GOAL]
case succ.cons.cons.h₂
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? xs n✝ = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ List.get? xs n✝ = some x
[PROOFSTEP]
solve_by_elim [Nat.succ.inj]
[GOAL]
case succ.cons.cons.hnc
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? xs n✝ = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ ¬x' = x
[PROOFSTEP]
apply h₀
[GOAL]
case succ.cons.cons.hnc.a
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.length xs = List.length ys →
        ∀ (i : ℕ), List.get? xs i = some x → (applyId (List.zip xs ys) x = y ↔ List.get? ys i = some y)
n✝ : ℕ
h₂ : List.get? xs n✝ = some x
head✝ : α
tail✝ : List α
h₁✝ : List.length (x' :: xs) = List.length (head✝ :: tail✝)
h₁ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ x ∈ xs
[PROOFSTEP]
apply List.get?_mem h₂
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x : α
⊢ applyId (List.zip xs ys) x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
simp only [List.applyId]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x : α
⊢ Option.getD (List.dlookup x (List.map Prod.toSigma (List.zip xs ys))) x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
cases h₃ : List.dlookup x (List.map Prod.toSigma (xs.zip ys)) with
| none =>
  dsimp [Option.getD]
  rw [h₁.mem_iff]
| some val =>
  have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
  replace h₁ : xs.length = ys.length := h₁.length_eq
  dsimp
  induction xs generalizing ys with
  | nil => contradiction
  | cons x' xs xs_ih =>
    cases' ys with y ys
    · cases h₃
    dsimp [List.dlookup] at h₃ ; split_ifs at h₃  with h
    · rw [Option.some_inj] at h₃
      subst x'; subst val
      simp only [List.mem_cons, true_or_iff, eq_self_iff_true]
    · cases' h₀ with _ _ h₀ h₅
      cases' h₂ with _ _ h₂ h₄
      have h₆ := Nat.succ.inj h₁
      specialize xs_ih h₅ h₃ h₄ h₆
      simp only [Ne.symm h, xs_ih, List.mem_cons, false_or_iff]
      suffices : val ∈ ys; tauto
      erw [← Option.mem_def, List.mem_dlookup_iff] at h₃
      simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃
      rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
      apply (List.mem_zip h₃).2
      simp only [List.NodupKeys, List.keys, comp, Prod.fst_toSigma, List.map_map]
      rwa [List.map_fst_zip _ _ (le_of_eq h₆)]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x : α
x✝ : Option α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = x✝
⊢ Option.getD x✝ x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
cases h₃ : List.dlookup x (List.map Prod.toSigma (xs.zip ys)) with
| none =>
  dsimp [Option.getD]
  rw [h₁.mem_iff]
| some val =>
  have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
  replace h₁ : xs.length = ys.length := h₁.length_eq
  dsimp
  induction xs generalizing ys with
  | nil => contradiction
  | cons x' xs xs_ih =>
    cases' ys with y ys
    · cases h₃
    dsimp [List.dlookup] at h₃ ; split_ifs at h₃  with h
    · rw [Option.some_inj] at h₃
      subst x'; subst val
      simp only [List.mem_cons, true_or_iff, eq_self_iff_true]
    · cases' h₀ with _ _ h₀ h₅
      cases' h₂ with _ _ h₂ h₄
      have h₆ := Nat.succ.inj h₁
      specialize xs_ih h₅ h₃ h₄ h₆
      simp only [Ne.symm h, xs_ih, List.mem_cons, false_or_iff]
      suffices : val ∈ ys; tauto
      erw [← Option.mem_def, List.mem_dlookup_iff] at h₃
      simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃
      rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
      apply (List.mem_zip h₃).2
      simp only [List.NodupKeys, List.keys, comp, Prod.fst_toSigma, List.map_map]
      rwa [List.map_fst_zip _ _ (le_of_eq h₆)]
[GOAL]
case none
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = none
⊢ Option.getD none x ∈ ys ↔ x ∈ xs
[PROOFSTEP]

| none =>
  dsimp [Option.getD]
  rw [h₁.mem_iff]
[GOAL]
case none
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = none
⊢ Option.getD none x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
dsimp [Option.getD]
[GOAL]
case none
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = none
⊢ x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
rw [h₁.mem_iff]
[GOAL]
case some
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x val : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
⊢ Option.getD (some val) x ∈ ys ↔ x ∈ xs
[PROOFSTEP]

| some val =>
  have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
  replace h₁ : xs.length = ys.length := h₁.length_eq
  dsimp
  induction xs generalizing ys with
  | nil => contradiction
  | cons x' xs xs_ih =>
    cases' ys with y ys
    · cases h₃
    dsimp [List.dlookup] at h₃ ; split_ifs at h₃  with h
    · rw [Option.some_inj] at h₃
      subst x'; subst val
      simp only [List.mem_cons, true_or_iff, eq_self_iff_true]
    · cases' h₀ with _ _ h₀ h₅
      cases' h₂ with _ _ h₂ h₄
      have h₆ := Nat.succ.inj h₁
      specialize xs_ih h₅ h₃ h₄ h₆
      simp only [Ne.symm h, xs_ih, List.mem_cons, false_or_iff]
      suffices : val ∈ ys; tauto
      erw [← Option.mem_def, List.mem_dlookup_iff] at h₃
      simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃
      rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
      apply (List.mem_zip h₃).2
      simp only [List.NodupKeys, List.keys, comp, Prod.fst_toSigma, List.map_map]
      rwa [List.map_fst_zip _ _ (le_of_eq h₆)]
[GOAL]
case some
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x val : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
⊢ Option.getD (some val) x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
[GOAL]
case some
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x val : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₂ : List.Nodup ys
⊢ Option.getD (some val) x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
replace h₁ : xs.length = ys.length := h₁.length_eq
[GOAL]
case some
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
x val : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₂ : List.Nodup ys
h₁ : List.length xs = List.length ys
⊢ Option.getD (some val) x ∈ ys ↔ x ∈ xs
[PROOFSTEP]
dsimp
[GOAL]
case some
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
x val : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₂ : List.Nodup ys
h₁ : List.length xs = List.length ys
⊢ val ∈ ys ↔ x ∈ xs
[PROOFSTEP]
induction xs generalizing ys with
| nil => contradiction
| cons x' xs xs_ih =>
  cases' ys with y ys
  · cases h₃
  dsimp [List.dlookup] at h₃ ; split_ifs at h₃  with h
  · rw [Option.some_inj] at h₃
    subst x'; subst val
    simp only [List.mem_cons, true_or_iff, eq_self_iff_true]
  · cases' h₀ with _ _ h₀ h₅
    cases' h₂ with _ _ h₂ h₄
    have h₆ := Nat.succ.inj h₁
    specialize xs_ih h₅ h₃ h₄ h₆
    simp only [Ne.symm h, xs_ih, List.mem_cons, false_or_iff]
    suffices : val ∈ ys; tauto
    erw [← Option.mem_def, List.mem_dlookup_iff] at h₃
    simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃
    rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
    apply (List.mem_zip h₃).2
    simp only [List.NodupKeys, List.keys, comp, Prod.fst_toSigma, List.map_map]
    rwa [List.map_fst_zip _ _ (le_of_eq h₆)]
[GOAL]
case some
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
x val : α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₂ : List.Nodup ys
h₁ : List.length xs = List.length ys
⊢ val ∈ ys ↔ x ∈ xs
[PROOFSTEP]
induction xs generalizing ys with
| nil => contradiction
| cons x' xs xs_ih =>
  cases' ys with y ys
  · cases h₃
  dsimp [List.dlookup] at h₃ ; split_ifs at h₃  with h
  · rw [Option.some_inj] at h₃
    subst x'; subst val
    simp only [List.mem_cons, true_or_iff, eq_self_iff_true]
  · cases' h₀ with _ _ h₀ h₅
    cases' h₂ with _ _ h₂ h₄
    have h₆ := Nat.succ.inj h₁
    specialize xs_ih h₅ h₃ h₄ h₆
    simp only [Ne.symm h, xs_ih, List.mem_cons, false_or_iff]
    suffices : val ∈ ys; tauto
    erw [← Option.mem_def, List.mem_dlookup_iff] at h₃
    simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃
    rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
    apply (List.mem_zip h₃).2
    simp only [List.NodupKeys, List.keys, comp, Prod.fst_toSigma, List.map_map]
    rwa [List.map_fst_zip _ _ (le_of_eq h₆)]
[GOAL]
case some.nil
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val : α
ys : List α
h₀ : List.Nodup []
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip [] ys)) = some val
h₂ : List.Nodup ys
h₁ : List.length [] = List.length ys
⊢ val ∈ ys ↔ x ∈ []
[PROOFSTEP]

| nil => contradiction
[GOAL]
case some.nil
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val : α
ys : List α
h₀ : List.Nodup []
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip [] ys)) = some val
h₂ : List.Nodup ys
h₁ : List.length [] = List.length ys
⊢ val ∈ ys ↔ x ∈ []
[PROOFSTEP]
contradiction
[GOAL]
case some.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
ys : List α
h₀ : List.Nodup (x' :: xs)
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip (x' :: xs) ys)) = some val
h₂ : List.Nodup ys
h₁ : List.length (x' :: xs) = List.length ys
⊢ val ∈ ys ↔ x ∈ x' :: xs
[PROOFSTEP]

| cons x' xs xs_ih =>
  cases' ys with y ys
  · cases h₃
  dsimp [List.dlookup] at h₃ ; split_ifs at h₃  with h
  · rw [Option.some_inj] at h₃
    subst x'; subst val
    simp only [List.mem_cons, true_or_iff, eq_self_iff_true]
  · cases' h₀ with _ _ h₀ h₅
    cases' h₂ with _ _ h₂ h₄
    have h₆ := Nat.succ.inj h₁
    specialize xs_ih h₅ h₃ h₄ h₆
    simp only [Ne.symm h, xs_ih, List.mem_cons, false_or_iff]
    suffices : val ∈ ys; tauto
    erw [← Option.mem_def, List.mem_dlookup_iff] at h₃
    simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃
    rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
    apply (List.mem_zip h₃).2
    simp only [List.NodupKeys, List.keys, comp, Prod.fst_toSigma, List.map_map]
    rwa [List.map_fst_zip _ _ (le_of_eq h₆)]
[GOAL]
case some.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
ys : List α
h₀ : List.Nodup (x' :: xs)
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip (x' :: xs) ys)) = some val
h₂ : List.Nodup ys
h₁ : List.length (x' :: xs) = List.length ys
⊢ val ∈ ys ↔ x ∈ x' :: xs
[PROOFSTEP]
cases' ys with y ys
[GOAL]
case some.cons.nil
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
h₀ : List.Nodup (x' :: xs)
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip (x' :: xs) [])) = some val
h₂ : List.Nodup []
h₁ : List.length (x' :: xs) = List.length []
⊢ val ∈ [] ↔ x ∈ x' :: xs
[PROOFSTEP]
cases h₃
[GOAL]
case some.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
h₀ : List.Nodup (x' :: xs)
y : α
ys : List α
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip (x' :: xs) (y :: ys))) = some val
h₂ : List.Nodup (y :: ys)
h₁ : List.length (x' :: xs) = List.length (y :: ys)
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
dsimp [List.dlookup] at h₃
[GOAL]
case some.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
h₀ : List.Nodup (x' :: xs)
y : α
ys : List α
h₃ : (if h : x' = x then some (h ▸ y) else List.dlookup x (List.map Prod.toSigma (List.zip xs ys))) = some val
h₂ : List.Nodup (y :: ys)
h₁ : List.length (x' :: xs) = List.length (y :: ys)
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
split_ifs at h₃  with h
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
h₀ : List.Nodup (x' :: xs)
y : α
ys : List α
h₂ : List.Nodup (y :: ys)
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : x' = x
h₃ : some (h ▸ y) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
rw [Option.some_inj] at h₃
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
h₀ : List.Nodup (x' :: xs)
y : α
ys : List α
h₂ : List.Nodup (y :: ys)
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : x' = x
h₃ : h ▸ y = val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
subst x'
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
y : α
ys : List α
h₂ : List.Nodup (y :: ys)
h₀ : List.Nodup (x :: xs)
h₁ : List.length (x :: xs) = List.length (y :: ys)
h₃ : (_ : x = x) ▸ y = val
⊢ val ∈ y :: ys ↔ x ∈ x :: xs
[PROOFSTEP]
subst val
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x : α
xs : List α
y : α
ys : List α
h₂ : List.Nodup (y :: ys)
h₀ : List.Nodup (x :: xs)
h₁ : List.length (x :: xs) = List.length (y :: ys)
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some ((_ : x = x) ▸ y) →
        List.Nodup ys → List.length xs = List.length ys → ((_ : x = x) ▸ y ∈ ys ↔ x ∈ xs)
⊢ (_ : x = x) ▸ y ∈ y :: ys ↔ x ∈ x :: xs
[PROOFSTEP]
simp only [List.mem_cons, true_or_iff, eq_self_iff_true]
[GOAL]
case neg
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
h₀ : List.Nodup (x' :: xs)
y : α
ys : List α
h₂ : List.Nodup (y :: ys)
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
cases' h₀ with _ _ h₀ h₅
[GOAL]
case neg.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
y : α
ys : List α
h₂ : List.Nodup (y :: ys)
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
cases' h₂ with _ _ h₂ h₄
[GOAL]
case neg.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
have h₆ := Nat.succ.inj h₁
[GOAL]
case neg.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    List.Nodup xs →
      List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val →
        List.Nodup ys → List.length xs = List.length ys → (val ∈ ys ↔ x ∈ xs)
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
specialize xs_ih h₅ h₃ h₄ h₆
[GOAL]
case neg.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
[PROOFSTEP]
simp only [Ne.symm h, xs_ih, List.mem_cons, false_or_iff]
[GOAL]
case neg.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ val = y ∨ x ∈ xs ↔ x ∈ xs
[PROOFSTEP]
suffices : val ∈ ys
[GOAL]
case neg.cons.cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
this : val ∈ ys
⊢ val = y ∨ x ∈ xs ↔ x ∈ xs
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ val ∈ ys
[PROOFSTEP]
tauto
[GOAL]
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : List.dlookup x (List.map Prod.toSigma (List.zip xs ys)) = some val
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ val ∈ ys
[PROOFSTEP]
erw [← Option.mem_def, List.mem_dlookup_iff] at h₃
[GOAL]
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : { fst := x, snd := val } ∈ List.map Prod.toSigma (List.zip xs ys)
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ val ∈ ys
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : val ∈ List.dlookup x (List.map Prod.toSigma (List.zip xs ys))
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ List.NodupKeys (List.map Prod.toSigma (List.zip xs ys))
[PROOFSTEP]
simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃
[GOAL]
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
h₃ : ∃ a b, (a, b) ∈ List.zip xs ys ∧ { fst := a, snd := b } = { fst := x, snd := val }
⊢ val ∈ ys
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : val ∈ List.dlookup x (List.map Prod.toSigma (List.zip xs ys))
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ List.NodupKeys (List.map Prod.toSigma (List.zip xs ys))
[PROOFSTEP]
rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
[GOAL]
case this.intro.intro.intro.refl
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
h₃ : (x, val) ∈ List.zip xs ys
⊢ val ∈ ys
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : val ∈ List.dlookup x (List.map Prod.toSigma (List.zip xs ys))
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ List.NodupKeys (List.map Prod.toSigma (List.zip xs ys))
[PROOFSTEP]
apply (List.mem_zip h₃).2
[GOAL]
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : val ∈ List.dlookup x (List.map Prod.toSigma (List.zip xs ys))
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ List.NodupKeys (List.map Prod.toSigma (List.zip xs ys))
[PROOFSTEP]
simp only [List.NodupKeys, List.keys, comp, Prod.fst_toSigma, List.map_map]
[GOAL]
case this
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : List.length (x' :: xs) = List.length (y :: ys)
h : ¬x' = x
h₃ : val ∈ List.dlookup x (List.map Prod.toSigma (List.zip xs ys))
h₅ : List.Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x' ≠ a'
h₄ : List.Pairwise (fun x x_1 => x ≠ x_1) ys
h₂ : ∀ (a' : α), a' ∈ ys → y ≠ a'
h₆ : List.length xs = List.length ys
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ List.Nodup (List.map (fun x => x.fst) (List.zip xs ys))
[PROOFSTEP]
rwa [List.map_fst_zip _ _ (le_of_eq h₆)]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
⊢ ¬x ∈ xs → applyId (List.zip xs ys) x = x
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
h : ¬x ∈ xs
⊢ applyId (List.zip xs ys) x = x
[PROOFSTEP]
dsimp [List.applyId]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
h : ¬x ∈ xs
⊢ Option.getD (List.dlookup x (List.map Prod.toSigma (List.zip xs ys))) x = x
[PROOFSTEP]
rw [List.dlookup_eq_none.2]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
h : ¬x ∈ xs
⊢ Option.getD none x = x
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
h : ¬x ∈ xs
⊢ ¬x ∈ List.keys (List.map Prod.toSigma (List.zip xs ys))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
h : ¬x ∈ xs
⊢ ¬x ∈ List.keys (List.map Prod.toSigma (List.zip xs ys))
[PROOFSTEP]
simp only [List.keys, not_exists, Prod.toSigma, exists_and_right, exists_eq_right, List.mem_map, Function.comp_apply,
  List.map_map, Prod.exists]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
h : ¬x ∈ xs
⊢ ∀ (x_1 : α), ¬(x, x_1) ∈ List.zip xs ys
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
x : α
h : ¬x ∈ xs
y : α
hy : (x, y) ∈ List.zip xs ys
⊢ False
[PROOFSTEP]
exact h (List.mem_zip hy).1
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
⊢ Injective (applyId (List.zip xs ys))
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
⊢ x = y
[PROOFSTEP]
by_cases hx : x ∈ xs
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : x ∈ xs
⊢ x = y
[PROOFSTEP]
by_cases hy : y ∈ xs
[GOAL]
case neg
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : ¬x ∈ xs
⊢ x = y
[PROOFSTEP]
by_cases hy : y ∈ xs
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : x ∈ xs
hy : y ∈ xs
⊢ x = y
[PROOFSTEP]
rw [List.mem_iff_get?] at hx hy
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : ∃ n, List.get? xs n = some x
hy : ∃ n, List.get? xs n = some y
⊢ x = y
[PROOFSTEP]
cases' hx with i hx
[GOAL]
case pos.intro
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hy : ∃ n, List.get? xs n = some y
i : ℕ
hx : List.get? xs i = some x
⊢ x = y
[PROOFSTEP]
cases' hy with j hy
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
i : ℕ
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
⊢ x = y
[PROOFSTEP]
suffices some x = some y by injection this
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
i : ℕ
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
this : some x = some y
⊢ x = y
[PROOFSTEP]
injection this
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
i : ℕ
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
⊢ some x = some y
[PROOFSTEP]
have h₂ := h₁.length_eq
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
i : ℕ
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ some x = some y
[PROOFSTEP]
rw [List.applyId_zip_eq h₀ h₂ _ _ _ hx] at h
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ some x = some y
[PROOFSTEP]
rw [← hx, ← hy]
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ List.get? xs i = List.get? xs j
[PROOFSTEP]
congr
[GOAL]
case pos.intro.intro.e_a
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ i = j
[PROOFSTEP]
apply List.get?_injective _ (h₁.nodup_iff.1 h₀)
[GOAL]
case pos.intro.intro.e_a
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ List.get? ys i = List.get? ys j
[PROOFSTEP]
symm
[GOAL]
case pos.intro.intro.e_a
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ List.get? ys j = List.get? ys i
[PROOFSTEP]
rw [h]
[GOAL]
case pos.intro.intro.e_a
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ List.get? ys j = some (applyId (List.zip xs ys) y)
[PROOFSTEP]
rw [← List.applyId_zip_eq]
[GOAL]
case pos.intro.intro.e_a.h₀
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ List.Nodup xs
[PROOFSTEP]
assumption
[GOAL]
case pos.intro.intro.e_a.h₁
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ List.length xs = List.length ys
[PROOFSTEP]
assumption
[GOAL]
case pos.intro.intro.e_a.h₂
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ List.get? xs j = some y
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ i < List.length ys
[PROOFSTEP]
rw [← h₁.length_eq]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : List.get? xs i = some x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ i < List.length xs
[PROOFSTEP]
rw [List.get?_eq_some] at hx
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
hx : ∃ h, List.get xs { val := i, isLt := h } = x
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
⊢ i < List.length xs
[PROOFSTEP]
cases' hx with hx hx'
[GOAL]
case intro
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
i : ℕ
h : List.get? ys i = some (applyId (List.zip xs ys) y)
j : ℕ
hy : List.get? xs j = some y
h₂ : List.length xs = List.length ys
hx : i < List.length xs
hx' : List.get xs { val := i, isLt := hx } = x
⊢ i < List.length xs
[PROOFSTEP]
exact hx
[GOAL]
case neg
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : x ∈ xs
hy : ¬y ∈ xs
⊢ x = y
[PROOFSTEP]
rw [← applyId_mem_iff h₀ h₁] at hx hy
[GOAL]
case neg
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : applyId (List.zip xs ys) x ∈ ys
hy : ¬applyId (List.zip xs ys) y ∈ ys
⊢ x = y
[PROOFSTEP]
rw [h] at hx
[GOAL]
case neg
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : applyId (List.zip xs ys) y ∈ ys
hy : ¬applyId (List.zip xs ys) y ∈ ys
⊢ x = y
[PROOFSTEP]
contradiction
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : ¬x ∈ xs
hy : y ∈ xs
⊢ x = y
[PROOFSTEP]
rw [← applyId_mem_iff h₀ h₁] at hx hy
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : ¬applyId (List.zip xs ys) x ∈ ys
hy : applyId (List.zip xs ys) y ∈ ys
⊢ x = y
[PROOFSTEP]
rw [h] at hx
[GOAL]
case pos
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : ¬applyId (List.zip xs ys) y ∈ ys
hy : applyId (List.zip xs ys) y ∈ ys
⊢ x = y
[PROOFSTEP]
contradiction
[GOAL]
case neg
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : ¬x ∈ xs
hy : ¬y ∈ xs
⊢ x = y
[PROOFSTEP]
rwa [List.applyId_eq_self, List.applyId_eq_self] at h
[GOAL]
case neg.a
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : x = applyId (List.zip xs ys) y
hx : ¬x ∈ xs
hy : ¬y ∈ xs
⊢ ¬y ∈ xs
[PROOFSTEP]
assumption
[GOAL]
case neg.a
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs ys : List α
h₀ : List.Nodup xs
h₁ : xs ~ ys
x y : α
h : applyId (List.zip xs ys) x = applyId (List.zip xs ys) y
hx : ¬x ∈ xs
hy : ¬y ∈ xs
⊢ ¬x ∈ xs
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
γ : Sort w
x✝ : ℕ
n : ℕ := x✝
h : 0 < n
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
α✝ : Type u
β : Type v
γ : Sort w
α : Type
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
h₀✝ : List.map Sigma.fst xs ~ List.map Sigma.snd xs
h₁✝ : List.Nodup (List.map Sigma.snd xs)
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : List.Nodup ys'
h₃ : List.length xs' ≤ List.length ys'
h₄ : List.length ys' ≤ List.length xs'
⊢ List.map Sigma.fst (List.map Prod.toSigma (List.zip xs' ys')) ~
    List.map Sigma.snd (List.map Prod.toSigma (List.zip xs' ys'))
[PROOFSTEP]
simp only [comp, List.map_fst_zip, List.map_snd_zip, *, Prod.fst_toSigma, Prod.snd_toSigma, List.map_map]
[GOAL]
α✝ : Type u
β : Type v
γ : Sort w
α : Type
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
h₀✝ : List.map Sigma.fst xs ~ List.map Sigma.snd xs
h₁✝ : List.Nodup (List.map Sigma.snd xs)
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : List.Nodup ys'
h₃ : List.length xs' ≤ List.length ys'
h₄ : List.length ys' ≤ List.length xs'
⊢ List.Nodup (List.map Sigma.snd (List.map Prod.toSigma (List.zip xs' ys')))
[PROOFSTEP]
simp only [comp, List.map_snd_zip, *, Prod.snd_toSigma, List.map_map]
[GOAL]
α : Type u
β : Type v
γ : Sort w
xs ys : List α
h : xs ~ ys
h' : List.Nodup ys
h₀ : List.length xs ≤ List.length ys
h₁ : List.length ys ≤ List.length xs
⊢ List.map Sigma.fst (List.toFinmap' (List.zip xs ys)) ~ List.map Sigma.snd (List.toFinmap' (List.zip xs ys))
[PROOFSTEP]
simp only [List.toFinmap', comp, List.map_fst_zip, List.map_snd_zip, *, Prod.fst_toSigma, Prod.snd_toSigma,
  List.map_map]
[GOAL]
α : Type u
β : Type v
γ : Sort w
xs ys : List α
h : xs ~ ys
h' : List.Nodup ys
h₀ : List.length xs ≤ List.length ys
h₁ : List.length ys ≤ List.length xs
⊢ List.Nodup (List.map Sigma.snd (List.toFinmap' (List.zip xs ys)))
[PROOFSTEP]
simp only [List.toFinmap', comp, List.map_snd_zip, *, Prod.snd_toSigma, List.map_map]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
f : InjectiveFunction α
⊢ Injective (apply f)
[PROOFSTEP]
cases' f with xs hperm hnodup
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs
hnodup : List.Nodup (List.map Sigma.snd xs)
⊢ Injective (apply (mapToSelf xs hperm hnodup))
[PROOFSTEP]
generalize h₀ : List.map Sigma.fst xs = xs₀
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs
hnodup : List.Nodup (List.map Sigma.snd xs)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
⊢ Injective (apply (mapToSelf xs hperm hnodup))
[PROOFSTEP]
generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs
hnodup : List.Nodup (List.map Sigma.snd xs)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map (id Sigma.snd) xs = xs₁
⊢ Injective (apply (mapToSelf xs hperm hnodup))
[PROOFSTEP]
dsimp [id] at h₁
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs
hnodup : List.Nodup (List.map Sigma.snd xs)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
⊢ Injective (apply (mapToSelf xs hperm hnodup))
[PROOFSTEP]
have hxs : xs = TotalFunction.List.toFinmap' (xs₀.zip xs₁) :=
  by
  rw [← h₀, ← h₁, List.toFinmap']; clear h₀ h₁ xs₀ xs₁ hperm hnodup
  induction xs
  case nil => simp only [List.zip_nil_right, List.map_nil]
  case cons xs_hd xs_tl
    xs_ih =>
    simp only [true_and_iff, Prod.toSigma, eq_self_iff_true, Sigma.eta, List.zip_cons_cons, List.map, List.cons_inj]
    exact xs_ih
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs
hnodup : List.Nodup (List.map Sigma.snd xs)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
⊢ xs = List.toFinmap' (List.zip xs₀ xs₁)
[PROOFSTEP]
rw [← h₀, ← h₁, List.toFinmap']
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs
hnodup : List.Nodup (List.map Sigma.snd xs)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
⊢ xs = List.map Prod.toSigma (List.zip (List.map Sigma.fst xs) (List.map Sigma.snd xs))
[PROOFSTEP]
clear h₀ h₁ xs₀ xs₁ hperm hnodup
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
⊢ xs = List.map Prod.toSigma (List.zip (List.map Sigma.fst xs) (List.map Sigma.snd xs))
[PROOFSTEP]
induction xs
[GOAL]
case nil
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
⊢ [] = List.map Prod.toSigma (List.zip (List.map Sigma.fst []) (List.map Sigma.snd []))
case cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
head✝ : (_ : α) × α
tail✝ : List ((_ : α) × α)
tail_ih✝ : tail✝ = List.map Prod.toSigma (List.zip (List.map Sigma.fst tail✝) (List.map Sigma.snd tail✝))
⊢ head✝ :: tail✝ =
    List.map Prod.toSigma (List.zip (List.map Sigma.fst (head✝ :: tail✝)) (List.map Sigma.snd (head✝ :: tail✝)))
[PROOFSTEP]
case nil => simp only [List.zip_nil_right, List.map_nil]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
⊢ [] = List.map Prod.toSigma (List.zip (List.map Sigma.fst []) (List.map Sigma.snd []))
[PROOFSTEP]
case nil => simp only [List.zip_nil_right, List.map_nil]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
⊢ [] = List.map Prod.toSigma (List.zip (List.map Sigma.fst []) (List.map Sigma.snd []))
[PROOFSTEP]
simp only [List.zip_nil_right, List.map_nil]
[GOAL]
case cons
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
head✝ : (_ : α) × α
tail✝ : List ((_ : α) × α)
tail_ih✝ : tail✝ = List.map Prod.toSigma (List.zip (List.map Sigma.fst tail✝) (List.map Sigma.snd tail✝))
⊢ head✝ :: tail✝ =
    List.map Prod.toSigma (List.zip (List.map Sigma.fst (head✝ :: tail✝)) (List.map Sigma.snd (head✝ :: tail✝)))
[PROOFSTEP]
case cons xs_hd xs_tl
  xs_ih =>
  simp only [true_and_iff, Prod.toSigma, eq_self_iff_true, Sigma.eta, List.zip_cons_cons, List.map, List.cons_inj]
  exact xs_ih
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih : xs_tl = List.map Prod.toSigma (List.zip (List.map Sigma.fst xs_tl) (List.map Sigma.snd xs_tl))
⊢ xs_hd :: xs_tl =
    List.map Prod.toSigma (List.zip (List.map Sigma.fst (xs_hd :: xs_tl)) (List.map Sigma.snd (xs_hd :: xs_tl)))
[PROOFSTEP]
case cons xs_hd xs_tl
  xs_ih =>
  simp only [true_and_iff, Prod.toSigma, eq_self_iff_true, Sigma.eta, List.zip_cons_cons, List.map, List.cons_inj]
  exact xs_ih
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih : xs_tl = List.map Prod.toSigma (List.zip (List.map Sigma.fst xs_tl) (List.map Sigma.snd xs_tl))
⊢ xs_hd :: xs_tl =
    List.map Prod.toSigma (List.zip (List.map Sigma.fst (xs_hd :: xs_tl)) (List.map Sigma.snd (xs_hd :: xs_tl)))
[PROOFSTEP]
simp only [true_and_iff, Prod.toSigma, eq_self_iff_true, Sigma.eta, List.zip_cons_cons, List.map, List.cons_inj]
[GOAL]
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih : xs_tl = List.map Prod.toSigma (List.zip (List.map Sigma.fst xs_tl) (List.map Sigma.snd xs_tl))
⊢ xs_tl =
    List.map (fun p => { fst := p.fst, snd := p.snd })
      (List.zipWith Prod.mk (List.map Sigma.fst xs_tl) (List.map Sigma.snd xs_tl))
[PROOFSTEP]
exact xs_ih
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs
hnodup : List.Nodup (List.map Sigma.snd xs)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (List.zip xs₀ xs₁)
⊢ Injective (apply (mapToSelf xs hperm hnodup))
[PROOFSTEP]
revert hperm hnodup
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (List.zip xs₀ xs₁)
⊢ ∀ (hperm : List.map Sigma.fst xs ~ List.map Sigma.snd xs) (hnodup : List.Nodup (List.map Sigma.snd xs)),
    Injective (apply (mapToSelf xs hperm hnodup))
[PROOFSTEP]
rw [hxs]
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (List.zip xs₀ xs₁)
⊢ ∀
    (hperm :
      List.map Sigma.fst (List.toFinmap' (List.zip xs₀ xs₁)) ~ List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁)))
    (hnodup : List.Nodup (List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁)))),
    Injective (apply (mapToSelf (List.toFinmap' (List.zip xs₀ xs₁)) hperm hnodup))
[PROOFSTEP]
intros hperm hnodup
[GOAL]
case mapToSelf
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (List.zip xs₀ xs₁)
hperm : List.map Sigma.fst (List.toFinmap' (List.zip xs₀ xs₁)) ~ List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁))
hnodup : List.Nodup (List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁)))
⊢ Injective (apply (mapToSelf (List.toFinmap' (List.zip xs₀ xs₁)) hperm hnodup))
[PROOFSTEP]
apply InjectiveFunction.applyId_injective
[GOAL]
case mapToSelf.h₀
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (List.zip xs₀ xs₁)
hperm : List.map Sigma.fst (List.toFinmap' (List.zip xs₀ xs₁)) ~ List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁))
hnodup : List.Nodup (List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁)))
⊢ List.Nodup xs₀
[PROOFSTEP]
rwa [← h₀, hxs, hperm.nodup_iff]
[GOAL]
case mapToSelf.h₁
α : Type u
β : Type v
γ : Sort w
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : List.map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : List.map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (List.zip xs₀ xs₁)
hperm : List.map Sigma.fst (List.toFinmap' (List.zip xs₀ xs₁)) ~ List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁))
hnodup : List.Nodup (List.map Sigma.snd (List.toFinmap' (List.zip xs₀ xs₁)))
⊢ xs₀ ~ xs₁
[PROOFSTEP]
rwa [← hxs, h₀, h₁] at hperm


[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ @UniversallyClosed = universally (topologically @IsClosedMap)
[PROOFSTEP]
ext X Y f
[GOAL]
case h.h.h.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyClosed f ↔ universally (topologically @IsClosedMap) f
[PROOFSTEP]
rw [UniversallyClosed_iff]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderComposition @UniversallyClosed
[PROOFSTEP]
rw [universallyClosed_eq]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderComposition (universally (topologically @IsClosedMap))
[PROOFSTEP]
exact StableUnderComposition.universally (fun X Y Z f g hf hg => @IsClosedMap.comp _ _ _ _ _ _ g.1.base f.1.base hg hf)
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ PropertyIsLocalAtTarget @UniversallyClosed
[PROOFSTEP]
rw [universallyClosed_eq]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ PropertyIsLocalAtTarget (universally (topologically @IsClosedMap))
[PROOFSTEP]
apply universallyIsLocalAtTargetOfMorphismRestrict
[GOAL]
case hP₁
X Y : Scheme
f : X ⟶ Y
⊢ RespectsIso (topologically @IsClosedMap)
[PROOFSTEP]
exact
  StableUnderComposition.respectsIso (fun X Y Z f g hf hg => @IsClosedMap.comp _ _ _ _ _ _ g.1.base f.1.base hg hf)
    (fun f => (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso f)).isClosedMap)
[GOAL]
case hP₂
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Opens ↑↑Y.toPresheafedSpace),
    iSup U = ⊤ → (∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)) → topologically (@IsClosedMap) f
[PROOFSTEP]
intro X Y f ι U hU H
[GOAL]
case hP₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑↑Y.toPresheafedSpace
hU : iSup U = ⊤
H : ∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)
⊢ topologically (@IsClosedMap) f
[PROOFSTEP]
simp_rw [topologically, morphismRestrict_base] at H
[GOAL]
case hP₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑↑Y.toPresheafedSpace
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (Set.restrictPreimage (U i).carrier ↑f.val.base)
⊢ topologically (@IsClosedMap) f
[PROOFSTEP]
exact (isClosedMap_iff_isClosedMap_of_iSup_eq_top hU).mpr H


[GOAL]
X : Scheme
⊢ Continuous fun x => PEmpty.elim x
[PROOFSTEP]
continuity
[GOAL]
X : Scheme
f g : ∅ ⟶ X
⊢ f.val.base = g.val.base
[PROOFSTEP]
ext a
[GOAL]
case w
X : Scheme
f g : ∅ ⟶ X
a : (forget TopCat).obj ↑∅.toPresheafedSpace
⊢ ↑f.val.base a = ↑g.val.base a
[PROOFSTEP]
exact PEmpty.elim a
[GOAL]
X : Scheme
f g : ∅ ⟶ X
a : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ NatTrans.app (f.val.c ≫ whiskerRight (eqToHom (_ : (Opens.map f.val.base).op = (Opens.map g.val.base).op)) ∅.presheaf)
      a =
    NatTrans.app g.val.c a
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ IsEmpty PEmpty
[PROOFSTEP]
infer_instance
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ IsOpenImmersion f
[PROOFSTEP]
apply (config := { allowSynthFailures := true }) IsOpenImmersion.of_stalk_iso
[GOAL]
case hf
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ OpenEmbedding ↑f.val.base
[PROOFSTEP]
apply openEmbedding_of_continuous_injective_open
[GOAL]
case hf.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ Continuous ↑f.val.base
[PROOFSTEP]
continuity
[GOAL]
case hf.h₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ Function.Injective ↑f.val.base
[PROOFSTEP]
rintro (i : X.carrier)
[GOAL]
case hf.h₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
i : ↑↑X.toPresheafedSpace
⊢ ∀ ⦃a₂ : (forget TopCat).obj ↑X.toPresheafedSpace⦄, ↑f.val.base i = ↑f.val.base a₂ → i = a₂
[PROOFSTEP]
exact isEmptyElim i
[GOAL]
case hf.h₃
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ IsOpenMap ↑f.val.base
[PROOFSTEP]
intro U _
[GOAL]
case hf.h₃
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
⊢ IsOpen (↑f.val.base '' U)
[PROOFSTEP]
convert isOpen_empty (α := Y)
[GOAL]
case h.e'_3.h
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
e_1✝ : (forget TopCat).obj ↑Y.toPresheafedSpace = ↑↑Y.toPresheafedSpace
⊢ ↑f.val.base '' U = ∅
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.h
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
e_1✝ : (forget TopCat).obj ↑Y.toPresheafedSpace = ↑↑Y.toPresheafedSpace
x✝ : (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ x✝ ∈ ↑f.val.base '' U ↔ x✝ ∈ ∅
[PROOFSTEP]
rw [Set.mem_empty_iff_false, iff_false_iff]
[GOAL]
case h.e'_3.h.h
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
e_1✝ : (forget TopCat).obj ↑Y.toPresheafedSpace = ↑↑Y.toPresheafedSpace
x✝ : (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ ¬x✝ ∈ ↑f.val.base '' U
[PROOFSTEP]
exact fun x => isEmptyElim (show X.carrier from x.choose)
[GOAL]
case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
rintro (i : X.carrier)
[GOAL]
case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
i : ↑↑X.toPresheafedSpace
⊢ IsIso (PresheafedSpace.stalkMap f.val i)
[PROOFSTEP]
exact isEmptyElim i
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
⊢ IsIso f
[PROOFSTEP]
haveI : IsEmpty X.carrier := ⟨fun x => isEmptyElim (show Y.carrier from f.1.base x)⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ IsIso f
[PROOFSTEP]
have : Epi f.1.base
[GOAL]
case this
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ Epi f.val.base
[PROOFSTEP]
rw [TopCat.epi_iff_surjective]
[GOAL]
case this
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ Function.Surjective ↑f.val.base
[PROOFSTEP]
rintro (x : Y.carrier)
[GOAL]
case this
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
x : ↑↑Y.toPresheafedSpace
⊢ ∃ a, ↑f.val.base a = x
[PROOFSTEP]
exact isEmptyElim x
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this✝ : IsEmpty ↑↑X.toPresheafedSpace
this : Epi f.val.base
⊢ IsIso f
[PROOFSTEP]
apply IsOpenImmersion.to_iso
[GOAL]
X : Scheme
⊢ IsAffineOpen ⊥
[PROOFSTEP]
convert rangeIsAffineOpenOfOpenImmersion (initial.to X)
[GOAL]
case h.e'_2
X : Scheme
⊢ ⊥ = Scheme.Hom.opensRange (initial.to X)
[PROOFSTEP]
ext
  -- Porting note : added this `erw` to turn LHS to `False`
[GOAL]
case h.e'_2.h.h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ↑(Scheme.Hom.opensRange (initial.to X))
[PROOFSTEP]
erw [Set.mem_empty_iff_false]
[GOAL]
case h.e'_2.h.h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ False ↔ x✝ ∈ ↑(Scheme.Hom.opensRange (initial.to X))
[PROOFSTEP]
rw [false_iff_iff]
[GOAL]
case h.e'_2.h.h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ ¬x✝ ∈ ↑(Scheme.Hom.opensRange (initial.to X))
[PROOFSTEP]
exact fun x => isEmptyElim (show (⊥_ Scheme).carrier from x.choose)
[GOAL]
A : Scheme
f : A ⟶ ⊥_ Scheme
⊢ IsIso f
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u_1
inst✝ : Category.{?u.34375, u_1} C
⊢ Category.{?u.34397, max (max (?u.34414 + 1) ?u.34375) u_1} (InducedCategory (PresheafedSpace C) toPresheafedSpace)
[PROOFSTEP]
infer_instance
  -- Porting note: adding an ext lemma.
  -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
C : Type u_1
inst✝ : Category.{?u.34683, u_1} C
X Y : SheafedSpace C
α β : X ⟶ Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.158005, u_1} C
X : SheafedSpace C
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ X.presheaf.obj U = ((𝟙 X).base _* X.presheaf).obj U
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : SheafedSpace C
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ NatTrans.app (𝟙 X).c U =
    eqToHom (_ : X.presheaf.obj U = X.presheaf.obj ((Opens.map (𝟙 ↑X.toPresheafedSpace)).op.obj U))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.162894, u_1} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝ : Category.{?u.162894, u_1} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
[PROOFSTEP]
rfl


[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType = affineLocally @RingHom.FiniteType
[PROOFSTEP]
ext X Y f
[GOAL]
case h.h.h.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFiniteType f ↔ affineLocally (@RingHom.FiniteType) f
[PROOFSTEP]
rw [LocallyOfFiniteType_iff, affineLocally_iff_affineOpens_le]
[GOAL]
case h.h.h.a.hP
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ RingHom.RespectsIso @RingHom.FiniteType
[PROOFSTEP]
exact RingHom.finiteType_respectsIso
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : LocallyOfFiniteType (f ≫ g)
⊢ LocallyOfFiniteType f
[PROOFSTEP]
revert hf
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ [hf : LocallyOfFiniteType (f ≫ g)], LocallyOfFiniteType f
[PROOFSTEP]
rw [locallyOfFiniteType_eq]
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ [hf : affineLocally (@RingHom.FiniteType) (f ≫ g)], affineLocally (@RingHom.FiniteType) f
[PROOFSTEP]
apply RingHom.finiteType_is_local.affineLocally_of_comp
[GOAL]
case H
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {R S T : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    RingHom.FiniteType (RingHom.comp g f) → RingHom.FiniteType g
[PROOFSTEP]
introv H
[GOAL]
case H
X✝ Y✝ : Scheme
f✝¹ : X✝ ⟶ Y✝
X Y Z : Scheme
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
H : RingHom.FiniteType (RingHom.comp g f)
⊢ RingHom.FiniteType g
[PROOFSTEP]
exact RingHom.FiniteType.of_comp_finiteType H


[GOAL]
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (𝟙 X.toSheafedSpace) x)
[PROOFSTEP]
erw [PresheafedSpace.stalkMap.id]
[GOAL]
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (𝟙 (PresheafedSpace.stalk X.toPresheafedSpace x))
[PROOFSTEP]
apply isLocalRingHom_id
[GOAL]
X✝ : LocallyRingedSpace
X Y Z : LocallyRingedSpace
f : Hom X Y
g : Hom Y Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (f.val ≫ g.val) x)
[PROOFSTEP]
erw [PresheafedSpace.stalkMap.comp]
[GOAL]
X✝ : LocallyRingedSpace
X Y Z : LocallyRingedSpace
f : Hom X Y
g : Hom Y Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap g.val (↑f.val.base x) ≫ PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
exact @isLocalRingHom_comp _ _ _ _ _ _ _ _ (f.2 _) (g.2 _)
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ (𝟙 X ≫ f).val = f.val
[PROOFSTEP]
simp [comp]
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ (f ≫ 𝟙 Y).val = f.val
[PROOFSTEP]
simp [comp]
[GOAL]
X : LocallyRingedSpace
x✝³ x✝² x✝¹ x✝ : LocallyRingedSpace
f : x✝³ ⟶ x✝²
g : x✝² ⟶ x✝¹
h : x✝¹ ⟶ x✝
⊢ ((f ≫ g) ≫ h).val = (f ≫ g ≫ h).val
[PROOFSTEP]
simp [comp]
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X.toSheafedSpace ⟶ Y.toSheafedSpace
inst✝ : IsIso f
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (SheafedSpace.forgetToPresheafedSpace.map f) x)
[PROOFSTEP]
infer_instance
[GOAL]
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ toTopCat X
h : OpenEmbedding ↑f
⊢ ∀ (x : ↑↑(SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace),
    LocalRing ↑(Presheaf.stalk (SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace.presheaf x)
[PROOFSTEP]
intro x
[GOAL]
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ toTopCat X
h : OpenEmbedding ↑f
x : ↑↑(SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace
⊢ LocalRing ↑(Presheaf.stalk (SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace.presheaf x)
[PROOFSTEP]
apply @RingEquiv.localRing _ _ _ (X.localRing (f x))
[GOAL]
case e
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ toTopCat X
h : OpenEmbedding ↑f
x : ↑↑(SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace
⊢ ↑(Presheaf.stalk X.presheaf (↑f x)) ≃+*
    ↑(Presheaf.stalk (SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace.presheaf x)
[PROOFSTEP]
exact (X.restrictStalkIso h x).symm.commRingCatIsoToRingEquiv
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
⊢ (Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s) =
    RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s)
[PROOFSTEP]
ext x
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s)) ↔
    x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s))
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s)) →
    x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s))
[PROOFSTEP]
rintro ⟨⟨y, hyU⟩, hy : IsUnit _, rfl : y = _⟩
[GOAL]
case h.h.mp.intro.mk.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hyU : ↑f.val.base x ∈ U
hy : IsUnit (↑(Presheaf.germ (toRingedSpace Y).toPresheafedSpace.presheaf { val := ↑f.val.base x, property := hyU }) s)
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s))
[PROOFSTEP]
erw [RingedSpace.mem_basicOpen _ _ ⟨x, show x ∈ (Opens.map f.1.base).obj U from hyU⟩, ←
  PresheafedSpace.stalkMap_germ_apply]
[GOAL]
case h.h.mp.intro.mk.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hyU : ↑f.val.base x ∈ U
hy : IsUnit (↑(Presheaf.germ (toRingedSpace Y).toPresheafedSpace.presheaf { val := ↑f.val.base x, property := hyU }) s)
⊢ IsUnit
    (↑(PresheafedSpace.stalkMap f.val ↑{ val := x, property := (_ : x ∈ (Opens.map f.val.base).obj U) })
      (↑(Presheaf.germ Y.presheaf
            { val := ↑f.val.base ↑{ val := x, property := (_ : x ∈ (Opens.map f.val.base).obj U) },
              property :=
                (_ :
                  ↑{ val := x, property := (_ : x ∈ (Opens.map f.val.base).obj U) } ∈ (Opens.map f.val.base).obj U) })
        s))
[PROOFSTEP]
exact (PresheafedSpace.stalkMap f.1 _).isUnit_map hy
[GOAL]
case h.h.mpr
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s)) →
    x ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s))
[PROOFSTEP]
rintro ⟨y, hy : IsUnit _, rfl⟩
[GOAL]
case h.h.mpr.intro.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
y : { x // x ∈ (Opens.map f.val.base).obj U }
hy : IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf y) (↑(NatTrans.app f.val.c (op U)) s))
⊢ ↑y ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s))
[PROOFSTEP]
erw [RingedSpace.mem_basicOpen _ _ ⟨f.1.base y.1, y.2⟩]
[GOAL]
case h.h.mpr.intro.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
y : { x // x ∈ (Opens.map f.val.base).obj U }
hy : IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf y) (↑(NatTrans.app f.val.c (op U)) s))
⊢ IsUnit (↑(Presheaf.germ Y.presheaf { val := ↑f.val.base ↑y, property := (_ : ↑y ∈ (Opens.map f.val.base).obj U) }) s)
[PROOFSTEP]
erw [← PresheafedSpace.stalkMap_germ_apply] at hy
[GOAL]
case h.h.mpr.intro.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
y : { x // x ∈ (Opens.map f.val.base).obj U }
hy :
  IsUnit
    (↑(PresheafedSpace.stalkMap f.val ↑y)
      (↑(Presheaf.germ Y.presheaf { val := ↑f.val.base ↑y, property := (_ : ↑y ∈ (Opens.map f.val.base).obj U) }) s))
⊢ IsUnit (↑(Presheaf.germ Y.presheaf { val := ↑f.val.base ↑y, property := (_ : ↑y ∈ (Opens.map f.val.base).obj U) }) s)
[PROOFSTEP]
exact (isUnit_map_iff (PresheafedSpace.stalkMap f.1 _) _).mp hy
[GOAL]
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ RingedSpace.basicOpen (toRingedSpace X) 0 = ⊥
[PROOFSTEP]
ext x
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) 0) ↔ x ∈ ↑⊥
[PROOFSTEP]
simp only [RingedSpace.basicOpen, Opens.coe_mk, Set.mem_image, Set.mem_setOf_eq, Subtype.exists, exists_and_right,
  exists_eq_right, Opens.coe_bot, Set.mem_empty_iff_false, iff_false, not_exists]
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ ∀ (x_1 : x ∈ U),
    ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
[PROOFSTEP]
intros hx
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
[PROOFSTEP]
rw [map_zero, isUnit_zero_iff]
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1
[PROOFSTEP]
change (0 : X.stalk x) ≠ (1 : X.stalk x)
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ 0 ≠ 1
[PROOFSTEP]
exact zero_ne_one


[GOAL]
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
⊢ IsOpenImmersion f ↔
    OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
⊢ IsOpenImmersion f →
    OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
intro h
[GOAL]
case mp
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
h : IsOpenImmersion f
⊢ OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
exact ⟨h.1, inferInstance⟩
[GOAL]
case mpr
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
⊢ (OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)) →
    IsOpenImmersion f
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mpr.intro
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
h₁ : OpenEmbedding ↑f.val.base
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
⊢ IsOpenImmersion f
[PROOFSTEP]
exact IsOpenImmersion.of_stalk_iso f h₁
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.StableUnderComposition @IsOpenImmersion
[PROOFSTEP]
intro X Y Z f g h₁ h₂
[GOAL]
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h₁ : IsOpenImmersion f
h₂ : IsOpenImmersion g
⊢ IsOpenImmersion (f ≫ g)
[PROOFSTEP]
exact LocallyRingedSpace.IsOpenImmersion.comp f g
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsOpenImmersion
[PROOFSTEP]
apply isOpenImmersion_stableUnderComposition.respectsIso
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (e : X ≅ Y), IsOpenImmersion e.hom
[PROOFSTEP]
intro _ _ _
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
X✝ Y✝ : Scheme
e✝ : X✝ ≅ Y✝
⊢ IsOpenImmersion e✝.hom
[PROOFSTEP]
infer_instance
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ PropertyIsLocalAtTarget @IsOpenImmersion
[PROOFSTEP]
constructor
[GOAL]
case RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsOpenImmersion
[PROOFSTEP]
exact isOpenImmersion_respectsIso
[GOAL]
case restrict
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Opens ↑↑Y.toPresheafedSpace), IsOpenImmersion f → IsOpenImmersion (f ∣_ U)
[PROOFSTEP]
intros
[GOAL]
case restrict
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
U✝ : Opens ↑↑Y✝.toPresheafedSpace
a✝ : IsOpenImmersion f✝
⊢ IsOpenImmersion (f✝ ∣_ U✝)
[PROOFSTEP]
infer_instance
[GOAL]
case of_openCover
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Scheme.OpenCover Y), (∀ (i : 𝒰.J), IsOpenImmersion pullback.snd) → IsOpenImmersion f
[PROOFSTEP]
intro X Y f 𝒰 H
[GOAL]
case of_openCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ IsOpenImmersion f
[PROOFSTEP]
rw [isOpenImmersion_iff_stalk]
[GOAL]
case of_openCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
constructor
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ OpenEmbedding ↑f.val.base
[PROOFSTEP]
apply (openEmbedding_iff_openEmbedding_of_iSup_eq_top 𝒰.iSup_opensRange f.1.base.2).mpr
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ ∀ (i : 𝒰.J),
    OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
intro i
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
i : 𝒰.J
⊢ OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
have := ((isOpenImmersion_respectsIso.arrow_iso_iff (morphismRestrictOpensRange f (𝒰.map i))).mpr (H i)).1
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
i : 𝒰.J
this : OpenEmbedding ↑(Arrow.mk (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i))).hom.val.base
⊢ OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
erw [Arrow.mk_hom, morphismRestrict_val_base] at this
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
i : 𝒰.J
this : OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier ↑f.val.base)
⊢ OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
norm_cast
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
intro x
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
⊢ IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
have := Arrow.iso_w (morphismRestrictStalkMap f (Scheme.Hom.opensRange (𝒰.map <| 𝒰.f <| f.1.base x)) ⟨x, 𝒰.Covers _⟩)
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this :
  (Arrow.mk
        (PresheafedSpace.stalkMap f.val
          ↑{ val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) })).hom =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      (Arrow.mk
            (PresheafedSpace.stalkMap
              (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) })).hom ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
⊢ IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
dsimp only [Arrow.mk_hom] at this
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this :
  PresheafedSpace.stalkMap f.val x =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
⊢ IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
rw [this]
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this :
  PresheafedSpace.stalkMap f.val x =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
⊢ IsIso
    ((morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right)
[PROOFSTEP]
haveI : IsOpenImmersion (f ∣_ Scheme.Hom.opensRange (𝒰.map <| 𝒰.f <| f.1.base x)) :=
  (isOpenImmersion_respectsIso.arrow_iso_iff (morphismRestrictOpensRange f (𝒰.map _))).mpr (H _)
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this✝ :
  PresheafedSpace.stalkMap f.val x =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
this : IsOpenImmersion (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
⊢ IsIso
    ((morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right)
[PROOFSTEP]
infer_instance
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X Y S : Scheme) (f : X ⟶ S) (g : Y ⟶ S), IsOpenImmersion g → IsOpenImmersion pullback.fst
[PROOFSTEP]
intro X Y Z f g H
[GOAL]
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion g
⊢ IsOpenImmersion pullback.fst
[PROOFSTEP]
infer_instance