internlm/Lean-Github huggingface dataset:
Theorem: Set.image_update
Proof state before:
case neg.refine_1
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ f x = update f a b x
Tactic:
rw [update_noteq]
Proof state after:
case neg.refine_1.h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a
Theorem: Set.image_update
Proof state before:
case neg.refine_1.h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a
Tactic:
rintro rfl
Proof state after:
case neg.refine_1.h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False
Theorem: Set.image_update
Proof state before:
case neg.refine_1.h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False
Tactic:
exact h hxs
Proof state after:
no goals
Theorem: Set.preimage_update_of_not_mem_not_mem
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
⊢ update f a b ⁻¹' s = f ⁻¹' s
Tactic:
ext x
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s
Theorem: Set.preimage_update_of_not_mem_not_mem
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s
Tactic:
simp only [mem_preimage, update_apply]
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ (if x = a then b else f x) ∈ s ↔ f x ∈ s
Theorem: Set.preimage_update_of_not_mem_not_mem
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ (if x = a then b else f x) ∈ s ↔ f x ∈ s
Tactic:
split_ifs with h
Proof state after:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : x = a
⊢ b ∈ s ↔ f x ∈ s

case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ s
Theorem: Set.preimage_update_of_not_mem_not_mem
Proof state before:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : x = a
⊢ b ∈ s ↔ f x ∈ s

case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ s
Tactic:
simp [hbs, h.symm ▸ has]
Proof state after:
case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ s
Theorem: Set.preimage_update_of_not_mem_not_mem
Proof state before:
case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ s
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.preimage_update_of_not_mem_mem
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∈ s
⊢ update f a b ⁻¹' s = f ⁻¹' s \ {a}
Tactic:
ext x
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∈ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s \ {a}
Theorem: Set.preimage_update_of_not_mem_mem
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∈ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s \ {a}
Tactic:
obtain (rfl | hxa) := eq_or_ne x a
Proof state after:
case h.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
b : β
f : α → β
s : Set β
hbs : b ∉ s
x : α
has : f x ∈ s
⊢ x ∈ update f x b ⁻¹' s ↔ x ∈ f ⁻¹' s \ {x}

case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s \ {a}
Theorem: Set.preimage_update_of_not_mem_mem
Proof state before:
case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∉ s
has : f a ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s \ {a}
Tactic:
simp [hxa]
Proof state after:
no goals
Theorem: Set.preimage_update_of_not_mem_mem
Proof state before:
case h.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
b : β
f : α → β
s : Set β
hbs : b ∉ s
x : α
has : f x ∈ s
⊢ x ∈ update f x b ⁻¹' s ↔ x ∈ f ⁻¹' s \ {x}
Tactic:
simpa
Proof state after:
no goals
Theorem: Set.preimage_update_of_mem
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
⊢ update f a b ⁻¹' s = insert a (f ⁻¹' s)
Tactic:
ext x
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)
Theorem: Set.preimage_update_of_mem
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)
Tactic:
obtain (rfl | hxa) := eq_or_ne x a
Proof state after:
case h.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
⊢ x ∈ update f x b ⁻¹' s ↔ x ∈ insert x (f ⁻¹' s)

case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)
Theorem: Set.preimage_update_of_mem
Proof state before:
case h.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
⊢ x ∈ update f x b ⁻¹' s ↔ x ∈ insert x (f ⁻¹' s)

case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)
Tactic:
simpa
Proof state after:
case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)
Theorem: Set.preimage_update_of_mem
Proof state before:
case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)
Tactic:
simp [hxa]
Proof state after:
no goals
Theorem: Set.preimage_update_eq_ite
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
⊢ update f a b ⁻¹' s = if b ∈ s then insert a (f ⁻¹' s) else if f a ∈ s then f ⁻¹' s \ {a} else f ⁻¹' s
Tactic:
split_ifs with hb ha
Proof state after:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∈ s
⊢ update f a b ⁻¹' s = insert a (f ⁻¹' s)

case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∈ s
⊢ update f a b ⁻¹' s = f ⁻¹' s \ {a}

case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∉ s
⊢ update f a b ⁻¹' s = f ⁻¹' s
Theorem: Set.preimage_update_eq_ite
Proof state before:
case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∉ s
⊢ update f a b ⁻¹' s = f ⁻¹' s
Tactic:
rw [preimage_update_of_not_mem_not_mem _ hb ha]
Proof state after:
no goals
Theorem: Set.preimage_update_eq_ite
Proof state before:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∈ s
⊢ update f a b ⁻¹' s = insert a (f ⁻¹' s)
Tactic:
rw [preimage_update_of_mem _ hb]
Proof state after:
no goals
Theorem: Set.preimage_update_eq_ite
Proof state before:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∈ s
⊢ update f a b ⁻¹' s = f ⁻¹' s \ {a}
Tactic:
rw [preimage_update_of_not_mem_mem _ hb ha]
Proof state after:
no goals
Theorem: Set.image_update_id_apply
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
f : α → β
a : α
b : β
x y : α
s : Set α
inst✝ : Decidable (x ∈ s)
⊢ update id x y '' s = if x ∉ s then s else insert y (s \ {x})
Tactic:
simp
Proof state after:
no goals
Theorem: Set.update_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
⊢ Injective (update f a b)
Tactic:
rintro x y hy
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : update f a b x = update f a b y
⊢ x = y
Theorem: Set.update_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : update f a b x = update f a b y
⊢ x = y
Tactic:
rw [update_apply, update_apply] at hy
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : (if x = a then b else f x) = if y = a then b else f y
⊢ x = y
Theorem: Set.update_injective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : (if x = a then b else f x) = if y = a then b else f y
⊢ x = y
Tactic:
split_ifs at hy with h_1 h_2
Proof state after:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : y = a
hy : b = b
⊢ x = y

case neg
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : ¬y = a
hy : b = f y
⊢ x = y

case pos
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : y = a
hy : f x = b
⊢ x = y

case neg
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : ¬y = a
hy : f x = f y
⊢ x = y
Theorem: Set.update_injective
Proof state before:
case neg
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : ¬y = a
hy : f x = f y
⊢ x = y
Tactic:
exact hf.eq_iff.1 hy
Proof state after:
no goals
Theorem: Set.update_injective
Proof state before:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : y = a
hy : b = b
⊢ x = y
Tactic:
rw [h_1,h_2]
Proof state after:
no goals
Theorem: Set.update_injective
Proof state before:
case neg
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : ¬y = a
hy : b = f y
⊢ x = y
Tactic:
exact (h ⟨y, hy.symm⟩).elim
Proof state after:
no goals
Theorem: Set.update_injective
Proof state before:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : y = a
hy : f x = b
⊢ x = y
Tactic:
exact (h ⟨x, hy⟩).elim
Proof state after:
no goals
Theorem: Set.update_injOn_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
⊢ InjOn (update f a b) s ↔ InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
Tactic:
refine ⟨fun h ↦ ⟨fun x hx y hy hxy ↦  h hx.1 hy.1 ?_, ?_⟩, fun h x hx y hy hxy ↦ ?_⟩
Proof state after:
case refine_1
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
x : α
hx : x ∈ s \ {a}
y : α
hy : y ∈ s \ {a}
hxy : f x = f y
⊢ update f a b x = update f a b y

case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
⊢ a ∈ s → ∀ x ∈ s, f x = b → x = a

case refine_3
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
⊢ x = y
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
⊢ x = y
Tactic:
obtain (rfl | hxa) := eq_or_ne x a
Proof state after:
case refine_3.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
⊢ x = y

case refine_3.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
⊢ x = y
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
⊢ x = y
Tactic:
obtain (rfl | hya) := eq_or_ne y a
Proof state after:
case refine_3.inr.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : update f y b x = update f y b y
hxa : x ≠ y
⊢ x = y

case refine_3.inr.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inr.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y
Tactic:
rw [update_noteq hxa, update_noteq hya] at hxy
Proof state after:
case refine_3.inr.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x = f y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inr.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x = f y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y
Tactic:
exact h.1 ⟨hx, hxa⟩ ⟨hy, hya⟩ hxy
Proof state after:
no goals
Theorem: Set.update_injOn_iff
Proof state before:
case refine_1
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
x : α
hx : x ∈ s \ {a}
y : α
hy : y ∈ s \ {a}
hxy : f x = f y
⊢ update f a b x = update f a b y
Tactic:
rwa [update_noteq hx.2, update_noteq hy.2]
Proof state after:
no goals