Theorem: exercise3_10 (LeanCourse/Assignments/Solutions/Solutions3.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) ↦ f '' s ∪ g '' t
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) => f '' s ∪ g '' t
⊢ ∃ 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) => f '' s ∪ g '' t
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
let R : Set γ → Set α × Set β :=
  fun s ↦ (f ⁻¹' s, g ⁻¹' s)
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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ ∃ 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ ∃ L R, L ∘ R = id ∧ R ∘ L = id
Tactic:
use L
State after:
case h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ ∃ R, L ∘ R = id ∧ R ∘ L = id

State before:
case h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ ∃ R, L ∘ R = id ∧ R ∘ L = id
Tactic:
use R
State after:
case h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ L ∘ R = id ∧ R ∘ L = id

State before:
case h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ L ∘ R = id ∧ R ∘ L = id
Tactic:
constructor
State after:
case h.left
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ L ∘ R = id

case h.right
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ R ∘ L = id

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

State before:
case h.left
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ L ∘ R = id
Tactic:
ext s x
State after:
case h.left.h.h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set γ
x : γ
⊢ x ∈ (L ∘ R) s ↔ x ∈ id s

State before:
case h.left.h.h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set γ
x : γ
⊢ x ∈ (L ∘ R) s ↔ x ∈ id s
Tactic:
obtain ⟨x, rfl⟩|⟨x, rfl⟩ := h2' x
State after:
case h.left.h.h.inl.intro
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set γ
x : α
⊢ f x ∈ (L ∘ R) s ↔ f x ∈ id s

case h.left.h.h.inr.intro
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set γ
x : β
⊢ g x ∈ (L ∘ R) s ↔ g x ∈ id s

State before:
case h.left.h.h.inl.intro
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set γ
x : α
⊢ f x ∈ (L ∘ R) s ↔ f x ∈ id s
Tactic:
simp [h1'', hf.eq_iff]
State after:
no goals

State before:
case h.left.h.h.inr.intro
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set γ
x : β
⊢ g x ∈ (L ∘ R) s ↔ g x ∈ id s
Tactic:
simp [h1', hg.eq_iff]
State after:
no goals

State before:
case h.right
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
⊢ R ∘ L = id
Tactic:
ext s x
State after:
case h.right.h.h₁.h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set α × Set β
x : α
⊢ x ∈ ((R ∘ L) s).1 ↔ x ∈ (id s).1

case h.right.h.h₂.h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set α × Set β
x : β
⊢ x ∈ ((R ∘ L) s).2 ↔ x ∈ (id s).2

State before:
case h.right.h.h₁.h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set α × Set β
x : α
⊢ x ∈ ((R ∘ L) s).1 ↔ x ∈ (id s).1
Tactic:
simp [hf.eq_iff, h1'']
State after:
no goals

State before:
case h.right.h.h₂.h
α : 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) => f '' s ∪ g '' t
R : Set γ → Set α × Set β := fun s => (f ⁻¹' s, g ⁻¹' s)
s : Set α × Set β
x : β
⊢ x ∈ ((R ∘ L) s).2 ↔ x ∈ (id s).2
Tactic:
simp [hg.eq_iff, h1']
State after:
no goals