Theorem: exercise3_9 (LeanCourse/Assignments/Assignment3.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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
⊢ γ

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⟩⟩
State after:
no goals

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
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

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
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

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'
State after:
no goals