internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case appDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
f₁✝ A✝ B✝ f₂✝ a₁✝ a₂✝ : VExpr
hf₁ : TY.HasType Γ✝ f₁✝ (forallE A✝ B✝)
a✝³ : TY.HasType Γ✝ f₂✝ (forallE A✝ B✝)
ha₁ : TY.HasType Γ✝ a₁✝ A✝
a✝² : TY.HasType Γ✝ a₂✝ A✝
a✝¹ : NormalEq TY Γ✝ f₁✝ f₂✝
a✝ : NormalEq TY Γ✝ a₁✝ a₂✝
ih1 : TY.IsDefEq Γ✝ f₁✝ f₂✝
ih2 : TY.IsDefEq Γ✝ a₁✝ a₂✝
⊢ TY.IsDefEq Γ✝ (app f₁✝ a₁✝) (app f₂✝ a₂✝)
Tactic:
exact TY.appDF hf₁ ih1 ha₁ ih2
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) body₁✝ body₂✝
⊢ TY.IsDefEq Γ✝ (lam A₁✝ body₁✝) (lam A₂✝ body₂✝)
Tactic:
have ⟨_, hB⟩ := TY.has_type ihB
Proof state after:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) body₁✝ body₂✝
w✝ : VExpr
hB : TY.HasType (A✝ :: Γ✝) body₁✝ w✝
⊢ TY.IsDefEq Γ✝ (lam A₁✝ body₁✝) (lam A₂✝ body₂✝)
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) body₁✝ body₂✝
w✝ : VExpr
hB : TY.HasType (A✝ :: Γ✝) body₁✝ w✝
⊢ TY.IsDefEq Γ✝ (lam A₁✝ body₁✝) (lam A₂✝ body₂✝)
Tactic:
exact TY.trans (TY.symm <| TY.lamDF hA (TY.symm hA₁) (TY.refl hB))
  (TY.lamDF hA (TY.trans (TY.symm hA₁) ihA) ihB)
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case forallEDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ B₁✝ : VExpr
v✝ : VLevel
B₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
hB₁ : TY.HasType (A✝ :: Γ✝) B₁✝ (sort v✝)
a✝ : NormalEq TY (A✝ :: Γ✝) B₁✝ B₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) B₁✝ B₂✝
⊢ TY.IsDefEq Γ✝ (forallE A₁✝ B₁✝) (forallE A₂✝ B₂✝)
Tactic:
exact TY.trans (TY.symm <| TY.forallEDF hA (TY.symm hA₁) hB₁ (TY.refl hB₁))
  (TY.forallEDF hA (TY.trans (TY.symm hA₁) ihA) hB₁ ihB)
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Tactic:
have ⟨_, AB⟩ := TY.is_type h1
Proof state after:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Tactic:
have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
Proof state after:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Tactic:
exact TY.trans (TY.lamDF hA (TY.refl hA) ih) (TY.eta h1)
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Tactic:
have ⟨_, AB⟩ := TY.is_type h1
Proof state after:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Tactic:
have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
Proof state after:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Tactic:
exact TY.trans (TY.symm (TY.eta h1)) (TY.lamDF hA (TY.refl hA) ih)
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case proofIrrel
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
h1 : TY.HasType Γ✝ p✝ (sort VLevel.zero)
h2 : TY.HasType Γ✝ h✝ p✝
h3 : TY.HasType Γ✝ h'✝ p✝
⊢ TY.IsDefEq Γ✝ h✝ h'✝
Tactic:
exact TY.proofIrrel h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
H : NormalEq TY Γ e1 e2
⊢ NormalEq TY Γ e2 e1
Tactic:
induction H with
| refl h => exact .refl h
| sortDF h1 h2 h3 => exact .sortDF h2 h1 h3.symm
| appDF h1 h2 h3 h4 _ _ ih1 ih2 => exact .appDF h2 h1 h4 h3 ih1 ih2
| lamDF h1 h2 _ _ ih1 ih2 => exact .lamDF h1 (TY.trans ih1.defeq h2) ih1 ih2
| forallEDF h1 h2 _ h4 h5 ih1 ih2 =>
  exact .forallEDF h1 (TY.trans ih1.defeq h2) ih1 (TY.defeq_l h5.defeq h4) ih2
| etaL h1 _ ih => exact .etaR h1 ih
| etaR h1 _ ih => exact .etaL h1 ih
| proofIrrel h1 h2 h3 => exact .proofIrrel h1 h3 h2
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case refl
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
e✝ A✝ : VExpr
h : TY.HasType Γ✝ e✝ A✝
⊢ NormalEq TY Γ✝ e✝ e✝
Tactic:
exact .refl h
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case sortDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
l₁✝ l₂✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF TY.univs l₁✝
h2 : VLevel.WF TY.univs l₂✝
h3 : l₁✝ ≈ l₂✝
⊢ NormalEq TY Γ✝ (sort l₂✝) (sort l₁✝)
Tactic:
exact .sortDF h2 h1 h3.symm
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case appDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
f₁✝ A✝ B✝ f₂✝ a₁✝ a₂✝ : VExpr
h1 : TY.HasType Γ✝ f₁✝ (forallE A✝ B✝)
h2 : TY.HasType Γ✝ f₂✝ (forallE A✝ B✝)
h3 : TY.HasType Γ✝ a₁✝ A✝
h4 : TY.HasType Γ✝ a₂✝ A✝
a✝¹ : NormalEq TY Γ✝ f₁✝ f₂✝
a✝ : NormalEq TY Γ✝ a₁✝ a₂✝
ih1 : NormalEq TY Γ✝ f₂✝ f₁✝
ih2 : NormalEq TY Γ✝ a₂✝ a₁✝
⊢ NormalEq TY Γ✝ (app f₂✝ a₂✝) (app f₁✝ a₁✝)
Tactic:
exact .appDF h2 h1 h4 h3 ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
h1 : TY.HasType Γ✝ A✝ (sort u✝)
h2 : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ih1 : NormalEq TY Γ✝ A₂✝ A₁✝
ih2 : NormalEq TY (A✝ :: Γ✝) body₂✝ body₁✝
⊢ NormalEq TY Γ✝ (lam A₂✝ body₂✝) (lam A₁✝ body₁✝)
Tactic:
exact .lamDF h1 (TY.trans ih1.defeq h2) ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case forallEDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ B₁✝ : VExpr
v✝ : VLevel
B₂✝ : VExpr
h1 : TY.HasType Γ✝ A✝ (sort u✝)
h2 : TY.IsDefEq Γ✝ A₁✝ A✝
a✝ : NormalEq TY Γ✝ A₁✝ A₂✝
h4 : TY.HasType (A✝ :: Γ✝) B₁✝ (sort v✝)
h5 : NormalEq TY (A✝ :: Γ✝) B₁✝ B₂✝
ih1 : NormalEq TY Γ✝ A₂✝ A₁✝
ih2 : NormalEq TY (A✝ :: Γ✝) B₂✝ B₁✝
⊢ NormalEq TY Γ✝ (forallE A₂✝ B₂✝) (forallE A₁✝ B₁✝)
Tactic:
exact .forallEDF h1 (TY.trans ih1.defeq h2) ih1 (TY.defeq_l h5.defeq h4) ih2
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
⊢ NormalEq TY Γ✝ e'✝ (lam A✝ e✝)
Tactic:
exact .etaR h1 ih
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
⊢ NormalEq TY Γ✝ (lam A✝ e✝) e'✝
Tactic:
exact .etaL h1 ih
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.symm
Proof state before:
case proofIrrel
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
h1 : TY.HasType Γ✝ p✝ (sort VLevel.zero)
h2 : TY.HasType Γ✝ h✝ p✝
h3 : TY.HasType Γ✝ h'✝ p✝
⊢ NormalEq TY Γ✝ h'✝ h✝
Tactic:
exact .proofIrrel h1 h3 h2
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.trans
Proof state before:
TY : Typing
Γ : List VExpr
e1 e2 e3 : VExpr
H1 : NormalEq TY Γ e1 e2
H2 : NormalEq TY Γ e2 e3
⊢ NormalEq TY Γ e1 e3
Tactic:
sorry
Proof state after:
no goals
Theorem: List.nodupKeys_cons
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
a : α✝ × β✝
l : List (α✝ × β✝)
⊢ NodupKeys (a :: l) ↔ (∀ (a' : α✝ × β✝), a' ∈ l → a.fst ≠ a'.fst) ∧ NodupKeys l
Tactic:
simp [nodupKeys_iff_pairwise]
Proof state after:
no goals
Theorem: List.Perm.lookup_eq
Proof state before:
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
h : l₁ ~ l₂
nd : NodupKeys l₁
⊢ lookup a l₁ = lookup a l₂
Tactic:
induction h with
| nil => rfl
| cons _ _ ih => simp [lookup]; split <;> [rfl; exact ih (pairwise_cons.1 nd).2]
| swap _ h ih =>
  simp at nd
  simp [lookup]; split <;> split <;> rename_i h1 _ h2 <;> try rfl
  simp at h1 h2; cases nd.1.1 (by rw [← h1, h2])
| trans h1 _ ih1 ih2 => exact (ih1 nd).trans (ih2 (h1.nodupKeys_iff.1 nd))
Proof state after:
no goals
Theorem: List.Perm.lookup_eq
Proof state before:
case nil
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
nd : NodupKeys []
⊢ lookup a [] = lookup a []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Perm.lookup_eq
Proof state before:
case cons
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ : α × β
l₁✝ l₂✝ : List (α × β)
a✝ : l₁✝ ~ l₂✝
ih : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
nd : NodupKeys (x✝ :: l₁✝)
⊢ lookup a (x✝ :: l₁✝) = lookup a (x✝ :: l₂✝)
Tactic:
simp [lookup]
Proof state after:
case cons
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ : α × β
l₁✝ l₂✝ : List (α × β)
a✝ : l₁✝ ~ l₂✝
ih : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
nd : NodupKeys (x✝ :: l₁✝)
⊢ (match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₁✝) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₂✝
Theorem: List.Perm.lookup_eq
Proof state before:
case cons
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ : α × β
l₁✝ l₂✝ : List (α × β)
a✝ : l₁✝ ~ l₂✝
ih : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
nd : NodupKeys (x✝ :: l₁✝)
⊢ (match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₁✝) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₂✝
Tactic:
split <;> [rfl; exact ih (pairwise_cons.1 nd).2]
Proof state after:
no goals
Theorem: List.Perm.lookup_eq
Proof state before:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd : NodupKeys (h :: x✝ :: ih)
⊢ lookup a (h :: x✝ :: ih) = lookup a (x✝ :: h :: ih)
Tactic:
simp at nd
Proof state after:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ lookup a (h :: x✝ :: ih) = lookup a (x✝ :: h :: ih)
Theorem: List.Perm.lookup_eq
Proof state before:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ lookup a (h :: x✝ :: ih) = lookup a (x✝ :: h :: ih)
Tactic:
simp [lookup]
Proof state after:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ (match a == h.fst with
    | true => some h.snd
    | false =>
      match a == x✝.fst with
      | true => some x✝.snd
      | false => lookup a ih) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false =>
      match a == h.fst with
      | true => some h.snd
      | false => lookup a ih
Theorem: List.Perm.lookup_eq
Proof state before:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ (match a == h.fst with
    | true => some h.snd
    | false =>
      match a == x✝.fst with
      | true => some x✝.snd
      | false => lookup a ih) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false =>
      match a == h.fst with
      | true => some h.snd
      | false => lookup a ih
Tactic:
split <;> split <;> rename_i h1 _ h2 <;> try rfl
Proof state after:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ : Bool
h1 : (a == h.fst) = true
x✝ : Bool
h2 : (a == x✝².fst) = true
⊢ some h.snd = some x✝².snd
Theorem: List.Perm.lookup_eq
Proof state before:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ : Bool
h1 : (a == h.fst) = true
x✝ : Bool
h2 : (a == x✝².fst) = true
⊢ some h.snd = some x✝².snd
Tactic:
simp at h1 h2
Proof state after:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ x✝ : Bool
h1 : a = h.fst
h2 : a = x✝².fst
⊢ some h.snd = some x✝².snd
Theorem: List.Perm.lookup_eq
Proof state before:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ x✝ : Bool
h1 : a = h.fst
h2 : a = x✝².fst
⊢ some h.snd = some x✝².snd
Tactic:
cases nd.1.1 (by rw [← h1, h2])
Proof state after:
no goals
Theorem: List.Perm.lookup_eq
Proof state before:
case swap.h_2.h_2
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ : Bool
h1 : (a == h.fst) = false
x✝ : Bool
h2 : (a == x✝².fst) = false
⊢ lookup a ih = lookup a ih
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Perm.lookup_eq
Proof state before:
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ x✝ : Bool
h1 : a = h.fst
h2 : a = x✝².fst
⊢ h.fst = x✝².fst
Tactic:
rw [← h1, h2]
Proof state after:
no goals
Theorem: List.Perm.lookup_eq
Proof state before:
case trans
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
l₁✝ l₂✝ l₃✝ : List (α × β)
h1 : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
ih2 : NodupKeys l₂✝ → lookup a l₂✝ = lookup a l₃✝
nd : NodupKeys l₁✝
⊢ lookup a l₁✝ = lookup a l₃✝
Tactic:
exact (ih1 nd).trans (ih2 (h1.nodupKeys_iff.1 nd))
Proof state after:
no goals
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case nil
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
nd : NodupKeys []
⊢ lookup a [] = some b ↔ (a, b) ∈ []
Tactic:
simp
Proof state after:
no goals
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
nd : NodupKeys (p :: l)
⊢ lookup a (p :: l) = some b ↔ (a, b) ∈ p :: l
Tactic:
let (a', b') := p
Proof state after:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : NodupKeys ((a', b') :: l)
⊢ lookup a ((a', b') :: l) = some b ↔ (a, b) ∈ (a', b') :: l
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : NodupKeys ((a', b') :: l)
⊢ lookup a ((a', b') :: l) = some b ↔ (a, b) ∈ (a', b') :: l
Tactic:
simp [lookup] at nd ⊢
Proof state after:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
⊢ (match a == a' with
      | true => some b'
      | false => lookup a l) =
      some b ↔
    a = a' ∧ b = b' ∨ (a, b) ∈ l
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
⊢ (match a == a' with
      | true => some b'
      | false => lookup a l) =
      some b ↔
    a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
split <;> rename_i h
Proof state after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = true
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l

case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = false
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = true
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp at h
Proof state after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : a = a'
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : a = a'
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
subst a'
Proof state after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ some b' = some b ↔ a = a ∧ b = b' ∨ (a, b) ∈ l
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ some b' = some b ↔ a = a ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp [eq_comm]
Proof state after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ b = b' ↔ b = b' ∨ (a, b) ∈ l