awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
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₂ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₂ ∩ sᶜ)

Tactic:
(piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right

Premises used: Set.piecewise_eqOn_compl, Set.EqOn.symm, Set.EqOn.mono, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
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₁ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₁ ∩ s)

Tactic:
exacts [(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right,
    (piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right]

Premises used: Set.piecewise_eqOn, Set.piecewise_eqOn_compl, Set.EqOn.symm, Set.EqOn.mono, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
simp :
  (∀ ⦃x : α⦄, x ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' x = g x) ↔
    ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)
⊢ EqOn (s.piecewise (β := fun (a : α) ↦ β) f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)

Tactic:
simp only [EqOn, ← forall_and]

Premises used: Set.EqOn, forall_and
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ (∀ ⦃x : α⦄, x ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' x = g x) ↔
    ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)

Tactic:
forall_congr' fun a => ?_

Premises used: forall_congr'
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
refine :
  ∀ (a : α),
    a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
⊢ (∀ ⦃x : α⦄, x ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' x = g x) ↔
    ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)

Tactic:
refine forall_congr' fun a => ?_

Premises used: forall_congr'
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
pos :
  a ∈ s →
    (a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a))
neg :
  ¬a ∈ s →
    (a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a))
⊢ a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

Tactic:
by_cases a ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h : a ∈ s
⊢ a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h : ¬a ∈ s
⊢ a ∈ t → s.piecewise (β := fun (a : α) ↦ β) f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t t' : Set α
h : EqOn f g (t ∩ s)
h' : EqOn f' g (t' ∩ sᶜ)
⊢ EqOn (s.piecewise (β := fun (a : α) ↦ β) f f') g (s.ite t t')

Tactic:
simp [eqOn_piecewise, *]

Premises used: Set.eqOn_piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t t' : Set α
h : EqOn f g t
h' : EqOn f' g t'
⊢ EqOn (s.piecewise (β := fun (a : α) ↦ β) f f') g (s.ite t t')

Tactic:
(h.mono inter_subset_left).piecewise_ite' s (h'.mono inter_subset_left)

Premises used: Set.EqOn.piecewise_ite', Set.inter_subset_left, Set.EqOn.mono
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
pos : x ∈ s → (x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t))
neg : ¬x ∈ s → (x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t))
⊢ x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
by_cases x ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h : x ∈ s
⊢ x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
simp [*, Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h : ¬x ∈ s
⊢ x ∈ s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
simp [*, Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
pos :
  ∀ (hx : x ∈ s),
    h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x
neg :
  ∀ (hx : ¬x ∈ s),
    h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x
⊢ h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise (β := δ) f g x) = s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) (fun (x : α) ↦ h x (g x)) x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
pos :
  ∀ (hx : x ∈ s),
    h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
      s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x
neg :
  ∀ (hx : ¬x ∈ s),
    h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
      s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x
⊢ h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
    s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
    s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x) =
    s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) (fun (x : α) ↦ h x (g x) (g' x)) x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
⊢ Eq (α := (i : α) → δ' i) (s.piecewise (β := δ') (fun (x : α) ↦ h x (f x)) fun (x : α) ↦ h x (g x)) fun (x : α) ↦
    h x (s.piecewise (β := δ) f g x)

Tactic:
funext fun _ => (apply_piecewise _ _ _ _).symm

Premises used: funext, Eq.symm, Set.apply_piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
⊢ Eq (α := (i : α) → δ'' i) (s.piecewise (β := δ'') (fun (x : α) ↦ h x (f x) (f' x)) fun (x : α) ↦ h x (g x) (g' x))
    fun (x : α) ↦ h x (s.piecewise (β := δ) f g x) (s.piecewise (β := δ') f' g' x)

Tactic:
funext fun _ => (apply_piecewise₂ _ _ _ _ _ _).symm

Premises used: funext, Set.apply_piecewise₂, Eq.symm
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
h : ∀ (x : α), s.piecewise (β := δ) f f x = f x
⊢ s.piecewise (β := δ) f f = f

Tactic:
ext x
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
x : α
pos : ∀ (hx : x ∈ s), s.piecewise (β := δ) f f x = f x
neg : ∀ (hx : ¬x ∈ s), s.piecewise (β := δ) f f x = f x
⊢ s.piecewise (β := δ) f f x = f x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
x : α
hx : x ∈ s
⊢ s.piecewise (β := δ) f f x = f x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
x : α
hx : ¬x ∈ s
⊢ s.piecewise (β := δ) f f x = f x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
h : ∀ (y : β), y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) ↔ y ∈ f '' s ∪ g '' sᶜ
⊢ range (s.piecewise (β := fun (a : α) ↦ β) f g) = f '' s ∪ g '' sᶜ

Tactic:
ext y
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
h : y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) → y ∈ f '' s ∪ g '' sᶜ
h₁ : y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g)
⊢ y ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g) ↔ y ∈ f '' s ∪ g '' sᶜ

Tactic:
constructor
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
pos : ∀ (h : x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
neg : ∀ (h : ¬x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
by_cases h : x ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
pos : s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
left
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
neg : s.piecewise (β := fun (a : α) ↦ β) f g x ∈ g '' sᶜ
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
right
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
pos : ∀ (h : x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s
neg : ∀ (h : ¬x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ g '' sᶜ
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
by_cases h : x ∈ s <;> [left; right]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
h₁ : x ∈ s ∧ f x = s.piecewise (β := fun (a : α) ↦ β) f g x
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s

Tactic:
use x
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
h₁ : x ∈ sᶜ ∧ g x = s.piecewise (β := fun (a : α) ↦ β) f g x
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ g '' sᶜ

Tactic:
use x
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ x ∈ s ∧ f x = s.piecewise (β := fun (a : α) ↦ β) f g x

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ ∧ g x = s.piecewise (β := fun (a : α) ↦ β) f g x

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
h : s.piecewise (β := fun (a : α) ↦ β) f g x = f x
⊢ f x ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g)

Tactic:
use x
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
h : s.piecewise (β := fun (a : α) ↦ β) f g x = g x
⊢ g x ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g)

Tactic:
use x
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x = f x

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x = g x

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
rw :
  (InjOn f s ∧
      InjOn g sᶜ ∧
        ∀ (x : α),
          x ∈ s →
            ∀ (y : α), y ∈ sᶜ → s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
⊢ Injective (s.piecewise (β := fun (a : α) ↦ β) f g) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
rw [← injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
    (piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]

Premises used: Set.piecewise_eqOn, Set.union_compl_self, Set.EqOn.injOn_iff, Set.piecewise_eqOn_compl, Set.injOn_union, disjoint_compl_right, Set.injOn_univ
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧
      InjOn g sᶜ ∧
        ∀ (x : α),
          x ∈ s →
            ∀ (y : α), y ∈ sᶜ → s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)

Premises used: Iff.rfl, and_congr, forall₄_congr
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
refine :
  ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ sᶜ),
    s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y
⊢ (InjOn f s ∧
      InjOn g sᶜ ∧
        ∀ (x : α),
          x ∈ s →
            ∀ (y : α), y ∈ sᶜ → s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
refine and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)

Premises used: Iff.rfl, and_congr, forall₄_congr
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
rw : f x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y
rw₁ rw₂ : f x ≠ g y ↔ f x ≠ g y
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y

Tactic:
rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_notMem s f g hy]

Premises used: Set.piecewise_eq_of_notMem, Set.piecewise_eq_of_mem
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
s : Set α
inst : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi (α := δ) t'
hg : g ∈ t.pi (α := δ) t'
i : α
ht : i ∈ t
pos : ∀ (hs : i ∈ s), s.piecewise (β := δ) f g i ∈ t' i
neg : ∀ (hs : ¬i ∈ s), s.piecewise (β := δ) f g i ∈ t' i
⊢ s.piecewise (β := δ) f g i ∈ t' i

Tactic:
by_cases hs : i ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
s : Set α
inst : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi (α := δ) t'
hg : g ∈ t.pi (α := δ) t'
i : α
ht : i ∈ t
hs : i ∈ s
⊢ s.piecewise (β := δ) f g i ∈ t' i

Tactic:
simp [hf i ht, hg i ht, hs]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
s : Set α
inst : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi (α := δ) t'
hg : g ∈ t.pi (α := δ) t'
i : α
ht : i ∈ t
hs : ¬i ∈ s
⊢ s.piecewise (β := δ) f g i ∈ t' i

Tactic:
simp [hf i ht, hg i ht, hs]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
ι : Type u_8
α : ι → Type u_9
s s' : Set ι
t t' : (i : ι) → Set (α i)
inst : (x : ι) → Decidable (x ∈ s')
⊢ s.pi (α := α) (s'.piecewise (β := fun (i : ι) ↦ Set (α i)) t t') = (s ∩ s').pi (α := α) t ∩ (s \ s').pi (α := α) t'

Tactic:
pi_if _ _ _

Premises used: Set.diff, setOf, Set.inter, Set.pi_if, Set.piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
ι : Type u_8
α : ι → Type u_9
s : Set ι
t t' : (i : ι) → Set (α i)
inst : (x : ι) → Decidable (x ∈ s)
⊢ pi (α := α) univ (s.piecewise (β := fun (i : ι) ↦ Set (α i)) t t') = s.pi (α := α) t ∩ sᶜ.pi (α := α) t'

Tactic:
simp [compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Data.Set.Piecewise
Goal:
ι : Type u_8
α : ι → Type u_9
s : Set ι
t : (i : ι) → Set (α i)
inst : (x : ι) → Decidable (x ∈ s)
⊢ pi (α := α) univ (s.piecewise (β := fun (i : ι) ↦ Set (α i)) t fun (x : ι) ↦ univ) = s.pi (α := α) t

Tactic:
simp
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : MulAction α β
inst_2 : One γ
c : α
f : β → γ
h :
  ∀ (x : β),
    Membership.mem (γ := Set β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • mulSupport f
⊢ (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • mulSupport f

Tactic:
ext x
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : MulAction α β
inst_2 : One γ
c : α
f : β → γ
x : β
⊢ Membership.mem (γ := Set β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • mulSupport f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem, mem_mulSupport]

Premises used: Function.mem_mulSupport, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : MulAction α β
inst_2 : Zero γ
c : α
f : β → γ
h : ∀ (x : β), Membership.mem (γ := Set β) (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • support f
⊢ (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • support f

Tactic:
ext x
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : MulAction α β
inst_2 : Zero γ
c : α
f : β → γ
x : β
⊢ Membership.mem (γ := Set β) (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • support f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem, mem_support]

Premises used: Function.mem_support, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : GroupWithZero α
inst_1 : MulAction α β
inst_2 : One γ
c : α
hc : c ≠ 0
f : β → γ
h :
  ∀ (x : β),
    Membership.mem (γ := Set β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • mulSupport f
⊢ (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • mulSupport f

Tactic:
ext x
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : GroupWithZero α
inst_1 : MulAction α β
inst_2 : One γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ Membership.mem (γ := Set β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • mulSupport f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_mulSupport]

Premises used: Function.mem_mulSupport, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : GroupWithZero α
inst_1 : MulAction α β
inst_2 : Zero γ
c : α
hc : c ≠ 0
f : β → γ
h : ∀ (x : β), Membership.mem (γ := Set β) (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • support f
⊢ (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • support f

Tactic:
ext x
-- Module: Mathlib.Data.Set.Pointwise.Support
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : GroupWithZero α
inst_1 : MulAction α β
inst_2 : Zero γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ Membership.mem (γ := Set β) (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • support f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_support]

Premises used: Function.mem_support, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : Finset α
rw : Membership.mem (γ := Set (Finset α)) {s : Finset α | #s = n} s ↔ #s = n
rw₁ rw₂ : #s = n ↔ #s = n
⊢ s ∈ powersetCard α n ↔ #s = n

Tactic:
rw [powersetCard, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.powersetCard
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑(↑s : Finset α) : Set α) = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
a : α
⊢ a ∈ (↑s : Finset α) ↔ a ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
⊢ #(↑s : Finset α) = n

Tactic:
s.prop

Premises used: Set.Mem, setOf, Subtype.prop, Set.powersetCard
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).ncard = n
rw₁ : #(↑s : Finset α) = n
rw₂ rw₃ : n = n
⊢ (↑s : Set α).ncard = n

Tactic:
rw [← coe_coe, Set.ncard_coe_finset, s.prop]

Premises used: Set.powersetCard.coe_coe, Subtype.prop, Set.ncard_coe_finset
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nonempty ↔ 1 ≤ n
rw₁ : (↑s : Finset α).Nonempty ↔ 1 ≤ n
rw₂ : 1 ≤ #(↑s : Finset α) ↔ 1 ≤ n
rw₃ rw₄ : 1 ≤ n ↔ 1 ≤ n
⊢ (↑s : Set α).Nonempty ↔ 1 ≤ n

Tactic:
rw [← Set.powersetCard.coe_coe, Finset.coe_nonempty, ← one_le_card, s.prop]

Premises used: Finset.coe_nonempty, Set.powersetCard.coe_coe, Subtype.prop, Finset.one_le_card
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nontrivial ↔ 1 < n
rw₁ : (↑s : Finset α).Nontrivial ↔ 1 < n
rw₂ : 1 < #(↑s : Finset α) ↔ 1 < n
rw₃ rw₄ : 1 < n ↔ 1 < n
⊢ (↑s : Set α).Nontrivial ↔ 1 < n

Tactic:
rw [← coe_coe, Finset.nontrivial_coe, ← one_lt_card_iff_nontrivial, card_eq]

Premises used: Finset.one_lt_card_iff_nontrivial, Set.powersetCard.coe_coe, Finset.nontrivial_coe, Set.powersetCard.card_eq