harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem pullback_comp (f : X ⟶ Y) (g : Y ⟶ Z) (x : Subobject Z) :
    (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
x : Subobject Z
⊢ (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)

Tactic:
induction' x using Quotient.inductionOn' with t

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
t : MonoOver Z
⊢ (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
t : MonoOver Z
⊢ (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))

Tactic:
exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_indicatorConstLp_le :
    ‖indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ (eLpNorm (s.indicator fun x => c) p μ).toReal ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Tactic:
refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ENNReal.ofReal (‖c‖ * (μ s).toReal ^ (1 / p.toReal))

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ 0 ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ μ s ^ (1 / p.toReal) ≠ ⊤

Tactic:
exact ENNReal.rpow_ne_top_of_nonneg (by positivity) hμs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ ‖indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Tactic:
rw [indicatorConstLp, Lp.norm_toLp]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ (eLpNorm (s.indicator fun x => c) p μ).toReal ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ 0 ≤ 1 / p.toReal

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ENNReal.ofReal (‖c‖ * (μ s).toReal ^ (1 / p.toReal))

Tactic:
refine (eLpNorm_indicator_const_le _ _).trans_eq ?_

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ ‖c‖ₑ * μ s ^ (1 / p.toReal) = ENNReal.ofReal (‖c‖ * (μ s).toReal ^ (1 / p.toReal))

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ ‖c‖ₑ * μ s ^ (1 / p.toReal) = ENNReal.ofReal (‖c‖ * (μ s).toReal ^ (1 / p.toReal))

Tactic:
rw [ENNReal.ofReal_mul (norm_nonneg _), ofReal_norm, ENNReal.toReal_rpow, ENNReal.ofReal_toReal]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ μ s ^ (1 / p.toReal) ≠ ⊤
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_pi : (π : Angle).toReal = π

Proof state:
⊢ (↑π).toReal = π

Tactic:
rw [toReal_coe_eq_self_iff]

Result:
⊢ -π < π ∧ π ≤ π

Proof state:
⊢ -π < π ∧ π ≤ π

Tactic:
exact ⟨Left.neg_lt_self Real.pi_pos, le_refl _⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_singleton_iff {x : α} [MeasurableSingletonClass α] :
    IntegrableOn f {x} μ ↔ f x = 0 ∨ μ {x} < ∞

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
x : α
inst✝ : MeasurableSingletonClass α
a✝ : α
ha : a✝ ∈ {x}
⊢ f a✝ = f x

Tactic:
simp only [mem_singleton_iff.1 ha]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
x : α
inst✝ : MeasurableSingletonClass α
⊢ f =ᶠ[ae (μ.restrict {x})] fun x_1 => f x

Tactic:
filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha

Result:
case h
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
x : α
inst✝ : MeasurableSingletonClass α
a✝ : α
ha : a✝ ∈ {x}
⊢ f a✝ = f x

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᶠ[ae (μ.restrict {x})] fun x_1 => f x
⊢ IntegrableOn f {x} μ ↔ f x = 0 ∨ μ {x} < ⊤

Tactic:
rw [IntegrableOn, integrable_congr this, integrable_const_iff, isFiniteMeasure_restrict,
  lt_top_iff_ne_top]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
x : α
inst✝ : MeasurableSingletonClass α
⊢ IntegrableOn f {x} μ ↔ f x = 0 ∨ μ {x} < ⊤

Tactic:
have : f =ᵐ[μ.restrict {x}] fun _ => f x := by
  filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha
  simp only [mem_singleton_iff.1 ha]

Result:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᶠ[ae (μ.restrict {x})] fun x_1 => f x
⊢ IntegrableOn f {x} μ ↔ f x = 0 ∨ μ {x} < ⊤
-- Mathlib/Data/List/Basic.lean
theorem get_cons {l : List α} {a : α} {n} (hl) :
    (a :: l).get ⟨n, hl⟩ = if hn : n = 0 then a else
      l.get ⟨n - 1, by contrapose! hl; rw [length_cons]; omega⟩ :=
  getElem_cons hl

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
a : α
n : ℕ
hn : ¬n = 0
hl : l.length ≤ n - 1
⊢ (a :: l).length ≤ n

Tactic:
rw [length_cons]

Result:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
a : α
n : ℕ
hn : ¬n = 0
hl : l.length ≤ n - 1
⊢ l.length + 1 ≤ n

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
a : α
n : ℕ
hl : n < (a :: l).length
hn : ¬n = 0
⊢ n - 1 < l.length

Tactic:
contrapose! hl

Result:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
a : α
n : ℕ
hn : ¬n = 0
hl : l.length ≤ n - 1
⊢ (a :: l).length ≤ n

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
a : α
n : ℕ
hn : ¬n = 0
hl : l.length ≤ n - 1
⊢ l.length + 1 ≤ n

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean
lemma compatibility [WellFoundedLT J]
    {j : J} (e : d.Extension val₀ j) {i : J} (e' : d.Extension val₀ i) (h : i ≤ j) :
    F.map (homOfLE h).op e.val = e'.val

Proof state:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
e : d.Extension val₀ j
i : J
h : i ≤ j
⊢ F.map (homOfLE h).op e.val = (e.ofLE h).val

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
e : d.Extension val₀ j
i : J
e' : d.Extension val₀ i
h : i ≤ j
⊢ F.map (homOfLE h).op e.val = e'.val

Tactic:
obtain rfl : e' = e.ofLE h := Subsingleton.elim _ _

Result:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
e : d.Extension val₀ j
i : J
h : i ≤ j
⊢ F.map (homOfLE h).op e.val = (e.ofLE h).val
-- Mathlib/Algebra/DirectSum/LinearMap.lean
lemma diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne
    {κ : ι → Type*} [∀ i, Fintype (κ i)] [∀ i, DecidableEq (κ i)]
    {s : Finset ι} (h : IsInternal fun i : s ↦ N i)
    (b : (i : s) → Basis (κ i) R (N i)) (σ : ι → ι) (hσ : ∀ i, σ i ≠ i)
    {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N <| σ i)) (hN : ∀ i, i ∉ s → N i = ⊥) :
    Matrix.diag (toMatrix (h.collectedBasis b) (h.collectedBasis b) f) = 0

Proof state:
case h.mk
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i => N ↑i
b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : { x // x ∈ s }
k : κ ↑i
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag ⟨i, k⟩ = 0 ⟨i, k⟩

Tactic:
simp only [Matrix.diag_apply, Pi.zero_apply, toMatrix_apply, IsInternal.collectedBasis_coe]

Result:
case h.mk
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i => N ↑i
b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : { x // x ∈ s }
k : κ ↑i
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i => N ↑i
b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag = 0

Tactic:
ext ⟨i, k⟩

Result:
case h.mk
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i => N ↑i
b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : { x // x ∈ s }
k : κ ↑i
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag ⟨i, k⟩ = 0 ⟨i, k⟩
-- Mathlib/Data/Finset/Prod.lean
theorem diag_union_offDiag : s.diag ∪ s.offDiag = s ×ˢ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.diag ∪ s.offDiag = s ×ˢ s

Tactic:
conv_rhs => rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.diag ∪ s.offDiag = filter (fun a => a.1 = a.2) (s ×ˢ s) ∪ filter (fun a => ¬a.1 = a.2) (s ×ˢ s)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.diag ∪ s.offDiag = filter (fun a => a.1 = a.2) (s ×ˢ s) ∪ filter (fun a => ¬a.1 = a.2) (s ×ˢ s)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem fourierIntegral_convergent_iff (he : Continuous e)
    (hL : Continuous fun p : V × W ↦ L p.1 p.2) {f : V → E} (w : W) :
    Integrable (fun v : V ↦ e (-L v w) • f v) μ ↔ Integrable f μ

Proof state:
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
⊢ Integrable (fun v => e (-(L v) x) • g v) μ

Tactic:
have c : Continuous fun v ↦ e (-L v x) :=
  he.comp (hL.comp (continuous_prod_mk.mpr ⟨continuous_id, continuous_const⟩)).neg

Result:
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
c : Continuous fun v => e (-(L v) x)
⊢ Integrable (fun v => e (-(L v) x) • g v) μ

Proof state:
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
c : Continuous fun v => e (-(L v) x)
⊢ Integrable (fun v => e (-(L v) x) • g v) μ

Tactic:
simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1), Circle.norm_smul]

Result:
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f : V → E
w : W
g : V → E
hg : Integrable g μ
x : W
c : Continuous fun v => e (-(L v) x)
⊢ Integrable (fun a => ‖g a‖) μ
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerRight_id {X Y : C} (f : X ⟶ Y) :
    f ▷ 𝟙_ C = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ▷ 𝟙_ C = (f ▷ 𝟙_ C ≫ (ρ_ Y).hom) ≫ (ρ_ Y).inv

Tactic:
simp [tensorHom_id]

Result:
no goals

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ▷ 𝟙_ C = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv

Tactic:
rw [← assoc, ← rightUnitor_naturality]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ▷ 𝟙_ C = (f ▷ 𝟙_ C ≫ (ρ_ Y).hom) ≫ (ρ_ Y).inv
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem isFractional_of_fg [IsLocalization S P] {I : Submodule R P} (hI : I.FG) :
    IsFractional S I

Proof state:
case intro.intro.mk
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)
⊢ ∃ a ∈ S, ∀ b ∈ ↑I, IsInteger R (a • b)

Tactic:
exact ⟨s, hs1, hs⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : Submodule R P
hI : I.FG
⊢ IsFractional S I

Tactic:
rcases hI with ⟨I, rfl⟩

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : Finset P
⊢ IsFractional S (span R ↑I)

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : Finset P
⊢ IsFractional S (span R ↑I)

Tactic:
rcases exist_integer_multiples_of_finset S I with ⟨⟨s, hs1⟩, hs⟩

Result:
case intro.intro.mk
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)
⊢ IsFractional S (span R ↑I)

Proof state:
case intro.intro.mk
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)
⊢ IsFractional S (span R ↑I)

Tactic:
rw [isFractional_span_iff]

Result:
case intro.intro.mk
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)
⊢ ∃ a ∈ S, ∀ b ∈ ↑I, IsInteger R (a • b)
-- Mathlib/Algebra/Order/SuccPred.lean
lemma strictMono_of_sub_one_lt : (∀ a, ¬ IsMin a → f (a - 1) < f a) → StrictMono f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f (a - 1) < f a) → StrictMono f

Tactic:
simpa [Order.pred_eq_sub_one] using strictMono_of_pred_lt (f := f)

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem restrictScalars_one_smulRight' (x : E) :
    ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x : ℂ →L[ℂ] E) =
      reCLM.smulRight x + I • imCLM.smulRight x

Proof state:
case h.mk
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
a b : ℝ
⊢ (restrictScalars ℝ (smulRight 1 x)) { re := a, im := b } =
    (reCLM.smulRight x + I • imCLM.smulRight x) { re := a, im := b }

Tactic:
simp [map_add, mk_eq_add_mul_I, mul_smul, smul_comm I b x]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
⊢ restrictScalars ℝ (smulRight 1 x) = reCLM.smulRight x + I • imCLM.smulRight x

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
a b : ℝ
⊢ (restrictScalars ℝ (smulRight 1 x)) { re := a, im := b } =
    (reCLM.smulRight x + I • imCLM.smulRight x) { re := a, im := b }
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem DifferentiableWithinAt.dist (hf : DifferentiableWithinAt ℝ f s x)
    (hg : DifferentiableWithinAt ℝ g s x) (hne : f x ≠ g x) :
    DifferentiableWithinAt ℝ (fun y => dist (f y) (g y)) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (fun y => ‖f y - g y‖) s x

Tactic:
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (fun y => Dist.dist (f y) (g y)) s x

Tactic:
simp only [dist_eq_norm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (fun y => ‖f y - g y‖) s x
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finite_mulSupport_inv {I : Ideal R} (hI : I ≠ 0) :
    (mulSupport fun v : HeightOneSpectrum R => (v.asIdeal : FractionalIdeal R⁰ K) ^
      (-((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ))).Finite

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk I).factors)) ≠ 1}.Finite

Tactic:
simp_rw [zpow_neg, Ne, inv_eq_one]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ¬↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) = 1}.Finite

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ (mulSupport fun v => ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))).Finite

Tactic:
rw [mulSupport]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk I).factors)) ≠ 1}.Finite

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ¬↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) = 1}.Finite

Tactic:
exact finite_mulSupport_coe hI

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Reflection.lean
theorem exists_iff : ∀ {m} (P : (Fin m → α) → Prop), Exists P ↔ ∃ x, P x
  | 0, P => by
    simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
    rfl
  | .succ n, P => by simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]

Proof state:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]

Result:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0 ↔ P finZeroElim

Proof state:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0 ↔ P finZeroElim

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.comp_linearMap {f : F → β} {s : Set F} (hf : ConvexOn 𝕜 s f) (g : E →ₗ[𝕜] F) :
    ConvexOn 𝕜 (g ⁻¹' s) (f ∘ g) :=
  ⟨hf.1.linear_preimage _, fun x hx y hy a b ha hb hab =>
    calc
      f (g (a • x + b • y)) = f (a • g x + b • g y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (g (a • x + b • y)) = f (a • g x + b • g y)

Tactic:
rw [g.map_add, g.map_smul, g.map_smul]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem constantCoeff_invOfUnit (φ : R⟦X⟧) (u : Rˣ) :
    constantCoeff R (invOfUnit φ u) = ↑u⁻¹

Proof state:
R : Type u_1
inst✝ : Ring R
φ : R⟦X⟧
u : Rˣ
⊢ (constantCoeff R) (φ.invOfUnit u) = ↑u⁻¹

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]

Result:
no goals