awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f s (image2 g t u) = image2 g' t (image2 f' s u)
have rw : image2 (fun (a : δ) (b : α) ↦ f b a) (image2 g t u) s = image2 g' t (image2 (fun (a : γ) (b : α) ↦ f' b a) u s)
Tactic: rw [image2_swap f', image2_swap f]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t
have rw : image2 f (image2 (fun (a : β) (b : α) ↦ g b a) t s) u = image2 (fun (a : β) (b : δ') ↦ g' b a) t (image2 f' s u)
Tactic: rw [image2_swap g, image2_swap g']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)
have simp_rw : image2 (fun (a : α) (b : β) ↦ g (f a b)) s t = image2 f' (g₁ '' s) (g₂ '' t)
Tactic: simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
simp_rw : image2 (fun (a : α) (b : β) ↦ g (f a b)) s t = image2 f' (g₁ '' s) (g₂ '' t)
⊢ g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)
have simp_rw₁ : Eq.{u_7 + 1} (α := Set δ) (image2 (fun (a : α) (b : β) ↦ g (f a b)) s t)
  (image2 (fun (a : α) (b : β') ↦ f' (g₁ a) b) s (g₂ '' t))
Tactic: simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
simp_rw : image2 (fun (a : α) (b : β) ↦ g (f a b)) s t = image2 f' (g₁ '' s) (g₂ '' t)
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set δ) (image2 (fun (a : α) (b : β) ↦ g (f a b)) s t)
    (image2 (fun (a : α) (b : β') ↦ f' (g₁ a) b) s (g₂ '' t))
⊢ g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)
have simp_rw₂ : Eq.{u_7 + 1} (α := Set δ) (image2 (fun (a : α) (b : β) ↦ g (f a b)) s t)
  (image2 (fun (a : α) (b : β) ↦ f' (g₁ a) (g₂ b)) s t)
Tactic: simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ image2 f' (g' '' s) ((fun (b : β) ↦ b) '' t) = image2 f' (g' '' s) t
have rw : image2 f' (g' '' s) t = image2 f' (g' '' s) t
Tactic: rw [image_id']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ image2 f' ((fun (a : α) ↦ a) '' s) (g' '' t) = image2 f' s (g' '' t)
have rw : image2 f' s (g' '' t) = image2 f' s (g' '' t)
Tactic: rw [image_id']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)
have rw : g '' image2 (fun (a : β) (b : α) ↦ f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)
Tactic: rw [image2_swap f]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ image2 f' (g' '' t) ((fun (a : α) ↦ a) '' s) = image2 f' (g' '' t) s
have rw : image2 f' (g' '' t) s = image2 f' (g' '' t) s
Tactic: rw [image_id']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ image2 f' ((fun (b : β) ↦ b) '' t) (g' '' s) = image2 f' t (g' '' s)
have rw : image2 f' t (g' '' s) = image2 f' t (g' '' s)
Tactic: rw [image_id']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
⊢ image2 f {a} t = t
have rw : f a '' t = t
Tactic: rw [image2_singleton_left, show f a = id from funext h, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
rw : f a '' t = t
⊢ image2 f {a} t = t
have rw₁ : id '' t = t
Tactic: rw [image2_singleton_left, show f a = id from funext h, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
rw : f a '' t = t
rw₁ : id '' t = t
⊢ image2 f {a} t = t
have rw₂ : t = t
Tactic: rw [image2_singleton_left, show f a = id from funext h, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
⊢ image2 f s {b} = s
have rw : (fun (a : α) ↦ f a b) '' s = s
Tactic: rw [image2_singleton_right, funext h, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
rw : (fun (a : α) ↦ f a b) '' s = s
⊢ image2 f s {b} = s
have rw₁ : (fun (x : α) ↦ x) '' s = s
Tactic: rw [image2_singleton_right, funext h, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
rw : (fun (a : α) ↦ f a b) '' s = s
rw₁ : (fun (x : α) ↦ x) '' s = s
⊢ image2 f s {b} = s
have rw₂ : s = s
Tactic: rw [image2_singleton_right, funext h, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'
have rw : image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'
Tactic: rw [image2_union_right]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'
have rw : image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'
Tactic: rw [image2_union_left]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t
have rw : image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t
have rw : image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t
Tactic: rw [image2_comm hf]
-- Lean 4 proof step from Mathlib.Data.Set.Operations (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : (↑(range f) : Type u_3)
⊢ rangeFactorization f a = b ↔ f a = (↑b : α)
have rw : Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) sorry = b ↔ f a = (↑b : α)
Tactic: rw [Set.rangeFactorization, ← b.coe_eta b.2, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Operations (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : (↑(range f) : Type u_3)
rw : Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯ = b ↔ f a = (↑b : α)
⊢ rangeFactorization f a = b ↔ f a = (↑b : α)
have rw₁ : Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) sorry = Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) sorry ↔
  f a = (↑(Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) sorry) : α)
Tactic: rw [Set.rangeFactorization, ← b.coe_eta b.2, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Operations (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : (↑(range f) : Type u_3)
rw : Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯ = b ↔ f a = (↑b : α)
rw₁ :
  Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯ = Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) ⋯ ↔
    f a = (↑(Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) ⋯) : α)
⊢ rangeFactorization f a = b ↔ f a = (↑b : α)
have rw₂ : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) sorry) : α) =
    (↑(Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) sorry) : α) ↔
  f a = (↑(Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) sorry) : α)
Tactic: rw [Set.rangeFactorization, ← b.coe_eta b.2, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Operations (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ f ∘ rangeSplitting f = Subtype.val (p := fun (x : β) ↦ x ∈ range f)
have h : ∀ (x : (↑(range f) : Type v)), (f ∘ rangeSplitting f) x = (↑x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Operations (goal)
Goal:
α : Type u
β : Type v
f : α → β
x : (↑(range f) : Type v)
⊢ (f ∘ rangeSplitting f) x = (↑x : β)
have h : f (rangeSplitting f x) = (↑x : β)
Tactic: simp only [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : α
⊢ Eq (α := Set αᵒᵖ) (Set.op {x}) {op x}
have h : ∀ (x_1 : αᵒᵖ), Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {op x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : α
x_1 : αᵒᵖ
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {op x} x_1
have h : Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {op x} x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : α
x_1 : αᵒᵖ
h : Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {op x} x_1
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {op x} x_1
have h₁ : Membership.mem (γ := Set αᵒᵖ) {op x} x_1 → Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : αᵒᵖ
⊢ Eq (α := Set α) (Set.unop {x}) {unop x}
have h : ∀ (x_1 : α), Membership.mem (γ := Set α) (Set.unop {x}) x_1 ↔ Membership.mem (γ := Set α) {unop x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : αᵒᵖ
x_1 : α
⊢ Membership.mem (γ := Set α) (Set.unop {x}) x_1 ↔ Membership.mem (γ := Set α) {unop x} x_1
have h : Membership.mem (γ := Set α) (Set.unop {x}) x_1 → Membership.mem (γ := Set α) {unop x} x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : αᵒᵖ
x_1 : α
h : Membership.mem (γ := Set α) (Set.unop {x}) x_1 → Membership.mem (γ := Set α) {unop x} x_1
⊢ Membership.mem (γ := Set α) (Set.unop {x}) x_1 ↔ Membership.mem (γ := Set α) {unop x} x_1
have h₁ : Membership.mem (γ := Set α) {unop x} x_1 → Membership.mem (γ := Set α) (Set.unop {x}) x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : α
⊢ Eq (α := Set α) (Set.unop {op x}) {x}
have h : ∀ (x_1 : α), Membership.mem (γ := Set α) (Set.unop {op x}) x_1 ↔ Membership.mem (γ := Set α) {x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x x_1 : α
⊢ Membership.mem (γ := Set α) (Set.unop {op x}) x_1 ↔ Membership.mem (γ := Set α) {x} x_1
have h : Membership.mem (γ := Set α) (Set.unop {op x}) x_1 → Membership.mem (γ := Set α) {x} x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x x_1 : α
h : Membership.mem (γ := Set α) (Set.unop {op x}) x_1 → Membership.mem (γ := Set α) {x} x_1
⊢ Membership.mem (γ := Set α) (Set.unop {op x}) x_1 ↔ Membership.mem (γ := Set α) {x} x_1
have h₁ : Membership.mem (γ := Set α) {x} x_1 → Membership.mem (γ := Set α) (Set.unop {op x}) x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x : αᵒᵖ
⊢ Eq (α := Set αᵒᵖ) (Set.op {unop x}) {x}
have h : ∀ (x_1 : αᵒᵖ), Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x x_1 : αᵒᵖ
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {x} x_1
have h : Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {x} x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Opposite (goal)
Goal:
α : Type u_1
x x_1 : αᵒᵖ
h : Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {x} x_1
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {x} x_1
have h₁ : Membership.mem (γ := Set αᵒᵖ) {x} x_1 → Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂
have inl : ∀ (a₁ : α) (hne : e a₁ ≠ b₂), (Disjoint on extend e f ⊥) (e a₁) b₂
Tactic: rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁
Cleared hypotheses: b₁, hne
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
inl : ∀ (a₁ : α) (hne : e a₁ ≠ b₂), (Disjoint on extend e f ⊥) (e a₁) b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂
have inr : ∀ (hb₁ : ¬∃ (a₁ : α), e a₁ = b₁), (Disjoint on extend e f ⊥) b₁ b₂
Tactic: rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂
have inl : ∀ (a₂ : α) (hne : e a₁ ≠ e a₂), (Disjoint on extend e f ⊥) (e a₁) (e a₂)
Tactic: rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂
Cleared hypotheses: b₂, hne
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
inl : ∀ (a₂ : α) (hne : e a₁ ≠ e a₂), (Disjoint on extend e f ⊥) (e a₁) (e a₂)
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂
have inl₁ : ∀ (hb₂ : ¬∃ (a₂ : α), e a₂ = b₂), (Disjoint on extend e f ⊥) (e a₁) b₂
Tactic: rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
have mp : s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
hs : s.Nonempty
mp : s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
⊢ s.Pairwise (r on f) ↔ ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
have mpr : (∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
have mp : ∀ (y : ι) (hy : y ∈ s), s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
Tactic: rcases hs with ⟨y, hy⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
⊢ s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
have mp : ∀ (H : s.Pairwise (r on f)) (x : ι) (hx : x ∈ s), r (f x) (f y)
Tactic: refine fun H => ⟨f y, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
⊢ r (f x) (f y)
have mp : ∀ (hy : x ∈ s), r (f x) (f x)
Tactic: rcases eq_or_ne x y with (rfl | hne)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
mp : ∀ (hy : x ∈ s), r (f x) (f x)
⊢ r (f x) (f y)
have mp₁ : ∀ (hne : x ≠ y), r (f x) (f y)
Tactic: rcases eq_or_ne x y with (rfl | hne)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst_1 : IsEquiv ι r
⊢ s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z
have inl : Set.Pairwise ∅ (r on f) ↔ ∃ (z : ι), ∀ (x : α), Membership.mem (γ := Set α) ∅ x → r (f x) z
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst_1 : IsEquiv ι r
inl : Set.Pairwise ∅ (r on f) ↔ ∃ (z : ι), ∀ (x : α), Membership.mem (γ := Set α) ∅ x → r (f x) z
⊢ s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z
have inr : ∀ (hne : s.Nonempty), s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i = j ∨ Disjoint (f i) (f j)
have rw : ¬Disjoint (f i) (f j) → i = j
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
⊢ (PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
have refine_1 : ∀ (hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t) (x : α × β) (hx : x ∈ s ×ˢ t) (y : α × β)
  (hy : y ∈ s ×ˢ t) (h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y), x = y
Tactic: refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
refine_1 :
  ∀ (hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t) (x : α × β) (hx : x ∈ s ×ˢ t) (y : α × β)
    (hy : y ∈ s ×ˢ t) (h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y), x = y
⊢ (PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
have refine_2 : ∀ (hs : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (h : x ≠ y),
  onFun.{u_1 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (a : α) ↦ f a '' t) x y
Tactic: refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
this : x.1 = y.1
⊢ (fun (p : α × β) ↦ f p.1 p.2) y = f x.1 y.2
have rw : (fun (p : α × β) ↦ f p.1 p.2) y = f y.1 y.2
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ x = y
have refine_1 : x.1 = y.1
Tactic: suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ x.1 = y.1
have refine_1 : f x.1 x.2 ∈ f y.1 '' t
Tactic: refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ f x.1 x.2 ∈ f y.1 '' t
have refine_1 : (fun (p : α × β) ↦ f p.1 p.2) y ∈ f y.1 '' t
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ onFun.{u_1 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (a : α) ↦ f a '' t) x y
have refine_2 : LE.le.{u_3} (α := Set γ) ((fun (a : α) ↦ f a '' t) x ⊓ (fun (a : α) ↦ f a '' t) y) ⊥
Tactic: refine disjoint_iff_inf_le.mpr ?_
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
⊢ (PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
have refine_1 : ∀ (ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) (x : α × β)
  (hx : x ∈ s ×ˢ t) (y : α × β) (hy : y ∈ s ×ˢ t) (h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y), x = y
Tactic: refine ⟨fun ht x hx y hy (h : f _ _ = _) => ?_, fun ht x hx y hy h => ?_⟩