internlm/Lean-Github huggingface dataset:
Theorem: left_inv_eq_right_inv₁
Proof state before:
M : Type
inst✝ : Monoid₁ M
a b c : M
hba : b ⋄ a = 𝟙
hac : a ⋄ c = 𝟙
⊢ b = c
Tactic:
rw [← DiaOneClass₁.one_dia c, ← hba, Semigroup₁.dia_assoc, hac, DiaOneClass₁.dia_one b]
Proof state after:
no goals
Theorem: dia_inv
Proof state before:
G : Type
inst✝ : Group₁ G
a : G
⊢ a ⋄ a⁻¹ = 𝟙
Tactic:
rw [← inv_dia a⁻¹, inv_eq_of_dia (inv_dia a)]
Proof state after:
no goals
Theorem: left_inv_eq_right_inv'
Proof state before:
M : Type
inst✝ : Monoid₃ M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c
Tactic:
rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]
Proof state after:
no goals
Theorem: Group₃.mul_inv
Proof state before:
G : Type
inst✝ : Group₃ G
a : G
⊢ a * a⁻¹ = 1
Tactic:
rw [← inv_mul a⁻¹, inv_eq_of_mul (inv_mul a)]
Proof state after:
no goals
Theorem: sb_right_inv
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
⊢ g (invFun g x) = x
Tactic:
have : x ∈ g '' univ := by
  contrapose! hx
  rw [sbSet, mem_iUnion]
  use 0
  rw [sbAux, mem_diff]
  exact ⟨mem_univ _, hx⟩
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet 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✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : x ∈ g '' univ
⊢ g (invFun g x) = x
Tactic:
have : ∃ y, g y = x := by
  simp at this
  assumption
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet 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✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this✝ : x ∈ g '' univ
this : ∃ y, g y = x
⊢ g (invFun g x) = x
Tactic:
exact invFun_eq this
Proof state after:
no goals
Theorem: sb_right_inv
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
⊢ x ∈ g '' univ
Tactic:
contrapose! hx
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbSet f g
Theorem: sb_right_inv
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbSet f g
Tactic:
rw [sbSet, mem_iUnion]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ ∃ i, x ∈ sbAux f g i
Theorem: sb_right_inv
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ ∃ i, x ∈ sbAux f g i
Tactic:
use 0
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbAux f g 0
Theorem: sb_right_inv
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbAux f g 0
Tactic:
rw [sbAux, mem_diff]
Proof state after:
case h
α : Type u_1
β : Type u_2
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✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ univ ∧ x ∉ g '' univ
Tactic:
exact ⟨mem_univ _, hx⟩
Proof state after:
no goals
Theorem: sb_right_inv
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : x ∈ g '' univ
⊢ ∃ y, g y = x
Tactic:
simp at this
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : ∃ y, g y = x
⊢ ∃ y, g y = x
Theorem: sb_right_inv
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : ∃ y, g y = x
⊢ ∃ y, g y = x
Tactic:
assumption
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
⊢ Injective (sbFun f g)
Tactic:
set A := sbSet f g with A_def
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
⊢ Injective (sbFun f g)
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
⊢ Injective (sbFun f g)
Tactic:
set h := sbFun f g with h_def
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
⊢ Injective h
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
⊢ Injective h
Tactic:
intro x₁ x₂
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
⊢ h x₁ = h x₂ → x₁ = x₂
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
⊢ h x₁ = h x₂ → x₁ = x₂
Tactic:
intro (hxeq : h x₁ = h x₂)
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂
Tactic:
simp only [h_def, sbFun, ← A_def] at hxeq
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂
⊢ x₁ = x₂
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂
⊢ x₁ = x₂
Tactic:
by_cases xA : x₁ ∈ A ∨ x₂ ∈ A
Proof state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂

case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂
Theorem: sb_injective
Proof state before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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:
push_neg  at xA
Proof state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂
Theorem: sb_injective
Proof state before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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:
rw [if_neg xA.1, if_neg xA.2] at hxeq
Proof state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : invFun g x₁ = invFun g x₂
xA : x₁ ∉ A ∧ x₂ ∉ A
⊢ x₁ = x₂
Theorem: sb_injective
Proof state before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : invFun g x₁ = invFun g x₂
xA : x₁ ∉ A ∧ x₂ ∉ A
⊢ x₁ = x₂
Tactic:
rw [← sb_right_inv f g xA.1, hxeq, sb_right_inv f g xA.2]
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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:
wlog x₁A : x₁ ∈ A generalizing x₁ x₂ hxeq xA
Proof state after:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₁ = x₂

α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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 _root_.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
    rw [hxeq, sb_right_inv f g x₂nA]
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
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
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:
rw [if_pos x₁A, if_pos x₂A] at hxeq
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₁ = f 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
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₁ = f x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂
Tactic:
exact hf hxeq
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₁ = x₂
Tactic:
symm
Proof state after:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₂ = x₁
Theorem: sb_injective
Proof state before:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₂ = x₁
Tactic:
apply this hxeq.symm xA.symm (xA.resolve_left x₁A)
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
Tactic:
apply _root_.not_imp_self.mp
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
Tactic:
intro (x₂nA : x₂ ∉ A)
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
rw [if_pos x₁A, if_neg x₂nA] at hxeq
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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 : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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 : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
rw [A_def, sbSet, mem_iUnion] at x₁A
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
  rw [hxeq, sb_right_inv f g x₂nA]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
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
Tactic:
rcases x₁A with ⟨n, hn⟩
Proof state after:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ A
Theorem: sb_injective
Proof state before:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ A
Tactic:
rw [A_def, sbSet, mem_iUnion]
Proof state after:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ i, x₂ ∈ sbAux f g i
Theorem: sb_injective
Proof state before:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ i, x₂ ∈ sbAux f g i
Tactic:
use n + 1
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ sbAux f g (n + 1)
Theorem: sb_injective
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ sbAux f g (n + 1)
Tactic:
simp [sbAux]
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ a ∈ sbAux f g n, g (f a) = x₂
Theorem: sb_injective
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ a ∈ sbAux f g n, g (f a) = x₂
Tactic:
exact ⟨x₁, hn, x₂eq.symm⟩
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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:
rw [hxeq, sb_right_inv f g x₂nA]
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ Surjective (sbFun f g)
Tactic:
set A := sbSet f g with A_def
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
⊢ Surjective (sbFun f g)
Theorem: sb_surjective
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
⊢ Surjective (sbFun f g)
Tactic:
set h := sbFun f g with h_def
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
⊢ Surjective h
Theorem: sb_surjective
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
⊢ Surjective h
Tactic:
intro y
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
y : β
⊢ ∃ a, h a = y
Theorem: sb_surjective
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
y : β
⊢ ∃ a, h a = y
Tactic:
by_cases gyA : g y ∈ A
Proof state after:
case pos
α : 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
y : β
gyA : g y ∈ A
⊢ ∃ a, h a = y

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
y : β
gyA : g y ∉ A
⊢ ∃ a, h a = y
Theorem: sb_surjective
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
y : β
gyA : g y ∉ A
⊢ ∃ a, h a = y
Tactic:
use g y
Proof state after:
case h
α : 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
y : β
gyA : g y ∉ A
⊢ h (g y) = y
Theorem: sb_surjective
Proof state before:
case h
α : 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
y : β
gyA : g y ∉ A
⊢ h (g y) = y
Tactic:
simp only [h_def, sbFun, if_neg gyA]
Proof state after:
case h
α : 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
y : β
gyA : g y ∉ A
⊢ invFun g (g y) = y