case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.84669
ι : Sort ?u.84672
π : α → Type ?u.84677
δ : α → Sort ?u.84682
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (piecewise s f₁ f₂) (s₁ ∩ s)

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.84669
ι : Sort ?u.84672
π : α → Type ?u.84677
δ : α → Sort ?u.84682
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₂ (piecewise s f₁ f₂) (s₂ ∩ sᶜ)
α : Type u_1
β : Type u_2
γ : Type ?u.84669
ι : Sort ?u.84672
π : α → Type ?u.84677
δ : α → Sort ?u.84682
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (piecewise s f₁ f₂) (Set.ite s s₁ s₂) (Set.ite t t₁ t₂)
refine' (h₁.congr _).union_union (h₂.congr _)
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.84669
ι : Sort ?u.84672
π : α → Type ?u.84677
δ : α → Sort ?u.84682
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (piecewise s f₁ f₂) (s₁ ∩ s)

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.84669
ι : Sort ?u.84672
π : α → Type ?u.84677
δ : α → Sort ?u.84682
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₂ (piecewise s f₁ f₂) (s₂ ∩ sᶜ)
exacts [(piecewise_eqOn s f₁ f₂).symm.mono (inter_subset_right _ _),
  (piecewise_eqOn_compl s f₁ f₂).symm.mono (inter_subset_right _ _)]