α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) ↔ r = 1 ∧ ¬s = univ ∨ ∃ x, x ∈ s ∧ f x = r
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ r ∈ range (mulIndicator s f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s
simp only [mem_range, mulIndicator, ne_eq, mem_image]
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) ↔ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) ↔ r = 1 ∧ ¬s = univ ∨ ∃ x, x ∈ s ∧ f x = r
rw [eq_univ_iff_forall, not_forall]
case refine_1
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) → (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r

case refine_2
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ ((r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r) → ∃ y, (if y ∈ s then f y else 1) = r
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) ↔ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
refine ⟨?_, ?_⟩
case refine_1.intro
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hy : (if y ∈ s then f y else 1) = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
case refine_1
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) → (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
rintro ⟨y, hy⟩
case refine_1.intro.inl
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : y ∈ s
hy : f y = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r

case refine_1.intro.inr
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : ¬y ∈ s
hy : 1 = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
case refine_1.intro
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hy : (if y ∈ s then f y else 1) = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
split_ifs at hy with hys
no goals
case refine_1.intro.inl
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : y ∈ s
hy : f y = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
tauto
case refine_1.intro.inr.h
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : ¬y ∈ s
hy : 1 = r
⊢ r = 1 ∧ ∃ x, ¬x ∈ s
case refine_1.intro.inr
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : ¬y ∈ s
hy : 1 = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
left
no goals
case refine_1.intro.inr.h
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : ¬y ∈ s
hy : 1 = r
⊢ r = 1 ∧ ∃ x, ¬x ∈ s
tauto
no goals
case refine_2
α : Type u_1
β : Type ?u.36476
ι : Type ?u.36479
M : Type u_2
N : Type ?u.36485
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ ((r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r) → ∃ y, (if y ∈ s then f y else 1) = r
rintro (⟨hr, ⟨x, hx⟩⟩ | ⟨x, ⟨hx, hxs⟩⟩) <;> use x <;> split_ifs <;> tauto