[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α α' : Sort u
β : α → Sort v
β' : α' → Sort v
f : (a : α) → β a
f' : (a : α') → β' a
hα : α = α'
h : ∀ (a : α) (a' : α'), HEq a a' → HEq (f a) (f' a')
⊢ HEq f f'
[PROOFSTEP]
subst hα
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
⊢ HEq f f'
[PROOFSTEP]
have : ∀ a, HEq (f a) (f' a) := λ a => h a a (HEq.refl a)
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ HEq f f'
[PROOFSTEP]
have : β = β' := by
  funext a
  exact type_eq_of_heq (this a)
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ β = β'
[PROOFSTEP]
funext a
[GOAL]
case h
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
a : α
⊢ β a = β' a
[PROOFSTEP]
exact type_eq_of_heq (this a)
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this✝ : ∀ (a : α), HEq (f a) (f' a)
this : β = β'
⊢ HEq f f'
[PROOFSTEP]
subst this
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ HEq f f'
[PROOFSTEP]
apply heq_of_eq
[GOAL]
case h
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ f = f'
[PROOFSTEP]
funext a
[GOAL]
case h.h
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
a : α
⊢ f a = f' a
[PROOFSTEP]
exact eq_of_heq (this a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)
[PROOFSTEP]
by_cases h : a == b
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : (a == b) = true
⊢ (f a == f b) = (a == b)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ (f a == f b) = (a == b)
[PROOFSTEP]
simp [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : (a == b) = true
⊢ f a = f b
[PROOFSTEP]
simpa [I.eq_iff] using h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ ¬f a = f b
[PROOFSTEP]
simpa [I.eq_iff] using h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
⊢ Injective fun x => if h : p x then f { val := x, property := h } else f' { val := x, property := h }
[PROOFSTEP]
intros x₁ x₂ h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (fun x => if h : p x then f { val := x, property := h } else f' { val := x, property := h }) x₁ =
    (fun x => if h : p x then f { val := x, property := h } else f' { val := x, property := h }) x₂
⊢ x₁ = x₂
[PROOFSTEP]
dsimp only at h 
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
⊢ x₁ = x₂
[PROOFSTEP]
by_cases h₁ : p x₁
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : p x₁
⊢ x₁ = x₂
[PROOFSTEP]
by_cases h₂ : p x₂
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : ¬p x₁
⊢ x₁ = x₂
[PROOFSTEP]
by_cases h₂ : p x₂
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : p x₁
h₂ : p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_pos h₁, dif_pos h₂] at h 
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : p x₁
h₂ : p x₂
h : f { val := x₁, property := h₁ } = f { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
injection (hf h)
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_pos h₁, dif_neg h₂] at h 
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : p x₁
h₂ : ¬p x₂
h : f { val := x₁, property := h₁ } = f' { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
exact (im_disj h).elim
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : ¬p x₁
h₂ : p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_neg h₁, dif_pos h₂] at h 
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : p x₂
h : f' { val := x₁, property := h₁ } = f { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
exact (im_disj h.symm).elim
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : ¬p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_neg h₁, dif_neg h₂] at h 
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : ¬p x₂
h : f' { val := x₁, property := h₁ } = f' { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
injection (hf' h)
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂
⊢ Surjective f
[PROOFSTEP]
specialize h (fun y ↦ ∃ x, f x = y) (fun _ ↦ True) (funext fun x ↦ eq_true ⟨_, rfl⟩)
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
⊢ Surjective f
[PROOFSTEP]
intro y
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ ∃ a, f a = y
[PROOFSTEP]
rw [congr_fun h y]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ True
[PROOFSTEP]
trivial
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7150
f✝ f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! y, p y
y : β
hpy : (fun y => p y) y
hy : ∀ (y_1 : β), (fun y => p y) y_1 → y_1 = y
x : α
hx : f x = y
⊢ (fun x => p (f x)) x
[PROOFSTEP]
simpa [hx]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7150
f✝ f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! x, p (f x)
x : α
hpx : (fun x => p (f x)) x
hx : ∀ (y : α), (fun x => p (f x)) y → y = x
y : β
hy : (fun y => p y) y
z : α
hz : f z = y
⊢ (fun x => p (f x)) z
[PROOFSTEP]
simpa [hz]
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
⊢ ¬Surjective f
[PROOFSTEP]
intro hf
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False
[PROOFSTEP]
let T : Type max u v := Sigma f
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False
[PROOFSTEP]
cases' hf (Set T) with U hU
[GOAL]
case intro
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
⊢ False
[PROOFSTEP]
let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
[GOAL]
case intro
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
⊢ False
[PROOFSTEP]
have hg : Injective g := by
  intro s t h
  suffices cast hU (g s).2 = cast hU (g t).2
    by
    simp only [cast_cast, cast_eq] at this 
    assumption
  · congr
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
⊢ Injective g
[PROOFSTEP]
intro s t h
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ s = t
[PROOFSTEP]
suffices cast hU (g s).2 = cast hU (g t).2
  by
  simp only [cast_cast, cast_eq] at this 
  assumption
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t
[PROOFSTEP]
simp only [cast_cast, cast_eq] at this 
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
this : s = t
⊢ s = t
[PROOFSTEP]
assumption
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd
[PROOFSTEP]
congr
[GOAL]
case intro
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
hg : Injective g
⊢ False
[PROOFSTEP]
exact cantor_injective g hg
[GOAL]
α : Sort u_2
β : Sort u_1
γ : Sort u_3
f✝ f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
⊢ h (f (g (i a))) = a
[PROOFSTEP]
rw [hf (i a), hh a]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.11227
f✝ f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂
[PROOFSTEP]
rw [h₂.comp_eq_id, comp.right_id]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.11227
f✝ f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂
[PROOFSTEP]
rw [← comp.assoc, h₁.comp_eq_id, comp.left_id]
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f a = b
[PROOFSTEP]
rw [hpi, dif_pos h'] at h 
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b
[PROOFSTEP]
injection h with h
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b
[PROOFSTEP]
subst h
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b
[PROOFSTEP]
apply Classical.choose_spec h'
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
[PROOFSTEP]
rw [hpi, dif_neg h'] at h 
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
[PROOFSTEP]
contradiction
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
a : α
b : β
h : ∃ a, f a = b
⊢ f (invFun f b) = b
[PROOFSTEP]
simp only [invFun, dif_pos h, h.choose_spec]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
a : α
b✝ : β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)
[PROOFSTEP]
rw [hg b]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
a : α
b✝ : β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b
[PROOFSTEP]
exact invFun_eq ⟨g b, hg b⟩
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update f a' b a = if a = a' then b else f a
[PROOFSTEP]
have h2 : (h : a = a') → Eq.rec (motive := λ _ _ => β) b h.symm = b :=
  by
  intro h
  rw [eq_rec_constant]
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ ∀ (h : a = a'), (_ : a' = a) ▸ b = b
[PROOFSTEP]
intro h
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h : a = a'
⊢ (_ : a' = a) ▸ b = b
[PROOFSTEP]
rw [eq_rec_constant]
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
⊢ update f a' b a = if a = a' then b else f a
[PROOFSTEP]
have h3 : (λ h : a = a' => Eq.rec (motive := λ _ _ => β) b h.symm) = (λ _ : a = a' => b) := funext h2
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
⊢ update f a' b a = if a = a' then b else f a
[PROOFSTEP]
let f := λ x => dite (a = a') x (λ (_ : ¬a = a') => (f a))
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝¹ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f✝ : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
f : (a = a' → β) → β := fun x => dite (a = a') x fun x => f✝ a
⊢ update f✝ a' b a = if a = a' then b else f✝ a
[PROOFSTEP]
exact congrArg f h3
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a : α
b : β a
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
⊢ v = v'
[PROOFSTEP]
have := congr_fun h a'
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a : α
b : β a
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : update f a' v a' = update f a' v' a'
⊢ v = v'
[PROOFSTEP]
rwa [update_same, update_same] at this 
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
[PROOFSTEP]
rw [← and_forall_ne a, update_same]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x x_1, p x (f x)
[PROOFSTEP]
rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ x x_1, p x (f x)
[PROOFSTEP]
simp [-not_and, not_and_or]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f g : (a : α) → β a
a : α
b : β a
⊢ update f a b = f ↔ b = f a
[PROOFSTEP]
simp [update_eq_iff]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f g : (a : α) → β a
a : α
b : β a
⊢ f = update f a b ↔ f a = b
[PROOFSTEP]
simp [eq_update_iff]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
[PROOFSTEP]
subst j
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
⊢ f i (update g i v i) = update (fun k => f k (g k)) i (f i v) i
[PROOFSTEP]
simp
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : ¬j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
⊢ f j (update g i v j) (update h i w j) = update (fun k => f k (g k) (h k)) i (f i v w) j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j
[PROOFSTEP]
subst j
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
⊢ f i (update g i v i) (update h i w i) = update (fun k => f k (g k) (h k)) i (f i v w) i
[PROOFSTEP]
simp
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : ¬j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
⊢ update (update f a v) b w = update (update f b w) a v
[PROOFSTEP]
funext c
[GOAL]
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ update (update f a v) b w c = update (update f b w) a v c
[PROOFSTEP]
simp only [update]
[GOAL]
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
by_cases h₁ : c = b
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
by_cases h₂ : c = a
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
by_cases h₂ : c = a
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_pos h₁, dif_pos h₂]
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (_ : b = c) ▸ w = (_ : a = c) ▸ v
[PROOFSTEP]
cases h (h₂.symm.trans h₁)
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : ¬c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_pos h₁, dif_pos h₁, dif_neg h₂]
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_neg h₁, dif_neg h₁, dif_pos h₂]
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : ¬c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_neg h₁, dif_neg h₁, dif_neg h₂]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
⊢ update (update f a v) a w = update f a w
[PROOFSTEP]
funext b
[GOAL]
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
⊢ update (update f a v) a w b = update f a w b
[PROOFSTEP]
by_cases h : b = a
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
h : b = a
⊢ update (update f a v) a w b = update f a w b
[PROOFSTEP]
simp [update, h]
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
h : ¬b = a
⊢ update (update f a v) a w b = update f a w b
[PROOFSTEP]
simp [update, h]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f✝ f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
[PROOFSTEP]
unfold extend
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f✝ f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b
[PROOFSTEP]
congr
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a
[PROOFSTEP]
simp only [extend_def, dif_pos, exists_apply_eq_apply]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ g (Classical.choose (_ : ∃ a_1, f a_1 = f a)) = g a
[PROOFSTEP]
exact hf (Classical.choose_spec (exists_apply_eq_apply f a))
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ extend f g e' b = e' b
[PROOFSTEP]
simp [Function.extend_def, hb]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
hf : FactorsThrough g f
x : α
⊢ g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x
[PROOFSTEP]
simp only [comp_apply, hf.extend_apply]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ g x✝¹ = g x✝
[PROOFSTEP]
rw [Classical.choose_spec h, comp_apply, comp_apply, hf]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
by_cases hb : ∃ a, f a = b
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
case neg
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case pos =>
  rcases hb with ⟨a, ha⟩
  subst b
  rw [hf.extend_apply, FactorsThrough.extend_apply, comp]
  case intro.hf =>
    intro a b h
    simp only [comp_apply]
    apply congr_arg
    exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case pos =>
  rcases hb with ⟨a, ha⟩
  subst b
  rw [hf.extend_apply, FactorsThrough.extend_apply, comp]
  case intro.hf =>
    intro a b h
    simp only [comp_apply]
    apply congr_arg
    exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
rcases hb with ⟨a, ha⟩
[GOAL]
case intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
a : α
ha : f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
subst b
[GOAL]
case intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ F (extend f g e' (f a)) = extend f (F ∘ g) (F ∘ e') (f a)
[PROOFSTEP]
rw [hf.extend_apply, FactorsThrough.extend_apply, comp]
[GOAL]
case intro.hf
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ FactorsThrough (F ∘ g) f
[PROOFSTEP]
case intro.hf =>
  intro a b h
  simp only [comp_apply]
  apply congr_arg
  exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ FactorsThrough (F ∘ g) f
[PROOFSTEP]
case intro.hf =>
  intro a b h
  simp only [comp_apply]
  apply congr_arg
  exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ FactorsThrough (F ∘ g) f
[PROOFSTEP]
intro a b h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a✝ a b : α
h : f a = f b
⊢ (F ∘ g) a = (F ∘ g) b
[PROOFSTEP]
simp only [comp_apply]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a✝ a b : α
h : f a = f b
⊢ F (g a) = F (g b)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a✝ a b : α
h : f a = f b
⊢ g a = g b
[PROOFSTEP]
exact hf h
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case neg => rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb, comp]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case neg => rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb, comp]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb, comp]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
⊢ Injective fun g => extend f g e'
[PROOFSTEP]
intro g₁ g₂ hg
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
⊢ g₁ = g₂
[PROOFSTEP]
refine' funext fun x ↦ _
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
⊢ g₁ x = g₂ x
[PROOFSTEP]
have H := congr_fun hg (f x)
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : (fun g => extend f g e') g₁ (f x) = (fun g => extend f g e') g₂ (f x)
⊢ g₁ x = g₂ x
[PROOFSTEP]
simp only [hf.extend_apply] at H 
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x
[PROOFSTEP]
exact H
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun g => g ∘ f) (g ∘ surjInv (_ : Surjective f)) = g
[PROOFSTEP]
simp only [comp.assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp.right_id]
[GOAL]
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x
[PROOFSTEP]
rw [apply_ite f, h, ite_not]
[GOAL]
p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (sometimes f)
[PROOFSTEP]
rwa [sometimes_eq]
[GOAL]
α β : Sort u_1
h : α = β
⊢ Bijective (Eq.mp h)
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Sort u_1
⊢ Bijective (Eq.mp (_ : α = α))
[PROOFSTEP]
refine ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
[GOAL]
α β : Sort u_1
h : α = β
⊢ Bijective (Eq.mpr h)
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Sort u_1
⊢ Bijective (Eq.mpr (_ : α = α))
[PROOFSTEP]
refine ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
[GOAL]
α β : Sort u_1
h : α = β
⊢ Bijective (cast h)
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Sort u_1
⊢ Bijective (cast (_ : α = α))
[PROOFSTEP]
refine ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
[GOAL]
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ HEq (C (g (f a))) (C a)
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ cast (_ : γ (f (g (f a))) = γ (f a)) (C (g (f a))) = C a
[PROOFSTEP]
rw [cast_eq_iff_heq, h]
