internlm/Lean-Github huggingface dataset:
Theorem: N.zero_add
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
n m a✝ b c a : N
hrec : 0 + a = a
⊢ 0 + succ a = succ a
Tactic:
rw [add_succ, hrec]
Proof state after:
no goals
Theorem: N.add_assoc
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + c = a + (b + c)
Tactic:
induction c with
| zero =>
  sorry
| succ c hrec =>
  sorry
Proof state after:
no goals
Theorem: N.add_assoc
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + zero = a + (b + zero)
Tactic:
sorry
Proof state after:
no goals
Theorem: N.add_assoc
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
n m a b c✝ c : N
hrec : a + b + c = a + (b + c)
⊢ a + b + succ c = a + (b + succ c)
Tactic:
sorry
Proof state after:
no goals
Theorem: N.succ_add
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ succ a + b = succ (a + b)
Tactic:
sorry
Proof state after:
no goals
Theorem: N.add_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b = b + a
Tactic:
sorry
Proof state after:
no goals
Theorem: N.one_eq_succ_zero
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ 1 = succ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: N.succ_eq_add_one
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ succ a = a + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: N.add_right_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + c = a + c + b
Tactic:
rw [add_assoc a b c]
Proof state after:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + (b + c) = a + c + b
Theorem: N.add_right_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + (b + c) = a + c + b
Tactic:
rw [add_comm b c]
Proof state after:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + (c + b) = a + c + b
Theorem: N.add_right_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + (c + b) = a + c + b
Tactic:
rw [← add_assoc]
Proof state after:
no goals
Theorem: N.mul_zero
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: N.mul_succ
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * succ b = a * b + a
Tactic:
rfl
Proof state after:
no goals
Theorem: N.zero_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * a = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: N.mul_one
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * 1 = a
Tactic:
sorry
Proof state after:
no goals
Theorem: N.one_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 1 * a = a
Tactic:
sorry
Proof state after:
no goals
Theorem: N.mul_add
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (b + c) = a * b + a * c
Tactic:
sorry
Proof state after:
no goals
Theorem: N.mul_assoc
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * b * c = a * (b * c)
Tactic:
sorry
Proof state after:
no goals
Theorem: N.succ_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ succ a * b = a * b + b
Tactic:
sorry
Proof state after:
no goals
Theorem: N.add_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ (a + b) * c = a * c + b * c
Tactic:
sorry
Proof state after:
no goals
Theorem: N.mul_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * b = b * a
Tactic:
sorry
Proof state after:
no goals
Theorem: N.pow_zero
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a ^ 0 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: N.pow_succ
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a ^ succ b = a ^ b * a
Tactic:
rfl
Proof state after:
no goals
Theorem: N.two_eq_succ_one
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
⊢ 2 = succ 1
Tactic:
rfl
Proof state after:
no goals
Theorem: even_mul_add_one
Proof state before:
n : ℕ
⊢ Even (n * (n + 1))
Tactic:
cases (even_or_odd n) with
| inl heven =>
 
  exact Even.mul_right heven (n + 1)
| inr hodd =>
  have hsucc : Even (n + 1) := by
   rw [even_add_one, ← odd_iff_not_even]
   exact hodd
  exact Even.mul_left hsucc n
Proof state after:
no goals
Theorem: even_mul_add_one
Proof state before:
case inl
n : ℕ
heven : Even n
⊢ Even (n * (n + 1))
Tactic:
exact Even.mul_right heven (n + 1)
Proof state after:
no goals
Theorem: even_mul_add_one
Proof state before:
case inr
n : ℕ
hodd : Odd n
⊢ Even (n * (n + 1))
Tactic:
have hsucc : Even (n + 1) := by
 rw [even_add_one, ← odd_iff_not_even]
 exact hodd
Proof state after:
case inr
n : ℕ
hodd : Odd n
hsucc : Even (n + 1)
⊢ Even (n * (n + 1))
Theorem: even_mul_add_one
Proof state before:
case inr
n : ℕ
hodd : Odd n
hsucc : Even (n + 1)
⊢ Even (n * (n + 1))
Tactic:
exact Even.mul_left hsucc n
Proof state after:
no goals
Theorem: even_mul_add_one
Proof state before:
n : ℕ
hodd : Odd n
⊢ Even (n + 1)
Tactic:
rw [even_add_one, ← odd_iff_not_even]
Proof state after:
n : ℕ
hodd : Odd n
⊢ Odd n
Theorem: even_mul_add_one
Proof state before:
n : ℕ
hodd : Odd n
⊢ Odd n
Tactic:
exact hodd
Proof state after:
no goals
Theorem: S1
Proof state before:
α β : Type
f : α → β
t : Set α
⊢ t ⊆ f ⁻¹' (f '' t)
Tactic:
sorry
Proof state after:
no goals
Theorem: S2
Proof state before:
α β : Type
f : α → β
t : Set α
hf : Injective f
⊢ t = f ⁻¹' (f '' t)
Tactic:
sorry
Proof state after:
no goals
Theorem: S3
Proof state before:
α β : Type
f✝ : α → β
t✝ : Set α
f : α → β
s : Set β
t : Set α
⊢ t ∪ f ⁻¹' s ⊆ f ⁻¹' (f '' t ∪ s)
Tactic:
sorry
Proof state after:
no goals
Theorem: N1
Proof state before:
a b c d : ℤ
hyp : c = b * a - d
hyp' : d = a * b
⊢ c = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: N2
Proof state before:
a b c : ℤ
h1 : a ∣ b
h2 : a ∣ c
⊢ a ∣ b + c
Tactic:
sorry
Proof state after:
no goals
Theorem: N5
Proof state before:
n : ℕ
⊢ 0 < fac n
Tactic:
sorry
Proof state after:
no goals
Theorem: F1
Proof state before:
⊢ Surjective fun n => n + 5
Tactic:
sorry
Proof state after:
no goals
Theorem: F2
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hinj : Surjective (g ∘ f)
⊢ Surjective g
Tactic:
sorry
Proof state after:
no goals
Theorem: F3
Proof state before:
f g : ℤ → ℤ
⊢ even_fun f → even_fun g → even_fun (f - g)
Tactic:
sorry
Proof state after:
no goals
Theorem: add_one_odd_of_even
Proof state before:
n : ℕ
h : Even n
⊢ Odd (n + 1)
Tactic:
apply Even.add_odd
Proof state after:
case a
n : ℕ
h : Even n
⊢ Even n

case a
n : ℕ
h : Even n
⊢ Odd 1
Theorem: add_one_odd_of_even
Proof state before:
case a
n : ℕ
h : Even n
⊢ Even n
Tactic:
exact h
Proof state after:
no goals
Theorem: add_one_odd_of_even
Proof state before:
case a
n : ℕ
h : Even n
⊢ Odd 1
Tactic:
exact odd_one
Proof state after:
no goals
Theorem: inverse_spec
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (inverse f y) = y
Tactic:
rw [inverse]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (if h : ∃ x, f x = y then choose h else default) = y
Theorem: inverse_spec
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (if h : ∃ x, f x = y then choose h else default) = y
Tactic:
rw [dif_pos h]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (choose h) = y
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
⊢ ∀ (f : α → Set α), ¬Surjective f
Tactic:
intros f surjf
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Tactic:
let S := { i | i ∉ f i}
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
⊢ False
Theorem: Cantor
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ False
Tactic:
have h₁ : j ∉ f j := by
  intro h'
  have : j ∉ f j := by
    rwa [h] at h'
  contradiction
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False
Theorem: Cantor
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False
Tactic:
have h₂ : j ∈ S := by
  sorry
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Theorem: Cantor
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Tactic:
have h₃ : j ∉ S := by
  sorry
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ False
Tactic:
have : j ∉ f j := by
  rwa [h] at h'
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
this : j ∉ f j
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ j ∈ S
Tactic:
sorry
Proof state after:
no goals
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ j ∉ S
Tactic:
sorry
Proof state after:
no goals
Theorem: sb_right_inv
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
⊢ g (invFun g x) = x
Tactic:
have : x ∈ g '' univ := by
  contrapose! hx
  rw [sb_set, mem_iUnion]
  use 0
  rw [sb_aux, mem_diff]
  sorry
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
this : x ∈ g '' univ
⊢ g (invFun g x) = x
Theorem: sb_right_inv
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
this : x ∈ g '' univ
⊢ g (invFun g x) = x
Tactic:
have : ∃ y, g y = x := by
  sorry
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
this✝ : x ∈ g '' univ
this : ∃ y, g y = x
⊢ g (invFun g x) = x
Theorem: sb_right_inv
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
this✝ : x ∈ g '' univ
this : ∃ y, g y = x
⊢ g (invFun g x) = x
Tactic:
sorry
Proof state after:
no goals
Theorem: sb_right_inv
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
⊢ x ∈ g '' univ
Tactic:
contrapose! hx
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sb_set f g
Theorem: sb_right_inv
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sb_set f g
Tactic:
rw [sb_set, mem_iUnion]
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ ∃ i, x ∈ sb_aux f g i
Theorem: sb_right_inv
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ ∃ i, x ∈ sb_aux f g i
Tactic:
use 0
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sb_aux f g 0
Theorem: sb_right_inv
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sb_aux f g 0
Tactic:
rw [sb_aux, mem_diff]
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ univ ∧ x ∉ g '' univ
Theorem: sb_right_inv
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ univ ∧ x ∉ g '' univ
Tactic:
sorry
Proof state after:
no goals
Theorem: sb_right_inv
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sb_set f g
this : x ∈ g '' univ
⊢ ∃ y, g y = x
Tactic:
sorry
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
⊢ Injective (sb_fun f g)
Tactic:
set A := sb_set f g with A_def
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
⊢ Injective (sb_fun f g)
Theorem: sb_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
⊢ Injective (sb_fun f g)
Tactic:
set h := sb_fun f g with h_def
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
⊢ Injective h
Theorem: sb_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
⊢ Injective h
Tactic:
intro x₁ x₂ hxeq
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂
Theorem: sb_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂
Tactic:
simp only [h_def, sb_fun, ←A_def] at hxeq
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₂
⊢ x₁ = x₂
Theorem: sb_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₂
⊢ x₁ = x₂
Tactic:
by_cases xA : x₁ ∈ A ∨ x₂ ∈ A
Proof state after:
case pos
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₂

case neg
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₂
Theorem: sb_injective
Proof state before:
case pos
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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:
rcases xA with (xA | xA)
Proof state after:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂

case pos.inr
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Theorem: sb_injective
Proof state before:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Tactic:
have x₂A : x₂ ∈ A := by
  apply not_imp_self.mp
  intro x₂nA
  rw [if_pos xA, if_neg x₂nA] at hxeq
  rw [A_def, sb_set, mem_iUnion] at xA
  have x₂eq : x₂ = g (f x₁) := by
    rw [← sb_right_inv f g x₂nA, hxeq]
  rcases xA with ⟨n, hn⟩
  rw [A_def, sb_set, mem_iUnion]
  use n + 1
  simp [sb_aux]
  exact ⟨x₁, hn, x₂eq.symm⟩
Proof state after:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Theorem: sb_injective
Proof state before:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Tactic:
simp [xA, x₂A] at hxeq
Proof state after:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₁ ∈ A
x₂A : x₂ ∈ A
hxeq : f x₁ = f x₂
⊢ x₁ = x₂
Theorem: sb_injective
Proof state before:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₁ ∈ A
x₂A : x₂ ∈ A
hxeq : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
exact hf hxeq
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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
Tactic:
apply not_imp_self.mp
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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
Theorem: sb_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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
Tactic:
intro x₂nA
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₂nA : x₂ ∉ A
⊢ x₂ ∈ A