awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
⊢ range (hs.piecewise (s := s) f) = ⋃ (i : ι), f i '' s i

Tactic:
ext fun x => ⟨?_, fun ⟨t, ⟨i, hi⟩, ht⟩ ↦ ?_⟩

Premises used: Set.ext, _private.0.IndexedPartition.range_piecewise.match_1, IndexedPartition.piecewise, Membership.mem, Iff.intro, Set.range
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
refine_1 : ∀ x ∈ range (hs.piecewise (s := s) f), Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
refine_2 :
  ∀ (x : β),
    Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x →
      ∀ (t : Set β) (i : ι) (hi : (fun (i : ι) ↦ f i '' s i) i = t) (ht : x ∈ t), x ∈ range (hs.piecewise (s := s) f)
⊢ range (hs.piecewise (s := s) f) = ⋃ (i : ι), f i '' s i

Tactic:
refine ext fun x => ⟨?_, fun ⟨t, ⟨i, hi⟩, ht⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : α
⊢ Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) (hs.piecewise (s := s) f x)

Tactic:
mem_iUnion_of_mem (hs.index x) ⟨x, hs.mem_index x, rfl⟩

Premises used: And.intro, IndexedPartition.index, Set.mem_iUnion_of_mem, Exists.intro, IndexedPartition.mem_index, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : α
⊢ Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) (hs.piecewise (s := s) f x)

Tactic:
exact mem_iUnion_of_mem (hs.index x) ⟨x, hs.mem_index x, rfl⟩
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
ht : x ∈ t
⊢ ∃ x_1 ∈ s i, f i x_1 = x

Tactic:
simp only [← hi, mem_image] at ht

Premises used: Set.mem_image
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
ht : ∃ x_1 ∈ s i, f i x_1 = x
refine_2 : ∀ (a : α) (ha1 : a ∈ s i) (ha2 : f i a = x), x ∈ range (hs.piecewise (s := s) f)
⊢ x ∈ range (hs.piecewise (s := s) f)

Tactic:
obtain ⟨a, ha1, ha2⟩ := ht
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
a : α
ha1 : a ∈ s i
ha2 : f i a = x
⊢ x ∈ range (hs.piecewise (s := s) f)

Tactic:
⟨a, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
a : α
ha1 : a ∈ s i
ha2 : f i a = x
refine_2 : hs.piecewise (s := s) f a = x
⊢ x ∈ range (hs.piecewise (s := s) f)

Tactic:
refine ⟨a, ?_⟩
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
a : α
ha1 : a ∈ s i
ha2 : f i a = x
⊢ hs.index (s := s) a = i

Tactic:
simp only [hs.mem_iff_index_eq] at ha1

Premises used: IndexedPartition.mem_iff_index_eq
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
a : α
ha2 : f i a = x
ha1 : hs.index (s := s) a = i
⊢ hs.piecewise (s := s) f a = x

Tactic:
simpa [hs.mem_iff_index_eq, ← ha1] using ha2

Premises used: IndexedPartition.mem_iff_index_eq
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : x ∈ range (hs.piecewise (s := s) f)
y : α
hy : hs.piecewise (s := s) f y = x
⊢ Membership.mem (γ := Set β) (⋃ (i : ι), range (f i)) x

Tactic:
simpa [IndexedPartition.piecewise_apply] using ⟨hs.index y, y, hy⟩

Premises used: IndexedPartition.piecewise_apply
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
x : α
_i _j : κ
hxi : Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {_i}, s i) x
hxj : Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {_j}, s i) x
obtain : ∀ (a : Set α) (ha : x ∈ a) (c : ι) (hc : (fun (i : ι) ↦ (⋃ (_ : i ∈ g ⁻¹' {_i}), s i : Set α)) c = a), _i = _j
⊢ _i = _j

Tactic:
obtain ⟨a, ⟨c, hc⟩, ha⟩ := hxi
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
x : α
_i _j : κ
hxj : Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {_j}, s i) x
a : Set α
ha : x ∈ a
c : ι
hc : (fun (i : ι) ↦ (⋃ (_ : i ∈ g ⁻¹' {_i}), s i : Set α)) c = a
obtain : ∀ (b : Set α) (hb : x ∈ b) (d : ι) (hd : (fun (i : ι) ↦ (⋃ (_ : i ∈ g ⁻¹' {_j}), s i : Set α)) d = b), _i = _j
⊢ _i = _j

Tactic:
obtain ⟨b, ⟨d, hd⟩, hb⟩ := hxj
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {k}, s i) (hs.some (s := s) (⋯.some (s := g ⁻¹' {k})))

Tactic:
mem_iUnion_of_mem ((singleton_nonempty k).preimage hg).some ?_

Premises used: Set.singleton_nonempty, Set.mem_iUnion_of_mem, Set.Nonempty.preimage, Set.Nonempty.some
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
refine :
  Membership.mem (γ := Set α) (⋃ (_ : ⋯.some (s := g ⁻¹' {k}) ∈ g ⁻¹' {k}), s (⋯.some (s := g ⁻¹' {k})))
    (hs.some (s := s) (⋯.some (s := g ⁻¹' {k})))
⊢ Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {k}, s i) (hs.some (s := s) (⋯.some (s := g ⁻¹' {k})))

Tactic:
refine mem_iUnion_of_mem ((singleton_nonempty k).preimage hg).some ?_

Premises used: Set.singleton_nonempty, Set.mem_iUnion_of_mem, Set.Nonempty.preimage, Set.Nonempty.some
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
simp : g (⋯.some (s := g ⁻¹' {k})) = k ∧ hs.some (s := s) (⋯.some (s := g ⁻¹' {k})) ∈ s (⋯.some (s := g ⁻¹' {k}))
⊢ Membership.mem (γ := Set α) (⋃ (_ : ⋯.some (s := g ⁻¹' {k}) ∈ g ⁻¹' {k}), s (⋯.some (s := g ⁻¹' {k})))
    (hs.some (s := s) (⋯.some (s := g ⁻¹' {k})))

Tactic:
simp only [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
left : g (⋯.some (s := g ⁻¹' {k})) = k
right : hs.some (s := s) (⋯.some (s := g ⁻¹' {k})) ∈ s (⋯.some (s := g ⁻¹' {k}))
⊢ g (⋯.some (s := g ⁻¹' {k})) = k ∧ hs.some (s := s) (⋯.some (s := g ⁻¹' {k})) ∈ s (⋯.some (s := g ⁻¹' {k}))

Tactic:
constructor
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ g (⋯.some (s := g ⁻¹' {k})) = k

Tactic:
simpa using ((singleton_nonempty k).preimage hg).some_mem

Premises used: Set.singleton_nonempty, Set.Nonempty.some_mem, Set.Nonempty.preimage
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some (s := s) (⋯.some (s := g ⁻¹' {k})) ∈ s (⋯.some (s := g ⁻¹' {k}))

Tactic:
hs.some_mem ((singleton_nonempty k).preimage hg).some

Premises used: Set.singleton_nonempty, IndexedPartition.some_mem, Set.Nonempty.preimage, Set.Nonempty.some
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some (s := s) (⋯.some (s := g ⁻¹' {k})) ∈ s (⋯.some (s := g ⁻¹' {k}))

Tactic:
exact hs.some_mem ((singleton_nonempty k).preimage hg).some

Premises used: Set.singleton_nonempty, IndexedPartition.some_mem, Set.Nonempty.preimage, Set.Nonempty.some
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
x : α
⊢ Membership.mem (γ := Set α) (⋃ (_ : hs.index (s := s) x ∈ g ⁻¹' {g (hs.index (s := s) x)}), s (hs.index (s := s) x)) x

Tactic:
simp [hs.mem_index]

Premises used: IndexedPartition.mem_index
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
⊢ mk (β := β) a₁ b₁ = mk (β := β) a₂ b₂ ↔ a₁ = a₂ ∧ b₁ ≍ b₂

Tactic:
simp
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk (β := β) a ∘ f = mk (β := β) b ∘ g
rcases : ∀ (i : γ), a = b ∧ f ≍ g
⊢ a = b ∧ f ≍ g

Tactic:
rcases ‹Nonempty γ› with ⟨i⟩

Premises used: Nonempty
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk (β := β) a ∘ f = mk (β := β) b ∘ g
i : γ
⊢ a = b

Tactic:
congr_arg Sigma.fst (congr_fun h i)

Premises used: Sigma.fst, congr_arg, congr_fun
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk (β := β) a ∘ f = mk (β := β) b ∘ g
i : γ
obtain : ∀ {g : γ → β a} (h : mk (β := β) a ∘ f = mk (β := β) a ∘ g), a = a ∧ f ≍ g
⊢ a = b ∧ f ≍ g

Tactic:
obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)

Premises used: Sigma.fst, congr_arg, congr_fun, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk (β := β) a ∘ f = mk (β := β) a ∘ g
⊢ a = a ∧ f ≍ g

Tactic:
simpa [funext_iff] using h

Premises used: funext_iff
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
p : (a : α) × β a → Prop
⊢ (∀ (x : (a : α) × β a), p x) ↔ ∀ (a : α) (b : β a), p (mk (β := fun (a : α) ↦ β a) a b)

Tactic:
⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩

Premises used: _private.0.Sigma.eta.match_1, Iff.intro, Sigma.mk
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
p : (a : α) × β a → Prop
⊢ (∃ (x : (a : α) × β a), p x) ↔ ∃ (a : α), ∃ (b : β a), p (mk (β := fun (a : α) ↦ β a) a b)

Tactic:
⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩

Premises used: Exists, _private.0.Sigma.exists.match_2, Iff.intro, Exists.intro, _private.0.Sigma.exists.match_1, Sigma.mk
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
p : (a : α) → β a → Prop
⊢ (∃ (a : α), ∃ (b : β a), p a b) ↔
    ∃ (x : (a : α) × β a), p (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))

Tactic:
(Sigma.exists (p := fun x ↦ p x.1 x.2)).symm

Premises used: Sigma.exists, Iff.symm
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
p : (a : α) → β a → Prop
⊢ (∀ (a : α) (b : β a), p a b) ↔
    ∀ (x : (a : α) × β a), p (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))

Tactic:
(Sigma.forall (p := fun x ↦ p x.1 x.2)).symm

Premises used: Sigma.forall, Iff.symm
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Nonempty.{u_4 + 1} (β a)
⊢ Surjective (α := (a : α) × β a) (fst (β := fun (a : α) ↦ β a))

Tactic:
fun a ↦
  let ⟨b⟩ := h a; ⟨⟨a, b⟩, rfl⟩

Premises used: Exists, Sigma.fst, _private.0.Sigma.fst_surjective.match_1, Exists.intro, Sigma.mk, Eq, Function.Surjective, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
⊢ Surjective (α := (a : α) × β a) (fst (β := fun (a : α) ↦ β a)) ↔ ∀ (a : α), Nonempty.{u_4 + 1} (β a)

Tactic:
⟨fun h a ↦ let ⟨x, hx⟩ := h a; hx ▸ ⟨x.2⟩, @fst_surjective _ _⟩

Premises used: Sigma.fst_surjective, _private.0.Sigma.fst_surjective_iff.match_1, Eq.rec, Nonempty.intro, Iff.intro, Nonempty, Sigma.snd
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton.{u_4 + 1} (β a)
a₁ : α
b₁ b₂ : β a₁
⊢ mk (β := fun (a : α) ↦ β a) a₁ b₁ = mk (β := fun (a : α) ↦ β a) a₁ b₂

Tactic:
congr_arg (mk a₁) <| Subsingleton.elim _ _

Premises used: congr_arg, Sigma.mk, Subsingleton.elim
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton.{u_4 + 1} (β a)
a₁ : α
b₁ b₂ : β a₁
⊢ mk (β := fun (a : α) ↦ β a) a₁ b₁ = mk (β := fun (a : α) ↦ β a) a₁ b₂

Tactic:
exact congr_arg (mk a₁) <| Subsingleton.elim _ _

Premises used: congr_arg, Sigma.mk, Subsingleton.elim
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
⊢ Injective (α := (a : α) × β a) (fst (β := fun (a : α) ↦ β a)) ↔ ∀ (a : α), Subsingleton.{u_4 + 1} (β a)

Tactic:
⟨fun h _ ↦ ⟨fun _ _ ↦ sigma_mk_injective <| h rfl⟩, @fst_injective _ _⟩

Premises used: Sigma.fst_injective, Subsingleton.intro, Iff.intro, rfl, sigma_mk_injective
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
x : α₁
y : β₁ x
⊢ map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (mk (β := β₁) x y) = mk (β := β₂) (f₁ x) (f₂ x y)

Tactic:
rfl

Premises used: Sigma.map, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h :
  Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) j y)
⊢ i = j

Tactic:
h₁ (Sigma.mk.inj_iff.mp h).1

Premises used: And.left, Iff.mp, Sigma.mk.inj_iff
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h :
  Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) j y)
obtain :
  ∀ (y : β₁ i)
    (h :
      Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
        Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i y)),
    Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) i y
⊢ Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) j y

Tactic:
obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1

Premises used: And.left, Iff.mp, Sigma.mk.inj_iff, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h :
  Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i y)
⊢ x = y

Tactic:
h₂ i (sigma_mk_injective h)

Premises used: sigma_mk_injective
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h :
  Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i y)
obtain :
  ∀
    (h :
      Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
        Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x)),
    Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) i x
⊢ Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) i y

Tactic:
obtain rfl : x = y := h₂ i (sigma_mk_injective h)

Premises used: rfl, sigma_mk_injective
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
h :
  Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x)
⊢ Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) i x

Tactic:
rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h : Injective (Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂)
a : α₁
⊢ Injective (f₂ a)

Tactic:
fun x y hxy ↦
  sigma_mk_injective <| @h ⟨a, x⟩ ⟨a, y⟩ (Sigma.ext rfl (heq_of_eq hxy))

Premises used: heq_of_eq, Function.Injective, Sigma.ext, rfl, sigma_mk_injective
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
⊢ Injective (Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂) ↔ ∀ (a : α₁), Injective (f₂ a)

Tactic:
⟨fun h ↦ h.of_sigma_map, h₁.sigma_map⟩

Premises used: Function.Injective.sigma_map, Iff.intro, Function.Injective.of_sigma_map
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
simp :
  ∀ (x : α₁) (b : β₂ (f₁ x)),
    ∃ (a : Sigma β₁), Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ a = Sigma.mk (β := fun (a : α₂) ↦ β₂ a) (f₁ x) b
⊢ Surjective (Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂)

Tactic:
simp only [Surjective, Sigma.forall, h₁.forall]

Premises used: Function.Surjective.forall, Sigma.forall, Function.Surjective
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)),
    ∃ (a : Sigma β₁), Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ a = Sigma.mk (β := fun (a : α₂) ↦ β₂ a) (f₁ x) b

Tactic:
fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)),
    ∃ (a : Sigma β₁), Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ a = Sigma.mk (β := fun (a : α₂) ↦ β₂ a) (f₁ x) b

Tactic:
exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
f : (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β))
⊢ uncurry (β := β) (γ := γ) (curry (β := β) (γ := γ) f) = f

Tactic:
funext fun ⟨_, _⟩ ↦ rfl

Premises used: Sigma.uncurry, _private.0.Sigma.uncurry_curry.match_1, funext, Sigma.curry, Eq, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
f : (x : α) → (y : β x) → γ x y
⊢ curry (β := β) (γ := γ) (uncurry (β := β) (γ := γ) f) = f

Tactic:
rfl

Premises used: Sigma.uncurry, Sigma.curry, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
i : (a : α) × β a
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
x : γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
obtain :
  ∀ (ia : α) (ib : β ia)
    (x :
      γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))),
    curry (β := fun (a : α) ↦ β a) (γ := γ)
        (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
          (mk (β := fun (a : α) ↦ β a) ia ib) x) =
      update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
        ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
        (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
          (curry (β := fun (a : α) ↦ β a) (γ := γ) f ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
          ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
⊢ curry (β := fun (a : α) ↦ β a) (γ := γ)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f i
        x) =
    update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
      (i.fst (β := fun (a : α) ↦ β a))
      (update (β := γ (i.fst (β := fun (a : α) ↦ β a)))
        (curry (β := fun (a : α) ↦ β a) (γ := γ) f (i.fst (β := fun (a : α) ↦ β a))) (i.snd (β := fun (a : α) ↦ β a)) x)

Tactic:
obtain ⟨ia, ib⟩ := i
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
h :
  ∀ (ja : α) (jb : β ja),
    curry (β := fun (a : α) ↦ β a) (γ := γ)
        (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
          (mk (β := fun (a : α) ↦ β a) ia ib) x)
        ja jb =
      update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
        ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
        (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
          (curry (β := fun (a : α) ↦ β a) (γ := γ) f ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
          ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
        ja jb
⊢ curry (β := fun (a : α) ↦ β a) (γ := γ)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x) =
    update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (curry (β := fun (a : α) ↦ β a) (γ := γ) f ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)

Tactic:
ext ja jb