internlm/Lean-Github huggingface dataset:
Theorem: ContDiff.orderedIteratedPiDeriv_right
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : (ι → 𝕜) → F
f' : (ι → 𝕜) → FormalMultilinearSeries 𝕜 (ι → 𝕜) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
⊢ ContDiff 𝕜 m (orderedIteratedPiDeriv js f)
Tactic:
have hfn : ContDiff 𝕜 n f := hf.of_le (le_trans (by simp) hn)
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : (ι → 𝕜) → F
f' : (ι → 𝕜) → FormalMultilinearSeries 𝕜 (ι → 𝕜) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
hfn : ContDiff 𝕜 (↑n) f
⊢ ContDiff 𝕜 m (orderedIteratedPiDeriv js f)
Theorem: ContDiff.orderedIteratedPiDeriv_right
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : (ι → 𝕜) → F
f' : (ι → 𝕜) → FormalMultilinearSeries 𝕜 (ι → 𝕜) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
hfn : ContDiff 𝕜 (↑n) f
⊢ ContDiff 𝕜 m (orderedIteratedPiDeriv js f)
Tactic:
conv => arg 3; intro x; rw [ContDiff.orderedIteratedPiDeriv_eq_iteratedFDeriv_apply hfn]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : (ι → 𝕜) → F
f' : (ι → 𝕜) → FormalMultilinearSeries 𝕜 (ι → 𝕜) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
hfn : ContDiff 𝕜 (↑n) f
⊢ ContDiff 𝕜 m fun x => (iteratedFDeriv 𝕜 n f x) fun i => Pi.single (js i) 1
Theorem: ContDiff.orderedIteratedPiDeriv_right
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : (ι → 𝕜) → F
f' : (ι → 𝕜) → FormalMultilinearSeries 𝕜 (ι → 𝕜) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
hfn : ContDiff 𝕜 (↑n) f
⊢ ContDiff 𝕜 m fun x => (iteratedFDeriv 𝕜 n f x) fun i => Pi.single (js i) 1
Tactic:
exact continuousMultilinear_apply_const (hf.iteratedFDeriv_right hn)
Proof state after:
no goals
Theorem: ContDiff.orderedIteratedPiDeriv_right
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : (ι → 𝕜) → F
f' : (ι → 𝕜) → FormalMultilinearSeries 𝕜 (ι → 𝕜) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
⊢ ↑n ≤ m + ↑n
Tactic:
simp
Proof state after:
no goals
Theorem: BEq.comm
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (x == y) = (y == x)
Tactic:
match hxy : x == y, hyx : y == x with
| true, true => rfl
| true, false => rw [BEq.symm hxy] at hyx; contradiction
| false, true => rw [BEq.symm hyx] at hxy; contradiction
| false, false => rfl
Proof state after:
no goals
Theorem: BEq.comm
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : (y == x) = true
⊢ true = true
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.comm
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : (y == x) = false
⊢ true = false
Tactic:
rw [BEq.symm hxy] at hyx
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : true = false
⊢ true = false
Theorem: BEq.comm
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : true = false
⊢ true = false
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.comm
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = false
hyx : (y == x) = true
⊢ false = true
Tactic:
rw [BEq.symm hyx] at hxy
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : true = false
hyx : (y == x) = true
⊢ false = true
Theorem: BEq.comm
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : true = false
hyx : (y == x) = true
⊢ false = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.comm
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = false
hyx : (y == x) = false
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
⊢ (x == y) = true → (x == z) = (y == z)
Tactic:
intro hxy
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
⊢ (x == z) = (y == z)
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
⊢ (x == z) = (y == z)
Tactic:
match hxz : x == z, hyz : y == z with
| true, true => rfl
| true, false => rw [BEq.trans (BEq.symm hxy) hxz] at hyz; contradiction
| false, true => rw [BEq.trans hxy hyz] at hxz; contradiction
| false, false => rfl
Proof state after:
no goals
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : (y == z) = true
⊢ true = true
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : (y == z) = false
⊢ true = false
Tactic:
rw [BEq.trans (BEq.symm hxy) hxz] at hyz
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : true = false
⊢ true = false
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : true = false
⊢ true = false
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = false
hyz : (y == z) = true
⊢ false = true
Tactic:
rw [BEq.trans hxy hyz] at hxz
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : true = false
hyz : (y == z) = true
⊢ false = true
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : true = false
hyz : (y == z) = true
⊢ false = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.subst_left
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = false
hyz : (y == z) = false
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
⊢ (x == y) = true → (z == x) = (z == y)
Tactic:
intro hxy
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
⊢ (z == x) = (z == y)
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
⊢ (z == x) = (z == y)
Tactic:
match hzx : z == x, hzy : z == y with
| true, true => rfl
| true, false => rw [BEq.trans hzx hxy] at hzy; contradiction
| false, true => rw [BEq.trans hzy (BEq.symm hxy)] at hzx; contradiction
| false, false => rfl
Proof state after:
no goals
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = true
hzy : (z == y) = true
⊢ true = true
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = true
hzy : (z == y) = false
⊢ true = false
Tactic:
rw [BEq.trans hzx hxy] at hzy
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = true
hzy : true = false
⊢ true = false
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = true
hzy : true = false
⊢ true = false
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = false
hzy : (z == y) = true
⊢ false = true
Tactic:
rw [BEq.trans hzy (BEq.symm hxy)] at hzx
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : true = false
hzy : (z == y) = true
⊢ false = true
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : true = false
hzy : (z == y) = true
⊢ false = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.subst_right
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = false
hzy : (z == y) = false
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.ne_of_bne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
⊢ (x != y) = true → x ≠ y
Tactic:
intro | h, rfl => rw [bne, BEq.refl] at h; contradiction
Proof state after:
no goals
Theorem: BEq.ne_of_bne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
x✝¹ : (x != y) = true
x✝ : x = y
h : (x != x) = true
⊢ False
Tactic:
rw [bne, BEq.refl] at h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
x✝¹ : (x != y) = true
x✝ : x = y
h : (!true) = true
⊢ False
Theorem: BEq.ne_of_bne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
x✝¹ : (x != y) = true
x✝ : x = y
h : (!true) = true
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.bne_of_ne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
⊢ x ≠ y → (x != y) = true
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x != y) = true
Theorem: BEq.bne_of_ne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x != y) = true
Tactic:
rw [bne, Bool.not_eq_true']
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x == y) = false
Theorem: BEq.bne_of_ne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x == y) = false
Tactic:
match hb : x == y with
| true => absurd h; exact BEq.eq_of_beq hb
| false => rfl
Proof state after:
no goals
Theorem: BEq.bne_of_ne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ true = false
Tactic:
absurd h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ x = y
Theorem: BEq.bne_of_ne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ x = y
Tactic:
exact BEq.eq_of_beq hb
Proof state after:
no goals
Theorem: BEq.bne_of_ne
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = false
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (x != y) = true → ∀ (z : α), (x != z) = true ∨ (z != y) = true
Tactic:
unfold bne
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (!x == y) = true → ∀ (z : α), (!x == z) = true ∨ (!z == y) = true
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (!x == y) = true → ∀ (z : α), (!x == z) = true ∨ (!z == y) = true
Tactic:
intro hxy z
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
⊢ (!x == z) = true ∨ (!z == y) = true
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
⊢ (!x == z) = true ∨ (!z == y) = true
Tactic:
match hxz : x == z, hyz : z == y with
| true, true => rw [BEq.subst_right hyz] at hxz; rw [hxz] at hxy; contradiction
| false, _ => left; rfl
| _, false => right; rfl
Proof state after:
no goals
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
hxz : (x == z) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Tactic:
rw [BEq.subst_right hyz] at hxz
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Tactic:
rw [hxz] at hxy
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!true) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!true) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true ∨ (!x✝) = true
Tactic:
left
Proof state after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true
Theorem: BEq.comp
Proof state before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: BEq.comp
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = x✝
hyz : (z == y) = false
⊢ (!x✝) = true ∨ (!false) = true
Tactic:
right
Proof state after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = x✝
hyz : (z == y) = false
⊢ (!false) = true
Theorem: BEq.comp
Proof state before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = x✝
hyz : (z == y) = false
⊢ (!false) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
case nil
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs : List α
i : [].Index
⊢ Setoid.r i.val (dedup s i).val
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
⊢ Setoid.r head.val (dedup s head).val
Tactic:
unfold dedup
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
⊢ Setoid.r head.val
    (if h : Logic.Any (List.map (Setoid.r x) xs) then
        let_fun this := ⋯;
        ⋯ ▸ dedup s (unmap (Setoid.r x) h.get)
      else
        let_fun this := ⋯;
        ⋯ ▸ head).val
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
⊢ Setoid.r head.val
    (if h : Logic.Any (List.map (Setoid.r x) xs) then
        let_fun this := ⋯;
        ⋯ ▸ dedup s (unmap (Setoid.r x) h.get)
      else
        let_fun this := ⋯;
        ⋯ ▸ head).val
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ dedup s (unmap (Setoid.r x) h✝.get)).val

case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ head).val
Theorem: List.Index.val_dedup
Proof state before:
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ head).val
Tactic:
next => rw [val_ndrec]; reflexivity using s.r
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ dedup s (unmap (Setoid.r x) h.get)).val
Tactic:
rw [val_ndrec]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val (dedup s (unmap (Setoid.r x) h.get)).val
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val (dedup s (unmap (Setoid.r x) h.get)).val
Tactic:
transitivity (h.get.unmap (s.r x)).val using s.r
Proof state after:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val (unmap (Setoid.r x) h.get).val

case right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) h.get).val (dedup s (unmap (Setoid.r x) h.get)).val
Theorem: List.Index.val_dedup
Proof state before:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val (unmap (Setoid.r x) h.get).val
Tactic:
rw [val_head, ←val_unmap (s.r x)]
Proof state after:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ h.get.val
Theorem: List.Index.val_dedup
Proof state before:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ h.get.val
Tactic:
exact Logic.Any.get_prop ..
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
case right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) h.get).val (dedup s (unmap (Setoid.r x) h.get)).val
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ head).val
Tactic:
rw [val_ndrec]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val head.val
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val head.val
Tactic:
reflexivity using s.r
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
⊢ Setoid.r i.tail.val (dedup s i.tail).val
Tactic:
unfold dedup
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
⊢ Setoid.r i.tail.val
    (if h : Logic.Any (List.map (Setoid.r x) xs) then
        let_fun this := ⋯;
        ⋯ ▸ dedup s i
      else
        let_fun this := ⋯;
        ⋯ ▸ (dedup s i).tail).val
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
⊢ Setoid.r i.tail.val
    (if h : Logic.Any (List.map (Setoid.r x) xs) then
        let_fun this := ⋯;
        ⋯ ▸ dedup s i
      else
        let_fun this := ⋯;
        ⋯ ▸ (dedup s i).tail).val
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ dedup s i).val

case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ (dedup s i).tail).val