harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supported_iUnion {δ : Type*} (s : δ → Set α) :
    supported M R (⋃ i, s i) = ⨆ i, supported M R (s i)

Proof state:
case intro.refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ i, s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : x ∉ l.support
x✝ : a ≠ 0
⊢ single x a ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Tactic:
by_cases h : ∃ i, x ∈ s i

Result:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ i, s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : x ∉ l.support
x✝ : a ≠ 0
h : ∃ i, x ∈ s i
⊢ single x a ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ i, s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : x ∉ l.support
x✝ : a ≠ 0
h : ¬∃ i, x ∈ s i
⊢ single x a ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Proof state:
case pos.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ i, s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : x ∉ l.support
x✝ : a ≠ 0
i : δ
hi : x ∈ s i
⊢ single x a ∈ ⨆ i, supported M R (s i)

Tactic:
exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)

Result:
no goals

Proof state:
case intro.refine_1
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ i, s i
l : α →₀ M
⊢ 0 ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Tactic:
exact zero_mem _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setLaverage_eq' (f : α → ℝ≥0∞) (s : Set α) :
    ⨍⁻ x in s, f x ∂μ = ∫⁻ x, f x ∂(μ s)⁻¹ • μ.restrict s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s

Tactic:
simp only [laverage_eq', restrict_apply_univ]

Result:
no goals
-- Mathlib/Analysis/Fourier/ZMod.lean
lemma dft_smul_const {R : Type*} [Ring R] [Module ℂ R] [Module R E] [IsScalarTower ℂ R E]
    (Φ : ZMod N → R) (e : E) :
    𝓕 (fun j ↦ Φ j • e) = fun k ↦ 𝓕 Φ k • e

Proof state:
N : ℕ
inst✝⁶ : NeZero N
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
R : Type u_2
inst✝³ : Ring R
inst✝² : Module ℂ R
inst✝¹ : Module R E
inst✝ : IsScalarTower ℂ R E
Φ : ZMod N → R
e : E
⊢ (𝓕 fun j => Φ j • e) = fun k => 𝓕 Φ k • e

Tactic:
simp only [dft_def, sum_smul, smul_assoc]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem mem_rtakeWhile_imp {x : α} (hx : x ∈ rtakeWhile p l) : p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true

Tactic:
exact mem_takeWhile_imp hx

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true

Tactic:
rw [rtakeWhile, mem_reverse] at hx

Result:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_setIfInBounds (a : Vector α n) (i x) :
    (a.setIfInBounds i x).toList = a.toList.set i x

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
x : α
⊢ (a.setIfInBounds i x).toList = a.toList.set i x

Tactic:
simp [Vector.setIfInBounds]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem liminf_sdiff [NeBot f] (a : α) : liminf u f \ a = liminf (fun b => u b \ a) f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ liminf u f \ a = liminf (fun b => u b \ a) f

Tactic:
simp only [sdiff_eq, inf_comm _ aᶜ, inf_liminf]

Result:
no goals
-- Mathlib/LinearAlgebra/Goursat.lean
lemma goursatFst_prod_goursatSnd_le : L.goursatFst.prod L.goursatSnd ≤ L

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
⊢ L.goursatFst.prod L.goursatSnd ≤ L

Tactic:
simpa only [← toAddSubgroup_le, goursatFst_toAddSubgroup, goursatSnd_toAddSubgroup]
  using L.toAddSubgroup.goursatFst_prod_goursatSnd_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.pmap {p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) {H₁ H₂} :
    pmap f l₁ H₁ ~ pmap f l₂ H₂

Proof state:
case swap
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ : List α
x y : α
l✝ : List α
H₁ : ∀ (a : α), a ∈ y :: x :: l✝ → p a
H₂ : ∀ (a : α), a ∈ x :: y :: l✝ → p a
⊢ List.pmap f (y :: x :: l✝) H₁ ~ List.pmap f (x :: y :: l✝) H₂

Tactic:
simp [swap]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ : List α
H₁ H₂ : ∀ (a : α), a ∈ [] → p a
⊢ List.pmap f [] H₁ ~ List.pmap f [] H₂

Tactic:
simp

Result:
no goals

Proof state:
case trans
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
_p₁ : l₁✝ ~ l₂✝
p₂ : l₂✝ ~ l₃✝
IH₁ : ∀ {H₁ : ∀ (a : α), a ∈ l₁✝ → p a} {H₂ : ∀ (a : α), a ∈ l₂✝ → p a}, List.pmap f l₁✝ H₁ ~ List.pmap f l₂✝ H₂
IH₂ : ∀ {H₁ : ∀ (a : α), a ∈ l₂✝ → p a} {H₂ : ∀ (a : α), a ∈ l₃✝ → p a}, List.pmap f l₂✝ H₁ ~ List.pmap f l₃✝ H₂
H₁ : ∀ (a : α), a ∈ l₁✝ → p a
H₂ : ∀ (a : α), a ∈ l₃✝ → p a
⊢ List.pmap f l₁✝ H₁ ~ List.pmap f l₃✝ H₂

Tactic:
exact IH₁.trans (IH₂ (H₁ := fun a m => H₂ a (p₂.subset m)))

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH : ∀ {H₁ : ∀ (a : α), a ∈ l₁✝ → p a} {H₂ : ∀ (a : α), a ∈ l₂✝ → p a}, List.pmap f l₁✝ H₁ ~ List.pmap f l₂✝ H₂
H₁ : ∀ (a : α), a ∈ x :: l₁✝ → p a
H₂ : ∀ (a : α), a ∈ x :: l₂✝ → p a
⊢ List.pmap f (x :: l₁✝) H₁ ~ List.pmap f (x :: l₂✝) H₂

Tactic:
simp [IH, Perm.cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p✝ : α → Prop
f : (a : α) → p✝ a → β
l₁ l₂ : List α
p : l₁ ~ l₂
H₁ : ∀ (a : α), a ∈ l₁ → p✝ a
H₂ : ∀ (a : α), a ∈ l₂ → p✝ a
⊢ List.pmap f l₁ H₁ ~ List.pmap f l₂ H₂

Tactic:
induction p with
| nil => simp
| cons x _p IH => simp [IH, Perm.cons]
| swap x y => simp [swap]
| trans _p₁ p₂ IH₁ IH₂ => exact IH₁.trans (IH₂ (H₁ := fun a m => H₂ a (p₂.subset m)))

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean
lemma contMDiffAt_ofComplex {n : WithTop ℕ∞} {z : ℂ} (hz : 0 < z.im) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) n ofComplex z

Proof state:
case right
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
    (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)

Tactic:
simp only [extChartAt, PartialHomeomorph.extend, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl, PartialHomeomorph.toFun_eq_coe, PartialHomeomorph.refl_partialEquiv,
  PartialEquiv.refl_source, PartialHomeomorph.singletonChartedSpace_chartAt_eq,
  PartialEquiv.refl_symm, PartialEquiv.refl_coe, CompTriple.comp_eq, modelWithCornersSelf_coe,
  Set.range_id, id_eq, contDiffWithinAt_univ]

Result:
case right
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContDiffAt ℂ n (↑(chartAt ℂ (↑ofComplex z)) ∘ ↑ofComplex) z

Proof state:
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex) z

Tactic:
rw [contMDiffAt_iff]

Result:
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z ∧
    ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
      (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)

Proof state:
case left
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z

Tactic:
rw [ContinuousAt, nhds_induced, tendsto_comap_iff]

Result:
case left
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ Tendsto (Subtype.val ∘ ↑ofComplex) (nhds z) (nhds ↑(↑ofComplex z))

Proof state:
case left
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ Tendsto id (nhds z) (nhds ↑(↑ofComplex z))

Tactic:
simpa only [ofComplex_apply_of_im_pos hz, Subtype.coe_mk] using tendsto_id

Result:
no goals

Proof state:
case right
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContDiffAt ℂ n (↑(chartAt ℂ (↑ofComplex z)) ∘ ↑ofComplex) z

Tactic:
exact contDiffAt_id.congr_of_eventuallyEq (eventuallyEq_coe_comp_ofComplex hz)

Result:
no goals

Proof state:
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z ∧
    ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
      (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)

Tactic:
constructor

Result:
case left
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z

case right
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
    (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)

Proof state:
case left
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ Tendsto (Subtype.val ∘ ↑ofComplex) (nhds z) (nhds ↑(↑ofComplex z))

Tactic:
refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_

Result:
case left
n : WithTop ℕ∞
z : ℂ
hz : 0 < z.im
⊢ Tendsto id (nhds z) (nhds ↑(↑ofComplex z))
-- Mathlib/Computability/TMConfig.lean
theorem code_is_ok (c) : Code.Ok c

Proof state:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let v ←
      (fun v => do
            let n ← f.eval v
            let ns ← fs.eval v
            pure (n.headI :: ns))
          v
    eval step (Cfg.ret k v)

Tactic:
simp only [bind_assoc, Cont.eval, pure_bind]

Result:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Proof state:
case cons.e_a.h.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))

Tactic:
refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_) <;>
  exact reaches_eval (ReflTransGen.single rfl)

Result:
no goals

Proof state:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [Code.eval, IHf]

Result:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let v ←
      (fun v => do
            let n ← f.eval v
            let ns ← fs.eval v
            pure (n.headI :: ns))
          v
    eval step (Cfg.ret k v)

Proof state:
case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v => Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) k v) = do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval]

Result:
case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) = do
    let v ← Nat.rec (f.eval v.tail) (fun y x => g.eval (y :: v.tail)) v.headI
    eval step (Cfg.ret k v)

Proof state:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.141342 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.141342

f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Tactic:
swap

Result:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.141342

case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.141342 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful [IsCofilteredOrEmpty D]
    [F.Full] [F.Faithful] (h : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) : IsCofilteredOrEmpty C

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Tactic:
obtain ⟨c, ⟨f⟩⟩ := h d.unop

Result:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ IsCofilteredOrEmpty C

Tactic:
suffices IsFilteredOrEmpty Cᵒᵖ from isCofilteredOrEmpty_of_isFilteredOrEmpty_op _

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ IsFilteredOrEmpty Cᵒᵖ

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ IsFilteredOrEmpty Cᵒᵖ

Tactic:
refine IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Proof state:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Tactic:
exact ⟨op c, ⟨f.op⟩⟩

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma ofColex_ne_ofColex {s t : Colex α} : ofColex s ≠ ofColex t ↔ s ≠ t

Proof state:
α : Type u_1
s t : Colex α
⊢ s.ofColex ≠ t.ofColex ↔ s ≠ t

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_def (m k : Nat) : m % k = m - k * (m / k)

Proof state:
m k : Nat
⊢ m = m % k + k * (m / k)

Tactic:
apply (Nat.mod_add_div _ _).symm

Result:
no goals

Proof state:
m k : Nat
⊢ m % k = m - k * (m / k)

Tactic:
rw [Nat.sub_eq_of_eq_add]

Result:
m k : Nat
⊢ m = m % k + k * (m / k)
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma sub_add_eq_sub_sub : s - (t + u) = s - t - u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s - (t + u) = s - t - u

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
a✝ : α
⊢ count a✝ (s - (t + u)) = count a✝ (s - t - u)

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
a✝ : α
⊢ count a✝ (s - (t + u)) = count a✝ (s - t - u)

Tactic:
simp [Nat.sub_add_eq]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem movedBy_mem_fixedBy_of_commute {g h : G} (comm : Commute g h) :
    (fixedBy α g)ᶜ ∈ fixedBy (Set α) h

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
⊢ (fixedBy α g)ᶜ ∈ fixedBy (Set α) h

Tactic:
rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem add_rat (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (x + r)

Proof state:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r

Tactic:
rw [Algebra.id.smul_eq_mul, id]

Result:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den * n) = ↑m / ↑n + ↑r

Proof state:
case intro.intro.intro.intro.intro
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
this✝ : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
this : ↑r.den ^ p ≠ 0
⊢ C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p

Tactic:
simp [mul_rpow, Nat.cast_nonneg, mul_div_mul_left, this]

Result:
no goals

Proof state:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ ↑r.den ^ p ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p (x + ↑r)

Tactic:
rcases h.exists_pos with ⟨C, _hC₀, hC⟩

Result:
case intro.intro
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (x + ↑r)

Proof state:
case intro.intro.intro.intro.intro
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p

Tactic:
have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r := by
  rw [Algebra.id.smul_eq_mul, id]
  nth_rewrite 4 [← Rat.num_div_den r]
  push_cast
  rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]

Result:
case intro.intro.intro.intro.intro
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_le_one_of_lintegral_rpow_eq_one {p q : ℝ} (hpq : p.IsConjExponent q)
    {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf_norm : ∫⁻ a, f a ^ p ∂μ = 1)
    (hg_norm : ∫⁻ a, g a ^ q ∂μ = 1) : (∫⁻ a, (f * g) a ∂μ) ≤ 1

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
  one_mul, one_mul, hpq.inv_add_inv_conj_ennreal]

Result:
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ⊤

Proof state:
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ⊤

Tactic:
simp [hpq.symm.pos]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ = 1

Tactic:
simp only [div_eq_mul_inv]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_add_left']

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ AEMeasurable (fun a => f a ^ p * (ENNReal.ofReal p)⁻¹) μ

Proof state:
case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ AEMeasurable (fun a => f a ^ p * (ENNReal.ofReal p)⁻¹) μ

Tactic:
exact (hf.pow_const _).mul_const _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (mkArray n (f a)).flatten

Proof state:
α : Type u_1
n : Nat
a : α
β : Type u_2
f : α → Array β
⊢ (flatMap f (mkArray n a)).toList = (mkArray n (f a)).flatten.toList

Tactic:
simp [flatMap_toList, List.flatMap_replicate]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
β : Type u_2
f : α → Array β
⊢ flatMap f (mkArray n a) = (mkArray n (f a)).flatten

Tactic:
rw [← toList_inj]

Result:
α : Type u_1
n : Nat
a : α
β : Type u_2
f : α → Array β
⊢ (flatMap f (mkArray n a)).toList = (mkArray n (f a)).flatten.toList
-- Mathlib/Data/List/Chain.lean
theorem Chain.rel [IsTrans α R] (hl : l.Chain R a) (hb : b ∈ l) : R a b

Proof state:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst✝ : IsTrans α R
hl : Chain R a l
hb : b ∈ l
⊢ R a b

Tactic:
rw [chain_iff_pairwise] at hl

Result:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst✝ : IsTrans α R
hl : Pairwise R (a :: l)
hb : b ∈ l
⊢ R a b

Proof state:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst✝ : IsTrans α R
hl : Pairwise R (a :: l)
hb : b ∈ l
⊢ R a b

Tactic:
exact rel_of_pairwise_cons hl hb

Result:
no goals