awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
rw :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
      MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₁ :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ ''
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₂ :
  image (α := (↑(f ⁻¹' t) : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
      (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
have rw₃ : f ''
    image (α := (↑(f ⁻¹' t) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
      (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
  (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
Tactic: rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
rw :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
      MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₁ :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ ''
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₂ :
  image (α := (↑(f ⁻¹' t) : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
      (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₃ :
  f ''
      image (α := (↑(f ⁻¹' t) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
        (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
have rw₄ : f '' (f ⁻¹' t ∩ s) = (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
Tactic: rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
rw :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
      MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₁ :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ ''
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₂ :
  image (α := (↑(f ⁻¹' t) : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
      (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₃ :
  f ''
      image (α := (↑(f ⁻¹' t) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
        (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₄ :
  f '' (f ⁻¹' t ∩ s) = (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
have rw₅ : f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
Tactic: rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
rw :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
      MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₁ :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ ''
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₂ :
  image (α := (↑(f ⁻¹' t) : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
      (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₃ :
  f ''
      image (α := (↑(f ⁻¹' t) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
        (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₄ :
  f '' (f ⁻¹' t ∩ s) = (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₅ : f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
have rw₆ : t ∩ f '' s = t ∩ f '' s
Tactic: rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set (↑t : Type u_2)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u =
    f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
have h : ∀ (x : α),
  x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u ↔
    x ∈ f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set (↑t : Type u_2)
⊢ t.restrictPreimage f ⁻¹' u =
    (fun (a : (↑(f ⁻¹' t) : Type u_1)) ↦ f (↑a : α)) ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
have rw : t.restrictPreimage f ⁻¹' u =
  Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
Tactic: rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
    preimage_image_eq _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set (↑t : Type u_2)
rw :
  t.restrictPreimage f ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
⊢ t.restrictPreimage f ⁻¹' u =
    (fun (a : (↑(f ⁻¹' t) : Type u_1)) ↦ f (↑a : α)) ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
have rw₁ : t.restrictPreimage f ⁻¹' u =
  Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹'
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u
Tactic: rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
    preimage_image_eq _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set (↑t : Type u_2)
rw :
  t.restrictPreimage f ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
rw₁ :
  t.restrictPreimage f ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹'
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u
⊢ t.restrictPreimage f ⁻¹' u =
    (fun (a : (↑(f ⁻¹' t) : Type u_1)) ↦ f (↑a : α)) ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
have rw₂ : t.restrictPreimage f ⁻¹' u = t.restrictPreimage f ⁻¹' u
Tactic: rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
    preimage_image_eq _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Injective (restrict f s t h) ↔ InjOn f s
have rw : Injective (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) t sorry) ↔ InjOn f s
Tactic: rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
rw : Injective (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) t ⋯) ↔ InjOn f s
⊢ Injective (restrict f s t h) ↔ InjOn f s
have rw₁ : Injective (s.restrict (π := fun (a : α) ↦ β) f) ↔ InjOn f s
Tactic: rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
rw : Injective (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) t ⋯) ↔ InjOn f s
rw₁ : Injective (s.restrict (π := fun (a : α) ↦ β) f) ↔ InjOn f s
⊢ Injective (restrict f s t h) ↔ InjOn f s
have rw₂ : Injective (s.restrict (π := fun (a : α) ↦ β) f) ↔ Injective (s.restrict (π := fun (a : α) ↦ β) f)
Tactic: rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Surjective (restrict f s t h) ↔ SurjOn f s t
have refine_1 : ∀ (h' : Surjective (restrict f s t h)) (b : β) (hb : b ∈ t), b ∈ f '' s
Tactic: refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
refine_1 : ∀ (h' : Surjective (restrict f s t h)) (b : β) (hb : b ∈ t), b ∈ f '' s
⊢ Surjective (restrict f s t h) ↔ SurjOn f s t
have refine_2 : ∀ (h' : SurjOn f s t) (x : (↑t : Type u_2)) (b : β) (hb : b ∈ t),
  ∃ (a : (↑s : Type u_1)), restrict f s t h a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb
Tactic: refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
⊢ b ∈ f '' s
have refine_1 : ∀ (a : α) (ha : a ∈ s)
  (ha' : restrict f s t h (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb),
  b ∈ f '' s
Tactic: obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb
⊢ b ∈ f '' s
have ha'₁ : f a = b
Tactic: replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ b ∈ f '' s
have refine_1 : f a ∈ f '' s
Tactic: rw [← ha']
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x : (↑t : Type u_2)
b : β
hb : b ∈ t
⊢ ∃ (a : (↑s : Type u_1)), restrict f s t h a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb
have refine_2 : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t),
  ∃ (a_1 : (↑s : Type u_1)), restrict f s t h a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hb
Tactic: obtain ⟨a, ha, rfl⟩ := h' hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
⊢ a = (↑y : G × P).1 • (↑x : G × P).2
have rw : a = (↑x : G × P).1 • (↑x : G × P).2
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).2 = (↑y : G × P).2
⊢ a = (↑x : G × P).1 • (↑y : G × P).2
have rw : a = (↑x : G × P).1 • (↑x : G × P).2
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsLeftCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
⊢ a = (↑y : G × P).1 • (↑x : G × P).2
have rw : a = (↑x : G × P).1 • (↑x : G × P).2
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
⊢ (s.smulAntidiagonal t a).Finite
have by_contra! : ∀ (h : (s.smulAntidiagonal t a).Infinite), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (hypothesis)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
⊢ False
have h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
Tactic: have h1 : (smulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) :=
    fun f ↦ hs fun n ↦ ⟨_, (mem_smulAntidiagonal.1 (f n).2).1⟩
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (hypothesis)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
⊢ False
have h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
Tactic: have h2 : (smulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) :=
    fun f ↦ ht fun n ↦ ⟨_, (mem_smulAntidiagonal.1 (f n).2).2.1⟩
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
⊢ False
have obtain : ∀ (g : ℕ ↪o ℕ)
  (hg :
    ∀ (m n : ℕ),
      m ≤ n →
        Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
          (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                  (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
                ((g : (a : ℕ) → ℕ) m : ℕ)) :
            G × P)
          (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                  (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
                ((g : (a : ℕ) → ℕ) n : ℕ)) :
            G × P)),
  False
Tactic: obtain ⟨g, hg⟩ := h1.exists_monotone_subseq fun n ↦ (h.natEmbedding _ n).2
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          G × P)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          G × P)
⊢ False
have obtain : ∀ (m n : ℕ) (mn : m < n)
  (h2' :
    Subrel (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2) (fun (x : G × P) ↦ x ∈ s.smulAntidiagonal t a)
      ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) m : ℕ))
      ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) n : ℕ))),
  False
Tactic: obtain ⟨m, n, mn, h2'⟩ := h2 fun n ↦ h.natEmbedding _ _
-- Lean 4 proof step from Mathlib.Data.Set.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          G × P)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          G × P)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2) (fun (x : G × P) ↦ x ∈ s.smulAntidiagonal t a)
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ False
have refine : Eq (α := (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
  ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) m : ℕ) :
    (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
  ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) n : ℕ) :
    (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
Tactic: refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Semiring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
⊢ Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β)
        (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) 1)) :
      SetSemiring β)
    (1 : SetSemiring β)
have rw : Eq.{u_2 + 1} (α := SetSemiring β)
  ((up : (a : Set β) → SetSemiring β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) 1) : SetSemiring β)
  (1 : SetSemiring β)
Tactic: rw [down_one, image_one, map_one, singleton_one, up_one]
-- Lean 4 proof step from Mathlib.Data.Set.Semiring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
rw :
  Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) 1) : SetSemiring β)
    (1 : SetSemiring β)
⊢ Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β)
        (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) 1)) :
      SetSemiring β)
    (1 : SetSemiring β)
have rw₁ : Eq (α := SetSemiring β)
  ((up : (a : Set β) → SetSemiring β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) : SetSemiring β)
  (1 : SetSemiring β)
Tactic: rw [down_one, image_one, map_one, singleton_one, up_one]
-- Lean 4 proof step from Mathlib.Data.Set.Semiring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
rw :
  Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) 1) : SetSemiring β)
    (1 : SetSemiring β)
rw₁ :
  Eq (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) : SetSemiring β)
    (1 : SetSemiring β)
⊢ Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β)
        (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) 1)) :
      SetSemiring β)
    (1 : SetSemiring β)
have rw₂ : Eq (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) {1} : SetSemiring β) (1 : SetSemiring β)
Tactic: rw [down_one, image_one, map_one, singleton_one, up_one]
-- Lean 4 proof step from Mathlib.Data.Set.Semiring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
rw :
  Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) 1) : SetSemiring β)
    (1 : SetSemiring β)
rw₁ :
  Eq (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) : SetSemiring β)
    (1 : SetSemiring β)
rw₂ : Eq (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) {1} : SetSemiring β) (1 : SetSemiring β)
⊢ Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β)
        (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) 1)) :
      SetSemiring β)
    (1 : SetSemiring β)
have rw₃ : Eq.{u_2 + 1} (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) 1 : SetSemiring β) (1 : SetSemiring β)
Tactic: rw [down_one, image_one, map_one, singleton_one, up_one]
-- Lean 4 proof step from Mathlib.Data.Set.Semiring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
rw :
  Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) 1) : SetSemiring β)
    (1 : SetSemiring β)
rw₁ :
  Eq (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) : SetSemiring β)
    (1 : SetSemiring β)
rw₂ : Eq (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) {1} : SetSemiring β) (1 : SetSemiring β)
rw₃ : Eq.{u_2 + 1} (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) 1 : SetSemiring β) (1 : SetSemiring β)
⊢ Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β)
        (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) 1)) :
      SetSemiring β)
    (1 : SetSemiring β)
have rw₄ : Eq.{u_2 + 1} (α := SetSemiring β) 1 1
Tactic: rw [down_one, image_one, map_one, singleton_one, up_one]