internlm/Lean-Github huggingface dataset:
Theorem: exercise1_4
Proof state before:
a b : ℝ
⊢ (a + b) * (a - b) = a ^ 2 - b ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: C06S01.Point.add_comm
Proof state before:
a b : Point
⊢ add a b = add b a
Tactic:
rw [add, add]
Proof state after:
a b : Point
⊢ { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z } = { x := b.x + a.x, y := b.y + a.y, z := b.z + a.z }
Theorem: C06S01.Point.addAlt_x
Proof state before:
a b : Point
⊢ (addAlt a b).x = a.x + b.x
Tactic:
rfl
Proof state after:
no goals
Theorem: C06S01.Point.addAlt_comm
Proof state before:
a b : Point
⊢ addAlt a b = addAlt b a
Tactic:
rw [addAlt, addAlt]
Proof state after:
a b : Point
⊢ (match a, b with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }) =
    match b, a with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }
Theorem: C06S01.Point.add_assoc
Proof state before:
a b c : Point
⊢ add (add a b) c = add a (add b c)
Tactic:
sorry
Proof state after:
no goals
Theorem: C06S01.Point.smul_distrib
Proof state before:
r : ℝ
a b : Point
⊢ add (smul r a) (smul r b) = smul r (add a b)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_1
Proof state before:
p : Prop
⊢ p ∨ ¬p
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_2
Proof state before:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
⊢ SequentialLimit (s ∘ r) a
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_3
Proof state before:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
⊢ SequentialLimit s₂ a
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_4
Proof state before:
⊢ SequentialLimit (fun n => 1 / (↑n + 1)) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: use_me
Proof state before:
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Tactic:
have : SequentialLimit (fun n ↦ (-1) * (1 / (n+1))) (-1 * 0) :=
  convergesTo_mul_const (-1) exercise3_4
Proof state after:
this : SequentialLimit (fun n => -1 * (1 / (↑n + 1))) (-1 * 0)
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Theorem: exercise3_5
Proof state before:
⊢ SequentialLimit (fun n => sin ↑n / (↑n + 1)) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_6
Proof state before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
⊢ ∀ (n : ℕ), u n ≤ l
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_7
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t = f '' (s ∩ f ⁻¹' t)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_8
Proof state before:
⊢ (fun x => x ^ 2) ⁻¹' {y | y ≥ 4} = {x | x ≤ -2} ∪ {x | x ≥ 2}
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_9
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
have h1' : ∀ x y, f x ≠ g y
Proof state after:
case h1'
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
⊢ ∀ (x : α) (y : β), f x ≠ g y

α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Theorem: exercise3_9
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
have h1'' : ∀ y x, g y ≠ f x
Proof state after:
case h1''
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
⊢ ∀ (y : β) (x : α), g y ≠ f x

α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Theorem: exercise3_9
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
have h2' : ∀ x, x ∈ range f ∪ range g := eq_univ_iff_forall.1 h2
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Theorem: exercise3_9
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
have hf' : ∀ x x', f x = f x' ↔ x = x' := fun x x' ↦ hf.eq_iff
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
hf' : ∀ (x x' : α), f x = f x' ↔ x = x'
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Theorem: exercise3_9
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
hf' : ∀ (x x' : α), f x = f x' ↔ x = x'
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
let L : Set α × Set β → Set γ :=
  fun (s, t) ↦ sorry
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
hf' : ∀ (x x' : α), f x = f x' ↔ x = x'
L : Set α × Set β → Set γ :=
  fun x =>
    match x with
    | (s, t) => sorryAx (Set γ)
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Theorem: exercise3_9
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
hf' : ∀ (x x' : α), f x = f x' ↔ x = x'
L : Set α × Set β → Set γ :=
  fun x =>
    match x with
    | (s, t) => sorryAx (Set γ)
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
let R : Set γ → Set α × Set β :=
  fun s ↦ sorry
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
hf' : ∀ (x x' : α), f x = f x' ↔ x = x'
L : Set α × Set β → Set γ :=
  fun x =>
    match x with
    | (s, t) => sorryAx (Set γ)
R : Set γ → Set α × Set β := fun s => sorryAx (Set α × Set β)
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Theorem: exercise3_9
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
h1'' : ∀ (y : β) (x : α), g y ≠ f x
h2' : ∀ (x : γ), x ∈ range f ∪ range g
hf' : ∀ (x x' : α), f x = f x' ↔ x = x'
L : Set α × Set β → Set γ :=
  fun x =>
    match x with
    | (s, t) => sorryAx (Set γ)
R : Set γ → Set α × Set β := fun s => sorryAx (Set α × Set β)
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise3_9
Proof state before:
case h1'
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
⊢ ∀ (x : α) (y : β), f x ≠ g y
Tactic:
intro x y h
Proof state after:
case h1'
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
x : α
y : β
h : f x = g y
⊢ False
Theorem: exercise3_9
Proof state before:
case h1'
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
x : α
y : β
h : f x = g y
⊢ False
Tactic:
apply h1.subset
Proof state after:
case h1'.a
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
x : α
y : β
h : f x = g y
⊢ ?h1'.a ∈ range f ∩ range g

case h1'.a
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
x : α
y : β
h : f x = g y
⊢ γ
Theorem: exercise3_9
Proof state before:
case h1'.a
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
x : α
y : β
h : f x = g y
⊢ ?h1'.a ∈ range f ∩ range g

case h1'.a
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
x : α
y : β
h : f x = g y
⊢ γ
Tactic:
exact ⟨⟨x, h⟩, ⟨y, rfl⟩⟩
Proof state after:
no goals
Theorem: exercise3_9
Proof state before:
case h1''
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
⊢ ∀ (y : β) (x : α), g y ≠ f x
Tactic:
intro x y
Proof state after:
case h1''
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
x : β
y : α
⊢ g x ≠ f y
Theorem: exercise3_9
Proof state before:
case h1''
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
x : β
y : α
⊢ g x ≠ f y
Tactic:
symm
Proof state after:
case h1''
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
x : β
y : α
⊢ f y ≠ g x
Theorem: exercise3_9
Proof state before:
case h1''
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
hf : Injective f
hg : Injective g
h1 : range f ∩ range g = ∅
h2 : range f ∪ range g = univ
h1' : ∀ (x : α) (y : β), f x ≠ g y
x : β
y : α
⊢ f y ≠ g x
Tactic:
apply h1'
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∉ A ∧ x₂ ∉ A
⊢ x₁ = x₂
Tactic:
sorry
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₁ = x₂
Tactic:
have x₂A : x₂ ∈ A := by
  apply not_imp_self.mp
  intro (x₂nA : x₂ ∉ A)
  rw [if_pos x₁A, if_neg x₂nA] at hxeq
  rw [A_def, sbSet, mem_iUnion] at x₁A
  have x₂eq : x₂ = g (f x₁) := by
    sorry
  rcases x₁A with ⟨n, hn⟩
  rw [A_def, sbSet, mem_iUnion]
  use n + 1
  simp [sbAux]
  exact ⟨x₁, hn, x₂eq.symm⟩
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂
Tactic:
sorry
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
have x₂eq : x₂ = g (f x₁) := by
  sorry
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
⊢ x₂ ∈ A
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
⊢ x₂ = g (f x₁)
Tactic:
sorry
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
⊢ SequentialLimit u l → SequentialLimit u l' → l = l'
Tactic:
sorry
Proof state after:
no goals
Theorem: sq_add_sq_eq_zero
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: gaussInt.norm_nonneg
Proof state before:
x : gaussInt
⊢ 0 ≤ norm x
Tactic:
sorry
Proof state after:
no goals
Theorem: gaussInt.norm_eq_zero
Proof state before:
x : gaussInt
⊢ norm x = 0 ↔ x = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: gaussInt.norm_pos
Proof state before:
x : gaussInt
⊢ 0 < norm x ↔ x ≠ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: gaussInt.norm_mul
Proof state before:
x y : gaussInt
⊢ norm (x * y) = norm x * norm y
Tactic:
sorry
Proof state after:
no goals
Theorem: Point.add_commutative
Proof state before:
n : ℕ
a b : Point
⊢ add a b = add b a
Tactic:
simp [add, add_comm]
Proof state after:
no goals
Theorem: map_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ f <$> x >>= g = x >>= g ∘ f
Tactic:
rw [map_eq_pure_bind, bind_assoc]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f
Theorem: map_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f
Tactic:
apply bind_congr
Proof state after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ ∀ (a : α), pure (f a) >>= g = (g ∘ f) a
Theorem: map_bind
Proof state before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ ∀ (a : α), pure (f a) >>= g = (g ∘ f) a
Tactic:
intro a
Proof state after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ pure (f a) >>= g = (g ∘ f) a
Theorem: map_bind
Proof state before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ pure (f a) >>= g = (g ∘ f) a
Tactic:
rw [pure_bind]
Proof state after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ g (f a) = (g ∘ f) a
Theorem: map_bind
Proof state before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ g (f a) = (g ∘ f) a
Tactic:
rfl
Proof state after:
no goals
Theorem: DijkstraMonad.dbind_congr
Proof state before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
have : wf₁ = wf₂ := by
  funext a
  exact (hf a).eq_param
Proof state after:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : wf₁ = wf₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Theorem: DijkstraMonad.dbind_congr
Proof state before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : wf₁ = wf₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
cases this
Proof state after:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Theorem: DijkstraMonad.dbind_congr
Proof state before:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
have : f₁ = f₂ := by
  funext a
  exact (hf a).eq_of_deq
Proof state after:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : f₁ = f₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Theorem: DijkstraMonad.dbind_congr
Proof state before:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : f₁ = f₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
cases this
Proof state after:
case refl.refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₁ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₁)
Theorem: DijkstraMonad.dbind_congr
Proof state before:
case refl.refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₁ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₁)
Tactic:
exact DEq.refl _
Proof state after:
no goals
Theorem: DijkstraMonad.dbind_congr
Proof state before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ wf₁ = wf₂
Tactic:
funext a
Proof state after:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ wf₁ a = wf₂ a
Theorem: DijkstraMonad.dbind_congr
Proof state before:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ wf₁ a = wf₂ a
Tactic:
exact (hf a).eq_param
Proof state after:
no goals
Theorem: DijkstraMonad.dbind_congr
Proof state before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ f₁ = f₂
Tactic:
funext a
Proof state after:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ f₁ a = f₂ a
Theorem: DijkstraMonad.dbind_congr
Proof state before:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ f₁ a = f₂ a
Tactic:
exact (hf a).eq_of_deq
Proof state after:
no goals
Theorem: DijkstraMonad.Push.deq
Proof state before:
W₁ : Type u → Type v₁
inst✝¹ : Monad W₁
W₂ : Type u → Type v₂
inst✝ : Monad W₂
F : MonadHom W₁ W₂
M : (α : Type u) → W₁ α → Type w
α : Type u
wa₂ wa₂' : W₂ α
base : W₁ α
body✝ : M α base
hx : MonadHom.app F base = wa₂
hy : MonadHom.app F base = wa₂'
⊢ DEq (Push F M α) { base := base, body := body✝, underly := hx } { base := base, body := body✝, underly := hy }
Tactic:
cases (Eq.trans hy.symm hx)
Proof state after:
case refl
W₁ : Type u → Type v₁
inst✝¹ : Monad W₁
W₂ : Type u → Type v₂
inst✝ : Monad W₂
F : MonadHom W₁ W₂
M : (α : Type u) → W₁ α → Type w
α : Type u
wa₂ : W₂ α
base : W₁ α
body✝ : M α base
hx hy : MonadHom.app F base = wa₂
⊢ DEq (Push F M α) { base := base, body := body✝, underly := hx } { base := base, body := body✝, underly := hy }
Theorem: DijkstraMonad.Push.deq
Proof state before:
case refl
W₁ : Type u → Type v₁
inst✝¹ : Monad W₁
W₂ : Type u → Type v₂
inst✝ : Monad W₂
F : MonadHom W₁ W₂
M : (α : Type u) → W₁ α → Type w
α : Type u
wa₂ : W₂ α
base : W₁ α
body✝ : M α base
hx hy : MonadHom.app F base = wa₂
⊢ DEq (Push F M α) { base := base, body := body✝, underly := hx } { base := base, body := body✝, underly := hy }
Tactic:
exact DEq.refl _
Proof state after:
no goals
Theorem: List.val_zipProof
Proof state before:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ Subtype.val <$> zipProof as h = as
Tactic:
induction as
Proof state after:
case nil
α : Type u
p : α → Prop
h : forAll p []
⊢ Subtype.val <$> zipProof [] h = []

case cons
α : Type u
p : α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {h : forAll p tail✝}, Subtype.val <$> zipProof tail✝ h = tail✝
h : forAll p (head✝ :: tail✝)
⊢ Subtype.val <$> zipProof (head✝ :: tail✝) h = head✝ :: tail✝
Theorem: List.val_zipProof
Proof state before:
α : Type u
p : α → Prop
h : forAll p []
⊢ Subtype.val <$> zipProof [] h = []
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: List.val_zipProof
Proof state before:
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, Subtype.val <$> zipProof as h = as
h : forAll p (a :: as)
⊢ Subtype.val <$> zipProof (a :: as) h = a :: as
Tactic:
case cons a as h_ind =>
  cases h with | intro ha has =>
  dsimp [Functor.map, zipProof, List.map] at *
  rw [h_ind]
Proof state after:
no goals
Theorem: List.val_zipProof
Proof state before:
α : Type u
p : α → Prop
h : forAll p []
⊢ Subtype.val <$> zipProof [] h = []
Tactic:
rfl
Proof state after:
no goals