awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
abseq :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))) u →
    p u
have mp : u ∈ f' '' univ → p u
Tactic: rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
a' : PFunctor.A.{u, u_1} (P F)
f' : (P F).B a' → α
abseq :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left : Membership.mem (γ := Set ((P F).B a')) univ i
hi : f' i = u
⊢ p u
have mp : p (f' i)
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' :
  ∀ (u : α),
    Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
        u →
      p u
⊢ ∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
    Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
        (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1)) ∧
      ∀ (i : (P F).B a_1), p (f_1 i)
have mpr : ∀ (i : (P F).B a),
  Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (f i)
Tactic: refine ⟨a, f, rfl, fun i => h' _ ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
x : F α
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' :
  ∀ (u : α),
    Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
        u →
      p u
i : (P F).B a
⊢ Membership.mem (γ := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (f i)
have mpr : f i ∈ f '' univ
Tactic: rw [supp_eq_of_isUniform h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> x) = g '' supp x
have rw : supp (g <$> abs.{u, u_1, u} (repr x)) = g '' supp (abs.{u, u_1, u} (repr x))
Tactic: rw [← abs_repr x]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs.{u, u_1, u} (repr x)) = g '' supp (abs.{u, u_1, u} (repr x))
have obtain : ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
  supp (g <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
Tactic: obtain ⟨a, f⟩ := repr x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
⊢ supp (g <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
have rw : supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → β) a (g ∘ f))) =
  g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
Tactic: rw [← abs_map, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
⊢ supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → β) a (g ∘ f))) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
have rw : g ∘ f '' univ = g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
Tactic: rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
rw : g ∘ f '' univ = g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → β) a (g ∘ f))) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
have rw₁ : g ∘ f '' univ = g '' f '' univ
Tactic: rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α β : Type u
g : α → β
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
rw : g ∘ f '' univ = g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
rw₁ : g ∘ f '' univ = g '' f '' univ
⊢ supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → β) a (g ∘ f))) =
    g '' supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
have rw₂ : g '' f '' univ = g '' f '' univ
Tactic: rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
⊢ SuppPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
have mp : SuppPreservation.{u, u_1} (F := F) → IsUniform.{u, u_1} (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
mp : SuppPreservation.{u, u_1} (F := F) → IsUniform.{u, u_1} (F := F)
⊢ SuppPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
have mpr : IsUniform.{u, u_1} (F := F) → SuppPreservation.{u, u_1} (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
a a' : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
f' : (P F).B a' → α
h' :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
⊢ f '' univ = f' '' univ
have mp : supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) =
  f' '' univ
Tactic: rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
a a' : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
f' : (P F).B a' → α
h' :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp :
  supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) =
    f' '' univ
⊢ f '' univ = f' '' univ
have mp₁ : Eq.{u + 1} (α := Set α)
  (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
  (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
Tactic: rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
a a' : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
f' : (P F).B a' → α
h' :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp :
  supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) =
    f' '' univ
mp₁ :
  Eq.{u + 1} (α := Set α)
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
⊢ f '' univ = f' '' univ
have mp₂ : Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
  (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
Tactic: rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
a a' : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
f' : (P F).B a' → α
h' :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp :
  supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) =
    f' '' univ
mp₁ :
  Eq.{u + 1} (α := Set α)
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp₂ :
  Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
⊢ f '' univ = f' '' univ
have mp₃ : Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f')))
  (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
Tactic: rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
a a' : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
f' : (P F).B a' → α
h' :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp :
  supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) =
    f' '' univ
mp₁ :
  Eq.{u + 1} (α := Set α)
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp₂ :
  Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
mp₃ :
  Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f')))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
⊢ f '' univ = f' '' univ
have mp₄ : Eq.{u + 1} (α := Set α)
  (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
  (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a' f'))
Tactic: rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
⊢ Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
have mpr : f '' univ =
  supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
    (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
Tactic: rwa [supp_eq_of_isUniform, PFunctor.supp_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : IsUniform.{u, u_1} (F := F)
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
mpr :
  f '' univ =
    supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
mpr₁ : IsUniform.{u, u_1} (F := F)
⊢ Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
have mpr₂ : f '' univ = f '' univ
Tactic: rwa [supp_eq_of_isUniform, PFunctor.supp_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
⊢ SuppPreservation.{u, u_1} (F := F) ↔ LiftpPreservation.{u, u_1} (F := F)
have mp : SuppPreservation.{u, u_1} (F := F) → LiftpPreservation.{u, u_1} (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
mp : SuppPreservation.{u, u_1} (F := F) → LiftpPreservation.{u, u_1} (F := F)
⊢ SuppPreservation.{u, u_1} (F := F) ↔ LiftpPreservation.{u, u_1} (F := F)
have mpr : LiftpPreservation.{u, u_1} (F := F) → SuppPreservation.{u, u_1} (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : SuppPreservation.{u, u_1} (F := F)
α : Type u
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' : SuppPreservation.{u, u_1} (F := F)
⊢ Liftp p (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) ↔
    Liftp (F := (↑(P F) : (α : Type u) → Type (max u u_1))) p
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
have h'₁ : IsUniform.{u, u_1} (F := F)
Tactic: rw [suppPreservation_iff_uniform] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h :
  ∀ ⦃α : Type u⦄ (x : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    Eq.{u + 1} (α := Set α) {y : α | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y}
      {y : α | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' : IsUniform.{u, u_1} (F := F)
⊢ Liftp p (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) ↔
    Liftp (F := (↑(P F) : (α : Type u) → Type (max u u_1))) p
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
have mp : (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)
Tactic: rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
⊢ LiftpPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
have rw : SuppPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
Tactic: rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_uniform]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
rw : SuppPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
⊢ LiftpPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
have rw₁ : IsUniform.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
Tactic: rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_uniform]
-- Lean 4 proof step from Mathlib.Data.Quot (hypothesis)
Goal:
α : Sort u_3
r : α → α → Prop
iseqv : Equivalence r
p : α → α → Prop
iseqv_1 : Equivalence p
Eq : ∀ (a b : α), ({ r := r, iseqv := iseqv } : α → α → Prop) a b ↔ ({ r := p, iseqv := iseqv_1 } : α → α → Prop) a b
⊢ _root_.Eq.{max 1 u_3} { r := r, iseqv := iseqv : Setoid α } { r := p, iseqv := iseqv_1 }
have this : _root_.Eq.{max 1 u_3} r p
Tactic: have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
α : Sort u_3
r : α → α → Prop
iseqv : Equivalence r
p : α → α → Prop
iseqv_1 : Equivalence p
Eq : ∀ (a b : α), ({ r := r, iseqv := iseqv } : α → α → Prop) a b ↔ ({ r := p, iseqv := iseqv_1 } : α → α → Prop) a b
this : _root_.Eq.{max 1 u_3} r p
⊢ _root_.Eq.{max 1 u_3} { r := r, iseqv := iseqv : Setoid α } { r := p, iseqv := iseqv_1 }
have subst : ∀ (iseqv_2 : Equivalence r)
  (Eq :
    ∀ (a b : α), ({ r := r, iseqv := iseqv } : α → α → Prop) a b ↔ ({ r := r, iseqv := iseqv_2 } : α → α → Prop) a b),
  _root_.Eq.{max 1 u_3} { r := r, iseqv := iseqv : Setoid α } { r := r, iseqv := iseqv_2 }
Tactic: subst this
Cleared hypotheses: p, iseqv_1, Eq, this
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ x ≈ y.out
have refine : ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧
Tactic: refine Iff.trans ?_ Quotient.eq
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧
have rw : ⟦x⟧ = y ↔ ⟦x⟧ = y
Tactic: rw [Quotient.out_eq y]
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ x.out ≈ y
have refine : x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧
Tactic: refine Iff.trans ?_ Quotient.eq
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧
have rw : x = ⟦y⟧ ↔ x = ⟦y⟧
Tactic: rw [Quotient.out_eq x]
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x.out ≈ y.out ↔ x = y
have rw : x = ⟦y.out⟧ ↔ x = y
Tactic: rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
α : Sort u_1
s : Setoid α
x y : Quotient s
rw : x = ⟦y.out⟧ ↔ x = y
⊢ x.out ≈ y.out ↔ x = y
have rw₁ : x = y ↔ x = y
Tactic: rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]
-- Lean 4 proof step from Mathlib.Data.Quot (goal)
Goal:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid.{u_4} (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun (i : ι) ↦ ⟦a i⟧
⊢ p f
have rw : p fun (i : ι) ↦ ⟦(f i).out⟧
Tactic: rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h :
  Eq.{u_3 + 1} (α := α) (↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } : α)
    (↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ } : α)
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ : ℚ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
have d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
Tactic: have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h :
  Eq.{u_3 + 1} (α := α) (↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } : α)
    (↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ } : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ : ℚ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
have d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
Tactic: have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h :
  Eq.{u_3 + 1} (α := α) (↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } : α)
    (↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ } : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ : ℚ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
have rw : ∀ (h : Eq.{u_3 + 1} (α := α) (↑(n₁ /. (↑d₁ : ℤ)) : α) (↑(n₂ /. (↑d₂ : ℤ)) : α))
  (d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0) (d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
Tactic: rw [mk_eq_divInt, mk_eq_divInt] at h ⊢
Cleared hypotheses: h, d₁a, d₂a
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : Eq.{u_3 + 1} (α := α) (↑(n₁ /. (↑d₁ : ℤ)) : α) (↑(n₂ /. (↑d₂ : ℤ)) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have h₁ : HDiv.hDiv (α := α) (↑n₁ : α) (↑(↑d₁ : ℤ) : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑(↑d₂ : ℤ) : α)
Tactic: rw [cast_divInt_of_ne_zero _ (by simpa), cast_divInt_of_ne_zero _ (by simpa)] at h
Cleared hypotheses: h, d₁a, d₂a
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : HDiv.hDiv (α := α) (↑n₁ : α) (↑(↑d₁ : ℤ) : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑(↑d₂ : ℤ) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have h₁ : HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑d₂ : α)
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
h : HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑d₂ : α)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa : ∀ (h : HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) * (↑d₂ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
Tactic: rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq,
      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁,
      ← Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
      at h
Cleared hypotheses: h