internlm/Lean-Github huggingface dataset:
Theorem: RegularOpens.coe_bot
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
⊢ ↑⊥ = ∅
Tactic:
have : (⊥ : RegularOpens X) = (⊥ : Closeds X).int := rfl
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
this : ⊥ = Closeds.int ⊥
⊢ ↑⊥ = ∅
Theorem: RegularOpens.coe_bot
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
this : ⊥ = Closeds.int ⊥
⊢ ↑⊥ = ∅
Tactic:
simp [this]
Proof state after:
no goals
Theorem: RegularOpens.coe_sInf
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
⊢ ↑(sInf U) = interior (⋂₀ ((fun u => closure ↑u) '' U))
Tactic:
have : sInf U = (sInf (cl '' U)).int := rfl
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
this : sInf U = Closeds.int (sInf (cl '' U))
⊢ ↑(sInf U) = interior (⋂₀ ((fun u => closure ↑u) '' U))
Theorem: RegularOpens.coe_sInf
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
this : sInf U = Closeds.int (sInf (cl '' U))
⊢ ↑(sInf U) = interior (⋂₀ ((fun u => closure ↑u) '' U))
Tactic:
simp [this]
Proof state after:
no goals
Theorem: RegularOpens.Closeds.coe_sSup
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
⊢ ↑(sSup C) = closure (⋃₀ (SetLike.coe '' C))
Tactic:
have : sSup C = Closeds.closure (sSup ((↑) '' C)) := rfl
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(sSup C) = closure (⋃₀ (SetLike.coe '' C))
Theorem: RegularOpens.Closeds.coe_sSup
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(sSup C) = closure (⋃₀ (SetLike.coe '' C))
Tactic:
simp [this]
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(Closeds.closure (⋃ x ∈ C, ↑x)) = closure (⋃ x ∈ C, ↑x)
Theorem: RegularOpens.Closeds.coe_sSup
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(Closeds.closure (⋃ x ∈ C, ↑x)) = closure (⋃ x ∈ C, ↑x)
Tactic:
rfl
Proof state after:
no goals
Theorem: RegularOpens.coe_sSup
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
⊢ ↑(sSup U) = interior (closure (⋃₀ ((fun u => closure ↑u) '' U)))
Tactic:
have : sSup U = (sSup (cl '' U)).int := rfl
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
this : sSup U = Closeds.int (sSup (cl '' U))
⊢ ↑(sSup U) = interior (closure (⋃₀ ((fun u => closure ↑u) '' U)))
Theorem: RegularOpens.coe_sSup
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
this : sSup U = Closeds.int (sSup (cl '' U))
⊢ ↑(sSup U) = interior (closure (⋃₀ ((fun u => closure ↑u) '' U)))
Tactic:
simp [this]
Proof state after:
no goals
Theorem: RegularOpens.coe_compl
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V U : RegularOpens X
⊢ ↑Uᶜ = interior (↑U)ᶜ
Tactic:
sorry
Proof state after:
no goals
Theorem: PointedFunction.comp
Proof state before:
X : PointedType
Y : PointedType
Z : PointedType
g : Y →. Z
f : X →. Y
⊢ (↑g ∘ ↑f) X.pt = Z.pt
Tactic:
simp
Proof state after:
no goals
Theorem: conjugate_one
Proof state before:
G : Type u_1
H✝ : Type u_2
K : Type u_3
inst✝² : Group G
inst✝¹ : Group H✝
inst✝ : Group K
H : Subgroup G
⊢ conjugate 1 H = H
Tactic:
sorry
Proof state after:
no goals
Theorem: conjugate_mul
Proof state before:
G : Type u_1
H✝ : Type u_2
K : Type u_3
inst✝² : Group G
inst✝¹ : Group H✝
inst✝ : Group K
x y : G
H : Subgroup G
⊢ conjugate (x * y) H = conjugate x (conjugate y H)
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
⊢ 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
hg : Injective g
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
hg : Injective g
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
hg : Injective g
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
hg : Injective g
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
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₂ : α
⊢ 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
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₂ : α
⊢ 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
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 : 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
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 : 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
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₂
⊢ 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₂
⊢ 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
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₂

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₂
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:
push_neg  at xA
Proof state after:
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₂
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:
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
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 : 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
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 : 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
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:
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
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
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
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₂
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
    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
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:
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
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₁ = 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
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₁ = 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
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
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
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
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
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
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
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
Tactic:
apply not_imp_self.mp
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
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
Tactic:
intro (x₂nA : x₂ ∉ A)
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₂nA : x₂ ∉ A
⊢ 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 : (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
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 : 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
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 : 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
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
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
  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
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₂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
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₂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
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₂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
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₂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
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₂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
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₂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
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₂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
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₂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
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₂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
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:
rw [hxeq, sb_right_inv f g x₂nA]
Proof state after:
no goals
Theorem: units_ne_neg_self
Proof state before:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ u ≠ -u
Tactic:
sorry
Proof state after:
no goals
Theorem: iterate_frobeniusMorphism
Proof state before:
R : Type u_1
M : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_3
inst✝¹ : Field K
inst✝ : CharP K p
x : K
n : ℕ
⊢ (↑(frobeniusMorphism p K))^[n] x = x ^ p ^ n
Tactic:
sorry
Proof state after:
no goals
Theorem: frobeniusMorphism_injective
Proof state before:
R : Type u_1
M : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_3
inst✝¹ : Field K
inst✝ : CharP K p
x : K
⊢ Injective ↑(frobeniusMorphism p K)
Tactic:
have : ∀ x : K, x ^ p = 0 → x = 0 := by exact?
Proof state after:
R : Type u_1
M : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_3
inst✝¹ : Field K
inst✝ : CharP K p
x : K
this : ∀ (x : K), x ^ p = 0 → x = 0
⊢ Injective ↑(frobeniusMorphism p K)
Theorem: frobeniusMorphism_injective
Proof state before:
R : Type u_1
M : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_3
inst✝¹ : Field K
inst✝ : CharP K p
x : K
this : ∀ (x : K), x ^ p = 0 → x = 0
⊢ Injective ↑(frobeniusMorphism p K)
Tactic:
sorry
Proof state after:
no goals
Theorem: frobeniusMorphism_injective
Proof state before:
R : Type u_1
M : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_3
inst✝¹ : Field K
inst✝ : CharP K p
x : K
⊢ ∀ (x : K), x ^ p = 0 → x = 0
Tactic:
exact?
Proof state after:
no goals
Theorem: frobeniusMorphism_bijective
Proof state before:
R : Type u_1
M : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_3
inst✝² : Field K
inst✝¹ : CharP K p
x : K
inst✝ : Finite K
⊢ Bijective ↑(frobeniusMorphism p K)
Tactic:
sorry
Proof state after:
no goals
Theorem: Group₃.mul_inv
Proof state before:
G : Type
inst✝ : Group₃ G
a : G
⊢ a * a⁻¹ = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: mul_left_cancel₃
Proof state before:
G : Type
inst✝ : Group₃ G
a b c : G
h : a * b = a * c
⊢ b = c
Tactic:
sorry
Proof state after:
no goals
Theorem: mul_right_cancel₃
Proof state before:
G : Type
inst✝ : Group₃ G
a b c : G
h : b * a = c * a
⊢ b = c
Tactic:
sorry
Proof state after:
no goals