internlm/Lean-Github huggingface dataset:
Theorem: Prod.Lex.mk_fst_mono_iff
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x : α
y₁ y₂ : β
⊢ (x, y₁) ≤ (x, y₂) ↔ y₁ ≤ y₂
Tactic:
simp [le_iff']
Proof state after:
no goals
Theorem: Prod.Lex.mk_fst_mono_lt_iff
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x : α
y₁ y₂ : β
⊢ (x, y₁) < (x, y₂) ↔ y₁ < y₂
Tactic:
simp [lt_iff']
Proof state after:
no goals
Theorem: Prod.Lex.mk_snd_mono_le_iff
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x₁ x₂ : α
y : β
⊢ (x₁, y) ≤ (x₂, y) ↔ x₁ ≤ x₂
Tactic:
simp [le_iff'']
Proof state after:
no goals
Theorem: Prod.Lex.mk_snd_mono_lt_iff
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x₁ x₂ : α
y : β
⊢ (x₁, y) < (x₂, y) ↔ x₁ < x₂
Tactic:
simp [lt_iff']
Proof state after:
no goals
Theorem: Prod.Lex.mk_false_lt_mk_true_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type ?u.49210
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝ : PartialOrder α
x₁ x₂ : α
⊢ (x₁, false) < (x₂, true) ↔ x₁ ≤ x₂
Tactic:
simp [lt_iff', le_iff_lt_or_eq]
Proof state after:
no goals
Theorem: Prod.Lex.mk_true_le_mk_false_iff_lt
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type ?u.50081
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝ : PartialOrder α
x y : α
⊢ (x, true) ≤ (y, false) ↔ x < y
Tactic:
simp [le_iff']
Proof state after:
no goals
Theorem: Prod.Lex.mk_true_lt_iff_lt
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type ?u.51649
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝ : PartialOrder α
x : α
y : Lex (α × Bool)
⊢ (x, true) < y ↔ x < y.1
Tactic:
simp [lt_iff']
Proof state after:
no goals
Theorem: Prod.Lex.lt_mk_true_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type ?u.53384
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝ : PartialOrder α
x : Lex (α × Bool)
y : α
⊢ x < (y, true) ↔ x ≤ (y, false)
Tactic:
simp [lt_iff', le_iff']
Proof state after:
no goals
Theorem: Prod.Lex.mk_min
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
x : α
y₁✝ y₂✝ y₁ y₂ : β
⊢ y₁ ≤ y₂ → (fun y => (x, y)) y₁ ≤ (fun y => (x, y)) y₂
Tactic:
simp
Proof state after:
no goals
Theorem: max_le_min_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ max x y ≤ min x y ↔ x = y
Tactic:
have h : max x y ≤ min x y ↔ y = x := by simpa using le_antisymm_iff.symm
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : max x y ≤ min x y ↔ y = x
⊢ max x y ≤ min x y ↔ x = y
Theorem: max_le_min_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : max x y ≤ min x y ↔ y = x
⊢ max x y ≤ min x y ↔ x = y
Tactic:
exact h.trans eq_comm
Proof state after:
no goals
Theorem: max_le_min_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ max x y ≤ min x y ↔ y = x
Tactic:
simpa using le_antisymm_iff.symm
Proof state after:
no goals
Theorem: max_eq_min_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x = y
⊢ min x y = max x y
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Finsupp.mul_eq_zero_of_disjoint_support
Proof state before:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ f * g = 0
Tactic:
rw [← Finsupp.support_eq_empty, ← Finset.subset_empty]
Proof state after:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ (f * g).support ⊆ ∅
Theorem: Finsupp.mul_eq_zero_of_disjoint_support
Proof state before:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ (f * g).support ⊆ ∅
Tactic:
refine Finsupp.support_mul.trans ?_
Proof state after:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ f.support ∩ g.support ⊆ ∅
Theorem: Finsupp.mul_eq_zero_of_disjoint_support
Proof state before:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ f.support ∩ g.support ⊆ ∅
Tactic:
rwa [Finset.subset_empty, ← Finset.disjoint_iff_inter_eq_empty]
Proof state after:
no goals
Theorem: Finsupp.mul_single_eq_zero
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ single i₁ x * single i₂ y = 0
Tactic:
classical
rw [Finsupp.mul_eq_zero_of_disjoint_support]
simp_rw [Finset.disjoint_iff_ne, Finsupp.mem_support_single]
simp_rw [and_imp, forall_eq]
intros
exact hi
Proof state after:
no goals
Theorem: Finsupp.mul_single_eq_zero
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ single i₁ x * single i₂ y = 0
Tactic:
rw [Finsupp.mul_eq_zero_of_disjoint_support]
Proof state after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ Disjoint (single i₁ x).support (single i₂ y).support
Theorem: Finsupp.mul_single_eq_zero
Proof state before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ Disjoint (single i₁ x).support (single i₂ y).support
Tactic:
simp_rw [Finset.disjoint_iff_ne, Finsupp.mem_support_single]
Proof state after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ ∀ (a : ι), a = i₁ ∧ x ≠ 0 → ∀ (b : ι), b = i₂ ∧ y ≠ 0 → a ≠ b
Theorem: Finsupp.mul_single_eq_zero
Proof state before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ ∀ (a : ι), a = i₁ ∧ x ≠ 0 → ∀ (b : ι), b = i₂ ∧ y ≠ 0 → a ≠ b
Tactic:
simp_rw [and_imp, forall_eq]
Proof state after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ x ≠ 0 → y ≠ 0 → i₁ ≠ i₂
Theorem: Finsupp.mul_single_eq_zero
Proof state before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ x ≠ 0 → y ≠ 0 → i₁ ≠ i₂
Tactic:
intros
Proof state after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
a✝¹ : x ≠ 0
a✝ : y ≠ 0
⊢ i₁ ≠ i₂
Theorem: Finsupp.mul_single_eq_zero
Proof state before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
a✝¹ : x ≠ 0
a✝ : y ≠ 0
⊢ i₁ ≠ i₂
Tactic:
exact hi
Proof state after:
no goals
Theorem: Finsupp.mul_filter
Proof state before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
⊢ filter P f * filter Q g = filter (fun i => P i ∧ Q i) (f * g)
Tactic:
ext i
Proof state after:
case h
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
i : ι
⊢ (filter P f * filter Q g) i = (filter (fun i => P i ∧ Q i) (f * g)) i
Theorem: Finsupp.mul_filter
Proof state before:
case h
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
i : ι
⊢ (filter P f * filter Q g) i = (filter (fun i => P i ∧ Q i) (f * g)) i
Tactic:
by_cases h₁ : P i <;> by_cases h₂ : Q i <;> simp [h₁, h₂]
Proof state after:
no goals
Theorem: Finsupp.mul_filter'
Proof state before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
⊢ filter P (f * g) = filter P f * filter P g
Tactic:
simp [Finsupp.mul_filter]
Proof state after:
no goals
Theorem: mul_eq_zero_of
Proof state before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : x = 0
⊢ x * y = 0
Tactic:
rw [h]
Proof state after:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : x = 0
⊢ 0 * y = 0
Theorem: mul_eq_zero_of
Proof state before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : x = 0
⊢ 0 * y = 0
Tactic:
exact MulZeroClass.zero_mul y
Proof state after:
no goals
Theorem: mul_eq_zero_of
Proof state before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : y = 0
⊢ x * y = 0
Tactic:
rw [h]
Proof state after:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : y = 0
⊢ x * 0 = 0
Theorem: mul_eq_zero_of
Proof state before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : y = 0
⊢ x * 0 = 0
Tactic:
exact MulZeroClass.mul_zero x
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul.ready.order_eq
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // valid a b p = true }
h : ready a b q = true
⊢ toOrder a (valid.fst q) = toOrder b (valid.snd q)
Tactic:
dsimp only [Stream.toOrder]
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // valid a b p = true }
h : ready a b q = true
⊢ (a.index (valid.fst q), a.ready (valid.fst q)) = (b.index (valid.snd q), b.ready (valid.snd q))
Theorem: Etch.Verification.Stream.mul.ready.order_eq
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // valid a b p = true }
h : ready a b q = true
⊢ (a.index (valid.fst q), a.ready (valid.fst q)) = (b.index (valid.snd q), b.ready (valid.snd q))
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.order_eq_of_mul_ready
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
Tactic:
dsimp only [Stream.toOrder]
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ (a.index (mul.valid.fst q), a.ready (mul.valid.fst q)) = ((mul a b).index q, (mul a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((mul a b).index q, (mul a b).ready q)
Theorem: Etch.Verification.Stream.order_eq_of_mul_ready
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ (a.index (mul.valid.fst q), a.ready (mul.valid.fst q)) = ((mul a b).index q, (mul a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((mul a b).index q, (mul a b).ready q)
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.Stream.mul_index'
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
⊢ index' (mul a b) q = max (index' a q.1) (index' b q.2)
Tactic:
rw [Stream.index']
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
⊢ (if h : (mul a b).valid q = true then ↑((mul a b).index { val := q, property := h }) else ⊤) =
    max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.Stream.mul_index'
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
⊢ (if h : (mul a b).valid q = true then ↑((mul a b).index { val := q, property := h }) else ⊤) =
    max (index' a q.1) (index' b q.2)
Tactic:
split_ifs with h
Proof state after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : (mul a b).valid q = true
⊢ ↑((mul a b).index { val := q, property := h }) = max (index' a q.1) (index' b q.2)

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : ¬(mul a b).valid q = true
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.Stream.mul_index'
Proof state before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : (mul a b).valid q = true
⊢ ↑((mul a b).index { val := q, property := h }) = max (index' a q.1) (index' b q.2)
Tactic:
simp at h
Proof state after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ ↑((mul a b).index { val := q, property := h✝ }) = max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.Stream.mul_index'
Proof state before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ ↑((mul a b).index { val := q, property := h✝ }) = max (index' a q.1) (index' b q.2)
Tactic:
simp [index'_val' _ h.1, index'_val' _ h.2]
Proof state after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ max ↑(a.index (mul.valid.fst { val := q, property := h✝ })) ↑(b.index (mul.valid.snd { val := q, property := h✝ })) =
    max ↑(a.index { val := q.1, property := ⋯ }) ↑(b.index { val := q.2, property := ⋯ })
Theorem: Etch.Verification.Stream.Stream.mul_index'
Proof state before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ max ↑(a.index (mul.valid.fst { val := q, property := h✝ })) ↑(b.index (mul.valid.snd { val := q, property := h✝ })) =
    max ↑(a.index { val := q.1, property := ⋯ }) ↑(b.index { val := q.2, property := ⋯ })
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.Stream.mul_index'
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : ¬(mul a b).valid q = true
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Tactic:
simp [-not_and, not_and_or] at h
Proof state after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.Stream.mul_index'
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Tactic:
rcases h with h | h
<;> simp [index'_invalid h]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q)) ≤ toOrder (mul a b) q
Tactic:
rw [Prod.Lex.le_iff'']
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ≤ (toOrder (mul a b) q).1 ∧
    ((min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 = (toOrder (mul a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (mul a b) q).2)
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ≤ (toOrder (mul a b) q).1 ∧
    ((min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 = (toOrder (mul a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (mul a b) q).2)
Tactic:
simp only [Monotone.map_min (@Prod.Lex.fst_mono ι Bool _ _)]
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (mul a b) q).1 ∧
    (min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (mul a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (mul a b) q).2)
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (mul a b) q).1 ∧
    (min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (mul a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (mul a b) q).2)
Tactic:
constructor
Proof state after:
case left
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (mul a b) q).1

case right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (mul a b) q).1 →
    (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (mul a b) q).2
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
case left
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (mul a b) q).1
Tactic:
exact min_le_max
Proof state after:
no goals
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
case right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (mul a b) q).1 →
    (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (mul a b) q).2
Tactic:
simp only [toOrder]
Proof state after:
case right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (a.index (mul.valid.fst q)) (b.index (mul.valid.snd q)) = (mul a b).index q →
    (min (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 ≤
      (mul a b).ready q
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
case right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
⊢ min (a.index (mul.valid.fst q)) (b.index (mul.valid.snd q)) = (mul a b).index q →
    (min (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 ≤
      (mul a b).ready q
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ toOrder (mul a b) q ≤ max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))
Tactic:
rw [Prod.Lex.le_iff']
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 < (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∨
    (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
      (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 < (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∨
    (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
      (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
right
Proof state after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
    (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
    (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
constructor
Proof state after:
case h.left
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1

case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h.left
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1
Tactic:
simp [Monotone.map_max (@Prod.Lex.fst_mono ι Bool _ _)]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
simp only [Bool.le_iff_imp, toOrder]
Proof state after:
case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (mul a b).ready q = true →
    (max (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 =
      true
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (mul a b).ready q = true →
    (max (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 =
      true
Tactic:
aesop
Proof state after:
no goals