harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w) (wn wr : Nat)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
    (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
    (htrue : ⟦aig, trueRef, assign⟧ = true)
      :
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (go aig curr falseRef trueRef n d wn wr q r).aig,
        (go aig curr falseRef trueRef n d wn wr q r).r.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divRec curr { n := lhs, d := rhs} { wn, wr, q := qbv, r := rbv }).r.getLsbD idx

Proof state:
case hr.hfalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).r.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).r.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
idx✝ : Nat
hidx✝ : idx✝ < w
hdiscr :
  { wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
      (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
    rhs
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := aig, ref := falseRef }⟧ = false

Tactic:
exact hfalse

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.isPrime_of_prime {P : Ideal A} (h : Prime P) : IsPrime P

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P.IsPrime

Tactic:
refine ⟨?_, fun hxy => ?_⟩

Result:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P ≠ ⊤

case refine_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
x✝ y✝ : A
hxy : x✝ * y✝ ∈ P
⊢ x✝ ∈ P ∨ y✝ ∈ P

Proof state:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime ⊤
⊢ False

Tactic:
rw [← Ideal.one_eq_top] at h

Result:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime 1
⊢ False

Proof state:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime 1
⊢ False

Tactic:
exact h.not_unit isUnit_one

Result:
no goals

Proof state:
case refine_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
x✝ y✝ : A
hxy : P ∣ span {x✝} * span {y✝}
⊢ P ∣ span {x✝} ∨ P ∣ span {y✝}

Tactic:
exact h.dvd_or_dvd hxy

Result:
no goals

Proof state:
case refine_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
x✝ y✝ : A
hxy : x✝ * y✝ ∈ P
⊢ x✝ ∈ P ∨ y✝ ∈ P

Tactic:
simp only [← Ideal.dvd_span_singleton, ← Ideal.span_singleton_mul_span_singleton] at hxy ⊢

Result:
case refine_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
x✝ y✝ : A
hxy : P ∣ span {x✝} * span {y✝}
⊢ P ∣ span {x✝} ∨ P ∣ span {y✝}

Proof state:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P ≠ ⊤

Tactic:
rintro rfl

Result:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime ⊤
⊢ False
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem ae_empty_or_univ_of_ae_le_preimage' (hf : Ergodic f μ) (hs : NullMeasurableSet s μ)
    (hs' : s ≤ᵐ[μ] f ⁻¹' s) (h_fin : μ s ≠ ∞) : s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
replace h_fin : μ (f ⁻¹' s) ≠ ∞ := by rwa [hf.measure_preimage hs]

Result:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : μ (f ⁻¹' s) ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : μ (f ⁻¹' s) ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s

Tactic:
exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : μ s ≠ ⊤
⊢ μ (f ⁻¹' s) ≠ ⊤

Tactic:
rwa [hf.measure_preimage hs]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : μ (f ⁻¹' s) ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_

Result:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : μ (f ⁻¹' s) ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem log_stirlingSeq_bounded_by_constant : ∃ c, ∀ n : ℕ, c ≤ log (stirlingSeq (n + 1))

Proof state:
case intro
d : ℝ
h : ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ d
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (n + 1))

Tactic:
exact ⟨log (stirlingSeq 1) - d, fun n => sub_le_comm.mp (h n)⟩

Result:
no goals

Proof state:
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (n + 1))

Tactic:
obtain ⟨d, h⟩ := log_stirlingSeq_bounded_aux

Result:
case intro
d : ℝ
h : ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ d
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (n + 1))
-- Mathlib/RingTheory/SurjectiveOnStalks.lean
lemma SurjectiveOnStalks.comp (hg : SurjectiveOnStalks g) (hf : SurjectiveOnStalks f) :
    SurjectiveOnStalks (g.comp f)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)

Tactic:
rwa [← RingHom.coe_comp, ← Localization.localRingHom_comp] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)

Tactic:
have := (hg I hI).comp (hf _ (hI.comap g))

Result:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
⊢ (g.comp f).SurjectiveOnStalks

Tactic:
intros I hI

Result:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_add_sub_eq_zero_iff (x y : F) : ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ ↔ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Tactic:
constructor

Result:
case mp
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ → ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

case mpr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ → ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ

Proof state:
case mp
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Tactic:
rw [add_comm] at h

Result:
case mp
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪y, x⟫_ℝ + ⟪x, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖

Tactic:
conv_rhs => rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖

Proof state:
case mpr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ → ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ

Tactic:
intro h

Result:
case mpr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ

Proof state:
case mpr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ

Tactic:
linarith

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖

Tactic:
simp only [← @inner_self_eq_norm_mul_norm ℝ, inner_add_left, inner_sub_right, real_inner_comm y x,
  sub_eq_zero, re_to_real]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ ↔ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Proof state:
case mp
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ → ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Tactic:
intro h

Result:
case mp
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Proof state:
case mp
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪y, x⟫_ℝ + ⟪x, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Tactic:
linarith

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
theorem isPrenex_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ) (hψ : IsPrenex ψ) :
    IsPrenex (φ.toPrenexImpRight ψ)

Proof state:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsPrenex
⊢ (φ.toPrenexImpRight ψ).IsPrenex

Tactic:
induction hψ with
| of_isQF hψ => rw [hψ.toPrenexImpRight]; exact (hφ.imp hψ).isPrenex
| all _ ih1 => exact (ih1 hφ.liftAt).all
| ex _ ih2 => exact (ih2 hφ.liftAt).ex

Result:
no goals

Proof state:
case all
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih1 : ∀ {φ : L.BoundedFormula α (n✝ + 1)}, φ.IsQF → (φ.toPrenexImpRight φ✝).IsPrenex
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight (∀'φ✝)).IsPrenex

Tactic:
exact (ih1 hφ.liftAt).all

Result:
no goals

Proof state:
case ex
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih2 : ∀ {φ : L.BoundedFormula α (n✝ + 1)}, φ.IsQF → (φ.toPrenexImpRight φ✝).IsPrenex
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight (∃'φ✝)).IsPrenex

Tactic:
exact (ih2 hφ.liftAt).ex

Result:
no goals

Proof state:
case of_isQF
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hψ : φ✝.IsQF
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ ⟹ φ✝).IsPrenex

Tactic:
exact (hφ.imp hψ).isPrenex

Result:
no goals

Proof state:
case of_isQF
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hψ : φ✝.IsQF
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight φ✝).IsPrenex

Tactic:
rw [hψ.toPrenexImpRight]

Result:
case of_isQF
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hψ : φ✝.IsQF
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ ⟹ φ✝).IsPrenex
-- Mathlib/Control/Fold.lean
theorem foldMap_map [Monoid γ] (f : α → β) (g : β → γ) (xs : t α) :
    foldMap g (f <$> xs) = foldMap (g ∘ f) xs

Proof state:
α β γ : Type u
t : Type u → Type u
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs

Tactic:
simp only [foldMap, traverse_map, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem extendDomain_subtypeDomain (f : α →₀ M) (hf : ∀ a ∈ f.support, P a) :
    (subtypeDomain P f).extendDomain = f

Proof state:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ (subtypeDomain P f).extendDomain a = f a

Tactic:
rw [extendDomain_toFun]

Result:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ (if h : P a then (subtypeDomain P f) ⟨a, h⟩ else 0) = f a

Proof state:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ (if h : P a then (subtypeDomain P f) ⟨a, h⟩ else 0) = f a

Tactic:
dsimp

Result:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ (if P a then f a else 0) = f a

Proof state:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ a ∉ f.support

Tactic:
refine mt ?_ h

Result:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ a ∈ f.support → P a

Proof state:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
⊢ (subtypeDomain P f).extendDomain a = f a

Tactic:
by_cases h : P a

Result:
case pos
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : P a
⊢ (subtypeDomain P f).extendDomain a = f a

case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ (subtypeDomain P f).extendDomain a = f a

Proof state:
case pos
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : P a
⊢ (subtypeDomain P f).extendDomain a = f a

Tactic:
exact dif_pos h

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ a ∈ f.support → P a

Tactic:
exact @hf _

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ (if P a then f a else 0) = f a

Tactic:
rw [if_neg h, eq_comm, ← not_mem_support_iff]

Result:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a
⊢ a ∉ f.support

Proof state:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
⊢ (subtypeDomain P f).extendDomain = f

Tactic:
ext a

Result:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
⊢ (subtypeDomain P f).extendDomain a = f a
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem trans_assoc_reparam {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :
    (p.trans q).trans r =
      (p.trans (q.trans r)).reparam
        (fun t => ⟨transAssocReparamAux t, transAssocReparamAux_mem_I t⟩) (by continuity)
        (Subtype.ext transAssocReparamAux_zero) (Subtype.ext transAssocReparamAux_one)

Proof state:
case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

Tactic:
exfalso

Result:
case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
-- Mathlib/RingTheory/Polynomial/Wronskian.lean
theorem wronskian_self_eq_zero (a : R[X]) : wronskian a a = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ a.wronskian a = 0

Tactic:
rw [wronskian, mul_comm, sub_self]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma extendMap_f {i : ι} {i' : ι'} (h : e.f i = i') :
    (extendMap φ e).f i' =
      (extendXIso K e h).hom ≫ φ.f i ≫ (extendXIso L e h).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extendMap φ e).f i' = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Tactic:
dsimp [extendMap]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ extend.mapX φ (e.r i') = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ extend.mapX φ (e.r i') = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Tactic:
rw [extend.mapX_some φ (e.r_eq_some h)]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/FreeCommRing.lean
theorem coe_eq : ((↑) : FreeRing α → FreeCommRing α) =
    @Functor.map FreeAbelianGroup _ _ _ fun l : List α => (l : Multiset α)

Proof state:
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : (FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ (FreeMonoid.lift FreeCommRing.of) (FreeMonoid.of hd * tl) = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)

Tactic:
rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]

Result:
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : (FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ FreeCommRing.of hd * FreeAbelianGroup.of ↑tl = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)

Proof state:
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ (FreeMonoid.lift FreeCommRing.of) L = FreeAbelianGroup.of ↑L

Tactic:
exact
  FreeMonoid.recOn L rfl fun hd tl ih => by
    rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
    conv_lhs => reduce
    rfl

Result:
no goals

Proof state:
case h
α : Type u
x : FreeRing α
⊢ (FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x =
    (FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x

Tactic:
rw [← AddMonoidHom.coe_coe]

Result:
case h
α : Type u
x : FreeRing α
⊢ ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x =
    (FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x

Proof state:
case h
α : Type u
x : FreeRing α
⊢ (FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x = (fun l => ↑l) <$> x

Tactic:
dsimp [Functor.map]

Result:
case h
α : Type u
x : FreeRing α
⊢ (FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x =
    (FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x

Proof state:
case h
α : Type u
x : FreeRing α
⊢ ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x =
    (FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x

Tactic:
apply FreeAbelianGroup.lift.unique

Result:
case h.hg
α : Type u
x : FreeRing α
⊢ ∀ (x : FreeMonoid α),
    ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of x) =
      ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) x

Proof state:
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of L) =
    ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) L

Tactic:
erw [FreeAbelianGroup.lift.of, Function.comp]

Result:
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ (FreeMonoid.lift FreeCommRing.of) L = FreeAbelianGroup.of ↑L
-- Mathlib/RingTheory/FreeCommRing.lean
theorem coe_eq : ((↑) : FreeRing α → FreeCommRing α) =
    @Functor.map FreeAbelianGroup _ _ _ fun l : List α => (l : Multiset α)

Proof state:
α : Type u
⊢ castFreeCommRing = Functor.map fun l => ↑l

Tactic:
funext x

Result:
case h
α : Type u
x : FreeRing α
⊢ ↑x = (fun l => ↑l) <$> x