internlm/Lean-Github huggingface dataset:
Theorem: exercise3_8
Proof state before:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)
Tactic:
rintro ⟨⟨x, xs, rfl⟩, fxv⟩
Proof state after:
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)
Theorem: exercise3_8
Proof state before:
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)
Tactic:
use x, ⟨xs, fxv⟩
Proof state after:
no goals
Theorem: exercise3_8
Proof state before:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t
Tactic:
rintro ⟨x, ⟨⟨xs, fxv⟩, rfl⟩⟩
Proof state after:
case h.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : x ∈ f ⁻¹' t
⊢ f x ∈ f '' s ∩ t
Theorem: exercise3_8
Proof state before:
case h.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : x ∈ f ⁻¹' t
⊢ f x ∈ f '' s ∩ t
Tactic:
exact ⟨⟨x, xs, rfl⟩, fxv⟩
Proof state after:
no goals
Theorem: exercise3_9
Proof state before:
⊢ (fun x => x ^ 2) ⁻¹' {y | y ≥ 4} = {x | x ≤ -2} ∪ {x | x ≥ 2}
Tactic:
ext x
Proof state after:
case h
x : ℝ
⊢ x ∈ (fun x => x ^ 2) ⁻¹' {y | y ≥ 4} ↔ x ∈ {x | x ≤ -2} ∪ {x | x ≥ 2}
Theorem: exercise3_9
Proof state before:
case h
x : ℝ
⊢ x ∈ (fun x => x ^ 2) ⁻¹' {y | y ≥ 4} ↔ x ∈ {x | x ≤ -2} ∪ {x | x ≥ 2}
Tactic:
simp [show (4 : ℝ) = 2 ^ 2 by norm_num, sq_le_sq, le_abs']
Proof state after:
no goals
Theorem: exercise3_9
Proof state before:
x : ℝ
⊢ 4 = 2 ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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)
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
⊢ γ
Theorem: exercise3_10
Proof 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⟩⟩
Proof state after:
no goals
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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'
Proof state after:
no goals
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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]
Proof state after:
no goals
Theorem: exercise3_10
Proof 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]
Proof state after:
no goals
Theorem: exercise3_10
Proof 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
Proof 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
Theorem: exercise3_10
Proof 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'']
Proof state after:
no goals
Theorem: exercise3_10
Proof 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']
Proof state after:
no goals
Theorem: exercise2_1
Proof state before:
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise2_2
Proof state before:
f g : ℝ → ℝ
x : ℝ
h : SurjectiveFunction (g ∘ f)
⊢ SurjectiveFunction g
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise2_3
Proof state before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction (g ∘ f) ↔ SurjectiveFunction g
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise2_4
Proof state before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction fun x => 2 * f (3 * (x + 4)) + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise2_5
Proof state before:
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => n * s n) s
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise2_6
Proof state before:
s t : ℕ → ℕ
k : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
⊢ EventuallyGrowsFaster (s₁ + s₂) (t₁ + t₂)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise2_7
Proof state before:
s t : ℕ → ℕ
k : ℕ
⊢ ∃ s, EventuallyGrowsFaster (fun n => s (n + 1)) s ∧ ∀ (n : ℕ), s n ≠ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
⊢ ∀ (k : ℕ), ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.div'_add_mod'
Proof state before:
a b : ℤ
⊢ b * div' a b + mod' a b = a
Tactic:
rw [div', mod']
Proof state after:
a b : ℤ
⊢ b * ((a + b / 2) / b) + ((a + b / 2) % b - b / 2) = a
Theorem: Int.abs_mod'_le
Proof state before:
a b : ℤ
h : 0 < b
⊢ |mod' a b| ≤ b / 2
Tactic:
rw [mod', abs_le]
Proof state after:
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2 ∧ (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.mod'_eq
Proof state before:
a b : ℤ
⊢ mod' a b = a - b * div' a b
Tactic:
linarith [div'_add_mod' a b]
Proof state after:
no goals
Theorem: gaussInt.norm_nonneg
Proof state before:
x : gaussInt
⊢ 0 ≤ norm x
Tactic:
apply add_nonneg <;>
apply sq_nonneg
Proof state after:
no goals
Theorem: gaussInt.norm_eq_zero
Proof state before:
x : gaussInt
⊢ norm x = 0 ↔ x = 0
Tactic:
rw [norm, sq_add_sq_eq_zero, gaussInt.ext_iff]
Proof state after:
x : gaussInt
⊢ x.re = 0 ∧ x.im = 0 ↔ x.re = 0.re ∧ x.im = 0.im
Theorem: gaussInt.norm_eq_zero
Proof state before:
x : gaussInt
⊢ x.re = 0 ∧ x.im = 0 ↔ x.re = 0.re ∧ x.im = 0.im
Tactic:
rfl
Proof state after:
no goals
Theorem: gaussInt.norm_pos
Proof state before:
x : gaussInt
⊢ 0 < norm x ↔ x ≠ 0
Tactic:
rw [lt_iff_le_and_ne, ne_comm, Ne, norm_eq_zero]
Proof state after:
x : gaussInt
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
Theorem: gaussInt.norm_pos
Proof state before:
x : gaussInt
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
Tactic:
simp [norm_nonneg]
Proof state after:
no goals
Theorem: gaussInt.norm_mul
Proof state before:
x y : gaussInt
⊢ norm (x * y) = norm x * norm y
Tactic:
simp [norm]
Proof state after:
x y : gaussInt
⊢ (x.re * y.re - x.im * y.im) ^ 2 + (x.re * y.im + x.im * y.re) ^ 2 = (x.re ^ 2 + x.im ^ 2) * (y.re ^ 2 + y.im ^ 2)
Theorem: gaussInt.norm_mul
Proof state before:
x y : gaussInt
⊢ (x.re * y.re - x.im * y.im) ^ 2 + (x.re * y.im + x.im * y.re) ^ 2 = (x.re ^ 2 + x.im ^ 2) * (y.re ^ 2 + y.im ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: gaussInt.norm_conj
Proof state before:
x : gaussInt
⊢ norm (conj x) = norm x
Tactic:
simp [norm]
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
⊢ norm (x % y) < norm y
Tactic:
have norm_y_pos : 0 < norm y := by rwa [norm_pos]
Proof state after:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
⊢ norm (x % y) < norm y
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
⊢ norm (x % y) < norm y
Tactic:
have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
Proof state after:
case H1
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
⊢ x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }

x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) < norm y