awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
x : α ⊕ β
b : β
inl :
  ∀ (val : α),
    Sum.inl val = Sum.inr b ↔ ∃ (h : isRight.{u, v} (β := β) (Sum.inl val) = true), getRight (Sum.inl val) h = b
inr :
  ∀ (val : β),
    Eq (α := α ⊕ β) (Sum.inr val) (Sum.inr b) ↔
      ∃ (h : isRight.{u, v} (α := α) (Sum.inr val) = true), getRight (Sum.inr val) h = b
⊢ x = Sum.inr b ↔ ∃ (h : x.isRight = true), x.getRight h = b

Tactic:
cases x
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
b : β
val : α
⊢ inl val = inr b ↔ ∃ (h : isRight.{u, v} (β := β) (inl val) = true), getRight (inl val) h = b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
b val : β
⊢ Eq (α := α ⊕ β) (inr val) (inr b) ↔ ∃ (h : isRight.{u, v} (α := α) (inr val) = true), getRight (inr val) h = b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isLeft = true
h₂ : x.getLeft?.isSome = true
⊢ x.getLeft h₁ = x.getLeft?.get h₂

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isRight = true
h₂ : x.getRight?.isSome = true
⊢ x.getRight h₁ = x.getRight?.get h₂

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
x : α ⊕ β
⊢ x.getLeft?.isSome = true ↔ x.isLeft = true

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
x : α ⊕ β
⊢ x.getRight?.isSome = true ↔ x.isRight = true

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq α
inst_1 : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ x = Sum.elim (update (β := fun (a : α) ↦ γ) f i x) g (inl i)

Tactic:
simp
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq α
inst_1 : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inl i → Sum.elim f g x_1 = Sum.elim (update (β := fun (a : α) ↦ γ) f i x) g x_1

Tactic:
simp +contextual
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq β
inst_1 : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ x = Sum.elim f (update (β := fun (a : β) ↦ γ) g i x) (inr i)

Tactic:
simp
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq β
inst_1 : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inr i → Sum.elim f g x_1 = Sum.elim f (update (β := fun (a : β) ↦ γ) g i x) x_1

Tactic:
simp +contextual
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq α
inst_1 : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i : α
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inl i) x ∘ inl = update (β := fun (a : α) ↦ γ) (f ∘ inl) i x

Tactic:
update_comp_eq_of_injective _ inl_injective _ _

Premises used: Sum.inl_injective, Function.update_comp_eq_of_injective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq α
inst_1 : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : α
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inl i) x (inl j) = update (β := fun (a : α) ↦ γ) (f ∘ inl) i x j

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i : α
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inl i) x ∘ inr = f ∘ inr

Tactic:
(update_comp_eq_of_forall_ne _ _) fun _ ↦ inr_ne_inl

Premises used: Function.update_comp_eq_of_forall_ne, Sum.inr_ne_inl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i : α
j : β
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inl i) x (inr j) = f (inr j)

Tactic:
Function.update_of_ne inr_ne_inl ..

Premises used: Sum.inr_ne_inl, Function.update_of_ne
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i : β
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x ∘ inl = f ∘ inl

Tactic:
(update_comp_eq_of_forall_ne _ _) fun _ ↦ inl_ne_inr

Premises used: Sum.inl_ne_inr, Function.update_comp_eq_of_forall_ne
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i : α
j : β
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inr j) x (inl i) = f (inl i)

Tactic:
Function.update_of_ne inl_ne_inr ..

Premises used: Sum.inl_ne_inr, Function.update_of_ne
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq β
inst_1 : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i : β
x : γ
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x ∘ inr = update (β := fun (a : β) ↦ γ) (f ∘ inr) i x

Tactic:
update_comp_eq_of_injective _ inr_injective _ _

Premises used: Sum.inr_injective, Function.update_comp_eq_of_injective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : DecidableEq β
inst_1 : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
rw : update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = (update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x ∘ inr) j
rw₁ rw₂ : update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j)
⊢ update (β := fun (a : α ⊕ β) ↦ γ) f (inr i) x (inr j) = update (β := fun (a : β) ↦ γ) (f ∘ inr) i x j

Tactic:
rw [← update_inr_comp_inr, Function.comp_apply]

Premises used: Function.comp_apply, Sum.update_inr_comp_inr
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : α ⊕ β → Type u_3
inst : DecidableEq α
inst_1 : DecidableEq (α ⊕ β)
f : (i : α ⊕ β) → γ i
i : α
x : γ (inl i)
j : α
⊢ Eq (α := γ (inl j)) (update (β := γ) f (inl i) x (inl j))
    (update (β := fun (j : α) ↦ γ (inl j)) (fun (j : α) ↦ f (inl j)) i x j)

Tactic:
Function.update_apply_of_injective f Sum.inl_injective i x j

Premises used: Function.update_apply_of_injective, Sum.inl_injective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : α ⊕ β → Type u_3
inst : DecidableEq β
inst_1 : DecidableEq (α ⊕ β)
f : (i : α ⊕ β) → γ i
i : β
x : γ (inr i)
j : β
⊢ Eq (α := γ (inr j)) (update (β := γ) f (inr i) x (inr j))
    (update (β := fun (j : β) ↦ γ (inr j)) (fun (j : β) ↦ f (inr j)) i x j)

Tactic:
Function.update_apply_of_injective f Sum.inr_injective i x j

Premises used: Function.update_apply_of_injective, Sum.inr_injective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : (a : α) → γ (inl a)
g : (b : β) → γ (inr b)
a : α
x : γ (inl a)
⊢ (fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) (update (β := fun (val : α) ↦ γ (inl val)) f a x) g t) =
    update (β := γ) (fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) f g t) (inl a) x

Tactic:
Function.rec_update Sum.inl_injective (Sum.rec · g) (fun _ _ => rfl) (fun
    | _, _, .inl _, h => (h _ rfl).elim
    | _, _, .inr _, _ => rfl) _ _ _

Premises used: False.elim, Sum.inl_injective, Function.rec_update, Eq, _private.0.Sum.rec_update_left.match_1, rfl, Sum.rec
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : (a : α) → γ (inl a)
g : (b : β) → γ (inr b)
b : β
x : γ (inr b)
⊢ (fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) f (update (β := fun (val : β) ↦ γ (inr val)) g b x) t) =
    update (β := γ) (fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) f g t) (inr b) x

Tactic:
Function.rec_update Sum.inr_injective (Sum.rec f) (fun _ _ => rfl) (fun
    | _, _, .inr _, h => (h _ rfl).elim
    | _, _, .inl _, _ => rfl) _ _ _

Premises used: Sum.inr_injective, False.elim, Function.rec_update, _private.0.Sum.rec_update_right.match_1, Eq, rfl, Sum.rec
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Sort u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → γ
g : β → γ
a : α
x : γ
⊢ Sum.elim (update (β := fun (a : α) ↦ γ) f a x) g = update (β := fun (a : α ⊕ β) ↦ γ) (Sum.elim f g) (inl a) x

Tactic:
rec_update_left _ _ _ _

Premises used: Sum.rec_update_left, Sum.elim
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Sort u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → γ
g : β → γ
b : β
x : γ
⊢ Sum.elim f (update (β := fun (a : β) ↦ γ) g b x) = update (β := fun (a : α ⊕ β) ↦ γ) (Sum.elim f g) (inr b) x

Tactic:
rec_update_right _ _ _ _

Premises used: Sum.rec_update_right, Sum.elim
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
⊢ Function.LeftInverse (α := β ⊕ α) swap swap

Tactic:
swap_swap

Premises used: Function.LeftInverse, Sum.swap_swap
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
⊢ Function.RightInverse (α := β ⊕ α) swap swap

Tactic:
swap_swap

Premises used: Function.LeftInverse, Sum.swap_swap, Function.RightInverse
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
inl :
  ∀ {a : α} {c : γ}, r a c → (isLeft.{u, v} (β := β) (Sum.inl a) = true ↔ isLeft.{u_1, u_2} (β := δ) (Sum.inl c) = true)
inr :
  ∀ {b : β} {d : δ}, s b d → (isLeft.{u, v} (α := α) (Sum.inr b) = true ↔ isLeft.{u_1, u_2} (α := γ) (Sum.inr d) = true)
⊢ x.isLeft = true ↔ y.isLeft = true

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a : α
c : γ
h : r a c
⊢ isLeft.{u, v} (β := β) (inl a) = true ↔ isLeft.{u_1, u_2} (β := δ) (inl c) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b : β
d : δ
h : s b d
⊢ isLeft.{u, v} (α := α) (inr b) = true ↔ isLeft.{u_1, u_2} (α := γ) (inr d) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
inl :
  ∀ {a : α} {c : γ},
    r a c → (isRight.{u, v} (β := β) (Sum.inl a) = true ↔ isRight.{u_1, u_2} (β := δ) (Sum.inl c) = true)
inr :
  ∀ {b : β} {d : δ},
    s b d → (isRight.{u, v} (α := α) (Sum.inr b) = true ↔ isRight.{u_1, u_2} (α := γ) (Sum.inr d) = true)
⊢ x.isRight = true ↔ y.isRight = true

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a : α
c : γ
h : r a c
⊢ isRight.{u, v} (β := β) (inl a) = true ↔ isRight.{u_1, u_2} (β := δ) (inl c) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b : β
d : δ
h : s b d
⊢ isRight.{u, v} (α := α) (inr b) = true ↔ isRight.{u_1, u_2} (α := γ) (inr d) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
c : γ
h : LiftRel r s x (Sum.inl c)
inl : ∀ {a : α}, r a c → isLeft.{u, v} (β := β) (Sum.inl a) = true
⊢ x.isLeft = true

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
c : γ
a : α
h : r a c
⊢ isLeft.{u, v} (β := β) (inl a) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
a : α
h : LiftRel r s (Sum.inl a) y
inl : ∀ {c : γ}, r a c → isLeft.{u_1, u_2} (β := δ) (Sum.inl c) = true
⊢ y.isLeft = true

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a : α
c : γ
h : r a c
⊢ isLeft.{u_1, u_2} (β := δ) (inl c) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
d : δ
h : LiftRel r s x (Sum.inr d)
inr : ∀ {b : β}, s b d → isRight.{u, v} (α := α) (Sum.inr b) = true
⊢ x.isRight = true

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
d : δ
b : β
h : s b d
⊢ isRight.{u, v} (α := α) (inr b) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
b : β
h : LiftRel r s (Sum.inr b) y
inr : ∀ {d : δ}, s b d → isRight.{u_1, u_2} (α := γ) (Sum.inr d) = true
⊢ y.isRight = true

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b : β
d : δ
h : s b d
⊢ isRight.{u_1, u_2} (α := γ) (inr d) = true

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isLeft = true
⊢ ∃ (a : α), ∃ (c : γ), r a c ∧ x = inl a ∧ y = inl c

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : y.isLeft = true
⊢ ∃ (a : α), ∃ (c : γ), r a c ∧ x = inl a ∧ y = inl c

Tactic:
exists_of_isLeft_left h₁ ((isLeft_congr h₁).mpr h₂)

Premises used: Iff.mpr, Sum.LiftRel.isLeft_congr, Sum.LiftRel.exists_of_isLeft_left
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isRight = true
⊢ ∃ (b : β), ∃ (d : δ), s b d ∧ x = inr b ∧ y = inr d

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : y.isRight = true
⊢ ∃ (b : β), ∃ (d : δ), s b d ∧ x = inr b ∧ y = inr d

Tactic:
exists_of_isRight_left h₁ ((isRight_congr h₁).mpr h₂)

Premises used: Iff.mpr, Sum.LiftRel.exists_of_isRight_left, Sum.LiftRel.isRight_congr
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
α' : Type w
β : Type v
β' : Type x
f : α → β
g : α' → β'
hf : Bijective f
hg : Bijective g
⊢ Bijective (Sum.map f g)

Tactic:
⟨hf.injective.sumMap hg.injective, hf.surjective.sumMap hg.surjective⟩

Premises used: Function.Injective.sumMap, Function.Surjective.sumMap, Function.Bijective.injective, Function.Bijective.surjective, And.intro, Function.Bijective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Sort u_3
f : α → γ
g₁ g₂ : β → γ
hg : Sum.elim f g₁ = Sum.elim f g₂
b : β
⊢ g₁ b = g₂ b

Tactic:
simpa using congr_fun hg (Sum.inr b)

Premises used: Sum.inr, congr_fun
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
inl : ∀ (a : α) (h : Sum.map f g (Sum.inl a) = Sum.inl c), ∃ (a : α), f a = c
inr : ∀ (b : β) (h : Sum.map f g (Sum.inr b) = Sum.inl c), ∃ (a : α), f a = c
⊢ ∃ (a : α), f a = c

Tactic:
obtain ⟨a | b, h⟩ := h (inl c)

Premises used: Sum.inl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h_1 : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ (a : α), f a = c

Tactic:
⟨a, inl_injective h⟩

Premises used: Sum.inl_injective, Exists.intro
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h_1 : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ (a : α), f a = c

Tactic:
exact ⟨a, inl_injective h⟩
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h_1 : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ (a : α), f a = c

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
inl : ∀ (a : α) (h : Sum.map f g (Sum.inl a) = Sum.inr d), ∃ (a : β), g a = d
inr : ∀ (b : β) (h : Sum.map f g (Sum.inr b) = Sum.inr d), ∃ (a : β), g a = d
⊢ ∃ (a : β), g a = d

Tactic:
obtain ⟨a | b, h⟩ := h (inr d)

Premises used: Sum.inr
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h_1 : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ (a : β), g a = d

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h_1 : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ (a : β), g a = d

Tactic:
⟨b, inr_injective h⟩

Premises used: Sum.inr_injective, Exists.intro
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h_1 : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ (a : β), g a = d

Tactic:
exact ⟨b, inr_injective h⟩
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
⊢ Bijective (Sum.map f g) ↔ Bijective f ∧ Bijective g

Tactic:
(map_injective.and map_surjective).trans <| and_and_and_comm

Premises used: Sum.map_injective, and_and_and_comm, Iff.and, Iff.trans, Function.Bijective, Sum.map_surjective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Sort u_3
β : Sort u_4
⊢ Function.Injective (α := α) (β := α ⊕' β) inl

Tactic:
fun _ _ ↦ inl.inj

Premises used: PSum.inl.inj, Function.Injective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Sort u_3
β : Sort u_4
⊢ Function.Injective (α := β) (β := α ⊕' β) inr

Tactic:
fun _ _ ↦ inr.inj

Premises used: Function.Injective, PSum.inr.inj
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
mp :
  c ∈ sumLift₂ f g a b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
mpr :
  ((∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂) →
    c ∈ sumLift₂ f g a b
⊢ c ∈ sumLift₂ f g a b ↔
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
constructor
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
mp :
  ∀ (a : α₁),
    c ∈ sumLift₂ f g (inl a) b →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
mp₁ :
  ∀ (a : α₂),
    c ∈ sumLift₂ f g (inr a) b →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ c ∈ sumLift₂ f g a b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rcases a with a | a
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
mp :
  ∀ (b : β₁),
    c ∈ sumLift₂ f g (inl a) (inl b) →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
mp₁ :
  ∀ (b : β₂),
    c ∈ sumLift₂ f g (inl a) (inr b) →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ c ∈ sumLift₂ f g (inl a) b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rcases b with b | b
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
mp :
  ∀ (b : β₁),
    c ∈ sumLift₂ f g (inr a) (inl b) →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
          inr a = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
mp₁ :
  ∀ (b : β₂),
    c ∈ sumLift₂ f g (inr a) (inr b) →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ c ∈ sumLift₂ f g (inr a) b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rcases b with b | b
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
mp :
  (∃ a_1 ∈ f a b, (Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) a_1 = c) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ c ∈ sumLift₂ f g (inl a) (inl b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rw [sumLift₂, mem_map]

Premises used: Finset.mem_map, Finset.sumLift₂
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
        Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
      inl a = inr a₂ ∧
        inl b = inr b₂ ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ g a₂ b₂

Tactic:
Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩

Premises used: And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
        Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
      inl a = inr a₂ ∧
        inl b = inr b₂ ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ g a₂ b₂

Tactic:
exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩

Premises used: Or.inl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
⊢ c ∈ sumLift₂ f g (inl a) (inr b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
fun h ↦ (notMem_empty _ h).elim

Premises used: False.elim, Finset.notMem_empty